:: MATRIX17 semantic presentation

begin

              Lm1:  for n, i being Nat st i in Seg n holds
(n + 1) - i in Seg n
proof
let n, i be Nat; ::_thesis: ( i in Seg n implies (n + 1) - i in Seg n )
assume A1: i in Seg n ; ::_thesis: (n + 1) - i in Seg n
 i <= n by A1, FINSEQ_1:1;
then  i + 1 <= n + 1 by XREAL_1:6;
then A3: (i + 1) - i <= (n + 1) - i by XREAL_1:9;
 1 <= i by A1, FINSEQ_1:1;
then  n + 1 <= i + n by XREAL_1:6;
then A4: (n + 1) - i <= (i + n) - i by XREAL_1:9;
 (n + 1) - i in NAT by A3, INT_1:3;
hence  (n + 1) - i in Seg n by A3, A4; ::_thesis: verum
end;

Lm2:  for n, i, j being Nat st [i,j] in [:(Seg n),(Seg n):] holds
( (n + 1) - j in Seg n & (n + 1) - i in Seg n )
proof
let n, i, j be Nat; ::_thesis: ( [i,j] in [:(Seg n),(Seg n):] implies ( (n + 1) - j in Seg n & (n + 1) - i in Seg n ) )
assume  [i,j] in [:(Seg n),(Seg n):] ; ::_thesis: ( (n + 1) - j in Seg n & (n + 1) - i in Seg n )
then  ( i in Seg n & j in Seg n ) by ZFMISC_1:87;
hence  ( (n + 1) - j in Seg n & (n + 1) - i in Seg n ) by Lm1; ::_thesis: verum
end;

definition
let K be Field;
let n be Nat;
let M be Matrix of n,K;
attrM is subsymmetric  means :Def1: :: MATRIX17:def 1
 for i, j, k, l being Nat st [i,j] in Indices M & k = (n + 1) - j & l = (n + 1) - i holds
M * (i,j) = M * (k,l);
end;

:: deftheorem Def1 defines subsymmetric MATRIX17:def_1_:_
 for K being Field
for n being Nat
for M being Matrix of n,K holds
( M is subsymmetric iff for i, j, k, l being Nat st [i,j] in Indices M & k = (n + 1) - j & l = (n + 1) - i holds
M * (i,j) = M * (k,l) );

registration
let n be Nat;
let K be Field;
let a be Element of K;
cluster(n,n) --> a ->  subsymmetric for Matrix of n,K;
coherence
 for b1 being Matrix of n,K st b1 = (n,n) --> a holds
b1 is subsymmetric
proof
let M be Matrix of n,K; ::_thesis: ( M = (n,n) --> a implies M is subsymmetric )
assume A1: M = (n,n) --> a ; ::_thesis: M is subsymmetric
let i, j, k, l be Nat; :: according to MATRIX17:def_1 ::_thesis: ( [i,j] in Indices M & k = (n + 1) - j & l = (n + 1) - i implies M * (i,j) = M * (k,l) )
assume that
A2: [i,j] in Indices M and
A3: ( k = (n + 1) - j & l = (n + 1) - i ) ; ::_thesis: M * (i,j) = M * (k,l)
A4: Indices M = [:(Seg n),(Seg n):] by MATRIX_1:24;
 ( k in Seg n & l in Seg n ) by A3, A2, A4, Lm2;
then  [k,l] in [:(Seg n),(Seg n):] by ZFMISC_1:87;
then  M * (k,l) = a by A1, A4, MATRIX_2:1;
hence  M * (i,j) = M * (k,l) by A1, A2, MATRIX_2:1; ::_thesis: verum
end;
end;

registration
let n be Nat;
let K be Field;
cluster Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular subsymmetric for Matrix of n,n, the carrier of K;
existence
 ex b1 being Matrix of n,K st b1 is subsymmetric
proof
take  (n,n) --> (0. K) ; ::_thesis: (n,n) --> (0. K) is subsymmetric
thus  (n,n) --> (0. K) is subsymmetric ; ::_thesis: verum
end;
end;

registration
let n be Nat;
let K be Field;
let M be subsymmetric Matrix of n,K;
cluster - M ->  subsymmetric for Matrix of n,K;
coherence
 for b1 being Matrix of n,K st b1 = - M holds
b1 is subsymmetric
proof
let N be Matrix of n,K; ::_thesis: ( N = - M implies N is subsymmetric )
assume A1: N = - M ; ::_thesis: N is subsymmetric
A2: Indices M = [:(Seg n),(Seg n):] by MATRIX_1:24;
let i, j, k, l be Nat; :: according to MATRIX17:def_1 ::_thesis: ( [i,j] in Indices N & k = (n + 1) - j & l = (n + 1) - i implies N * (i,j) = N * (k,l) )
assume that
A3: [i,j] in Indices N and
A4: ( k = (n + 1) - j & l = (n + 1) - i ) ; ::_thesis: N * (i,j) = N * (k,l)
A5: Indices (- M) = [:(Seg n),(Seg n):] by MATRIX_1:24;
then  ( i in Seg n & j in Seg n ) by A1, A3, ZFMISC_1:87;
then  ( k in Seg n & l in Seg n ) by A4, Lm1;
then A6: [k,l] in [:(Seg n),(Seg n):] by ZFMISC_1:87;
(- M) * (i,j) = - (M * (i,j)) by A1, A2, A3, A5, MATRIX_3:def_2
.= - (M * (k,l)) by A1, A2, A3, A5, A4, Def1
.= (- M) * (k,l) by A2, A6, MATRIX_3:def_2 ;
hence  N * (i,j) = N * (k,l) by A1; ::_thesis: verum
end;
end;

registration
let n be Nat;
let K be Field;
let M1, M2 be subsymmetric Matrix of n,K;
clusterM1 + M2 ->  subsymmetric for Matrix of n,K;
coherence
 for b1 being Matrix of n,K st b1 = M1 + M2 holds
b1 is subsymmetric
proof
let M be Matrix of n,K; ::_thesis: ( M = M1 + M2 implies M is subsymmetric )
assume A1: M = M1 + M2 ; ::_thesis: M is subsymmetric
let i, j, k, l be Nat; :: according to MATRIX17:def_1 ::_thesis: ( [i,j] in Indices M & k = (n + 1) - j & l = (n + 1) - i implies M * (i,j) = M * (k,l) )
assume that
A2: [i,j] in Indices M and
A3: ( k = (n + 1) - j & l = (n + 1) - i ) ; ::_thesis: M * (i,j) = M * (k,l)
A4: Indices M = [:(Seg n),(Seg n):] by MATRIX_1:24;
 ( (n + 1) - j in Seg n & (n + 1) - i in Seg n ) by A2, A4, Lm2;
then A5: [k,l] in [:(Seg n),(Seg n):] by A3, ZFMISC_1:87;
A6: ( Indices M1 = [:(Seg n),(Seg n):] & Indices M2 = [:(Seg n),(Seg n):] ) by MATRIX_1:24;
(M1 + M2) * (i,j) = (M1 * (i,j)) + (M2 * (i,j)) by A2, A4, A6, MATRIX_3:def_3
.= (M1 * (k,l)) + (M2 * (i,j)) by A2, A4, A6, A3, Def1
.= (M1 * (k,l)) + (M2 * (k,l)) by A2, A4, A6, A3, Def1
.= (M1 + M2) * (k,l) by A6, A5, MATRIX_3:def_3 ;
hence  M * (i,j) = M * (k,l) by A1; ::_thesis: verum
end;
end;

registration
let n be Nat;
let K be Field;
let a be Element of K;
let M be subsymmetric Matrix of n,K;
clustera * M ->  subsymmetric for Matrix of n,K;
coherence
 for b1 being Matrix of n,K st b1 = a * M holds
b1 is subsymmetric
proof
let M1 be Matrix of n,K; ::_thesis: ( M1 = a * M implies M1 is subsymmetric )
assume A1: M1 = a * M ; ::_thesis: M1 is subsymmetric
A2: Indices M = [:(Seg n),(Seg n):] by MATRIX_1:24;
let i, j, k, l be Nat; :: according to MATRIX17:def_1 ::_thesis: ( [i,j] in Indices M1 & k = (n + 1) - j & l = (n + 1) - i implies M1 * (i,j) = M1 * (k,l) )
assume that
A3: [i,j] in Indices M1 and
A4: ( k = (n + 1) - j & l = (n + 1) - i ) ; ::_thesis: M1 * (i,j) = M1 * (k,l)
 Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24;
then  ( k in Seg n & l in Seg n ) by A3, A4, Lm2;
then A5: [k,l] in [:(Seg n),(Seg n):] by ZFMISC_1:87;
A6: [i,j] in Indices M by A2, A3, MATRIX_1:24;
then (a * M) * (i,j) = a * (M * (i,j)) by MATRIX_3:def_5
.= a * (M * (k,l)) by A4, A6, Def1
.= (a * M) * (k,l) by A2, A5, MATRIX_3:def_5 ;
hence  M1 * (i,j) = M1 * (k,l) by A1; ::_thesis: verum
end;
end;

registration
let n be Nat;
let K be Field;
let M1, M2 be subsymmetric Matrix of n,K;
clusterK287(K,M1,M2) ->  subsymmetric for Matrix of n,K;
coherence
 for b1 being Matrix of n,K st b1 = M1 - M2 holds
b1 is subsymmetric
proof
 M1 - M2 = M1 + (- M2) ;
hence  for b1 being Matrix of n,K st b1 = M1 - M2 holds
b1 is subsymmetric ; ::_thesis: verum
end;
end;

registration
let n be Nat;
let K be Field;
let M be subsymmetric Matrix of n,K;
clusterM @  ->  subsymmetric for Matrix of n,K;
coherence
 for b1 being Matrix of n,K st b1 = M @ holds
b1 is subsymmetric
proof
let M1 be Matrix of n,K; ::_thesis: ( M1 = M @ implies M1 is subsymmetric )
assume A1: M1 = M @ ; ::_thesis: M1 is subsymmetric
A2: Indices M = [:(Seg n),(Seg n):] by MATRIX_1:24;
let i, j, k, l be Nat; :: according to MATRIX17:def_1 ::_thesis: ( [i,j] in Indices M1 & k = (n + 1) - j & l = (n + 1) - i implies M1 * (i,j) = M1 * (k,l) )
assume that
A3: [i,j] in Indices M1 and
A4: ( k = (n + 1) - j & l = (n + 1) - i ) ; ::_thesis: M1 * (i,j) = M1 * (k,l)
 [i,j] in [:(Seg n),(Seg n):] by A3, MATRIX_1:24;
then A5: ( i in Seg n & j in Seg n ) by ZFMISC_1:87;
then A6: [j,i] in [:(Seg n),(Seg n):] by ZFMISC_1:87;
 ( (n + 1) - j in Seg n & (n + 1) - i in Seg n ) by A5, Lm1;
then A7: ( [((n + 1) - i),((n + 1) - j)] in [:(Seg n),(Seg n):] & [((n + 1) - j),((n + 1) - i)] in [:(Seg n),(Seg n):] ) by ZFMISC_1:87;
thus M1 * (i,j) = M * (j,i) by A1, A2, A6, MATRIX_1:def_6
.= M * (l,k) by A4, A6, A2, Def1
.= M1 * (k,l) by A1, A7, A2, A4, MATRIX_1:def_6 ; ::_thesis: verum
end;
end;

registration
let n be Nat;
let K be Field;
cluster line_circulant  ->  subsymmetric for Matrix of n,n, the carrier of K;
coherence
 for b1 being Matrix of n,K st b1 is line_circulant holds
b1 is subsymmetric
proof
let M be Matrix of n,K; ::_thesis: ( M is line_circulant implies M is subsymmetric )
assume  M is line_circulant ; ::_thesis: M is subsymmetric
then consider p being FinSequence of K such that
 len p = width M and
A1: M is_line_circulant_about p by MATRIX16:def_2;
A2: Indices M = [:(Seg n),(Seg n):] by MATRIX_1:24;
let i, j, k, l be Nat; :: according to MATRIX17:def_1 ::_thesis: ( [i,j] in Indices M & k = (n + 1) - j & l = (n + 1) - i implies M * (i,j) = M * (k,l) )
assume that
A3: [i,j] in Indices M and
A4: ( k = (n + 1) - j & l = (n + 1) - i ) ; ::_thesis: M * (i,j) = M * (k,l)
 ( k in Seg n & l in Seg n ) by A3, A2, A4, Lm2;
then A5: [k,l] in [:(Seg n),(Seg n):] by ZFMISC_1:87;
M * (k,l) = p . (((((n + 1) - i) - ((n + 1) - j)) mod (len p)) + 1) by A1, A2, A4, A5, MATRIX16:def_1
.= p . (((j - i) mod (len p)) + 1) ;
hence  M * (i,j) = M * (k,l) by A3, A1, MATRIX16:def_1; ::_thesis: verum
end;
cluster col_circulant  ->  subsymmetric for Matrix of n,n, the carrier of K;
coherence
 for b1 being Matrix of n,K st b1 is col_circulant holds
b1 is subsymmetric
proof
let M be Matrix of n,K; ::_thesis: ( M is col_circulant implies M is subsymmetric )
assume  M is col_circulant ; ::_thesis: M is subsymmetric
then consider p being FinSequence of K such that
A1: len p = len M and
A2: M is_col_circulant_about p by MATRIX16:def_5;
A3: len M = n by MATRIX_1:24;
A4: Indices M = [:(Seg n),(Seg n):] by MATRIX_1:24;
let i, j, k, l be Nat; :: according to MATRIX17:def_1 ::_thesis: ( [i,j] in Indices M & k = (n + 1) - j & l = (n + 1) - i implies M * (i,j) = M * (k,l) )
assume that
A5: [i,j] in Indices M and
A6: ( k = (n + 1) - j & l = (n + 1) - i ) ; ::_thesis: M * (i,j) = M * (k,l)
 ( k in Seg n & l in Seg n ) by A5, A4, A6, Lm2;
then A7: [k,l] in [:(Seg n),(Seg n):] by ZFMISC_1:87;
M * (k,l) = p . (((((n + 1) - j) - ((n + 1) - i)) mod n) + 1) by A1, A2, A3, A4, A6, A7, MATRIX16:def_4
.= p . (((i - j) mod n) + 1) ;
hence  M * (i,j) = M * (k,l) by A1, A2, A3, A5, MATRIX16:def_4; ::_thesis: verum
end;
end;

definition
let K be Field;
let n be Nat;
let M be Matrix of n,K;
attrM is Anti-subsymmetric  means :Def2: :: MATRIX17:def 2
 for i, j, k, l being Nat st [i,j] in Indices M & k = (n + 1) - j & l = (n + 1) - i holds
M * (i,j) = - (M * (k,l));
end;

:: deftheorem Def2 defines Anti-subsymmetric MATRIX17:def_2_:_
 for K being Field
for n being Nat
for M being Matrix of n,K holds
( M is Anti-subsymmetric iff for i, j, k, l being Nat st [i,j] in Indices M & k = (n + 1) - j & l = (n + 1) - i holds
M * (i,j) = - (M * (k,l)) );

registration
let n be Nat;
let K be Field;
cluster Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular Anti-subsymmetric for Matrix of n,n, the carrier of K;
existence
 ex b1 being Matrix of n,K st b1 is Anti-subsymmetric
proof
take M = (n,n) --> (0. K); ::_thesis: M is Anti-subsymmetric
let i, j, k, l be Nat; :: according to MATRIX17:def_2 ::_thesis: ( [i,j] in Indices M & k = (n + 1) - j & l = (n + 1) - i implies M * (i,j) = - (M * (k,l)) )
assume that
A1: [i,j] in Indices M and
A2: ( k = (n + 1) - j & l = (n + 1) - i ) ; ::_thesis: M * (i,j) = - (M * (k,l))
A3: Indices M = [:(Seg n),(Seg n):] by MATRIX_1:24;
 ( k in Seg n & l in Seg n ) by A2, A1, A3, Lm2;
then  [k,l] in [:(Seg n),(Seg n):] by ZFMISC_1:87;
then A4: M * (k,l) = 0. K by A3, MATRIX_2:1;
 0. K = - (0. K) by RLVECT_1:12;
hence  M * (i,j) = - (M * (k,l)) by A4, A1, MATRIX_2:1; ::_thesis: verum
end;
end;

theorem :: MATRIX17:1
for K being Fanoian Field
for n, i, j, k, l being Nat
for M1 being Matrix of n,K st [i,j] in Indices M1 & i + j = n + 1 & k = (n + 1) - j & l = (n + 1) - i & M1 is Anti-subsymmetric holds
M1 * (i,j) = 0. K
proof
let K be Fanoian Field; ::_thesis: for n, i, j, k, l being Nat
for M1 being Matrix of n,K st [i,j] in Indices M1 & i + j = n + 1 & k = (n + 1) - j & l = (n + 1) - i & M1 is Anti-subsymmetric holds
M1 * (i,j) = 0. K
let n, i, j, k, l be Nat; ::_thesis: for M1 being Matrix of n,K st [i,j] in Indices M1 & i + j = n + 1 & k = (n + 1) - j & l = (n + 1) - i & M1 is Anti-subsymmetric holds
M1 * (i,j) = 0. K
let M1 be Matrix of n,K; ::_thesis: ( [i,j] in Indices M1 & i + j = n + 1 & k = (n + 1) - j & l = (n + 1) - i & M1 is Anti-subsymmetric implies M1 * (i,j) = 0. K )
assume that
A1: [i,j] in Indices M1 and
A2: ( i + j = n + 1 & k = (n + 1) - j & l = (n + 1) - i ) and
A3: M1 is Anti-subsymmetric ; ::_thesis: M1 * (i,j) = 0. K
 M1 * (i,j) = - (M1 * (i,j)) by A1, A3, A2, Def2;
then  (M1 * (i,j)) + (M1 * (i,j)) = 0. K by RLVECT_1:5;
then  ((1_ K) * (M1 * (i,j))) + (M1 * (i,j)) = 0. K by VECTSP_1:def_8;
then  ((1_ K) * (M1 * (i,j))) + ((1_ K) * (M1 * (i,j))) = 0. K by VECTSP_1:def_8;
then  ( (1_ K) + (1_ K) <> 0. K & ((1_ K) + (1_ K)) * (M1 * (i,j)) = 0. K ) by VECTSP_1:def_7, VECTSP_1:def_19;
hence  M1 * (i,j) = 0. K by VECTSP_1:12; ::_thesis: verum
end;

registration
let n be Nat;
let K be Field;
let M be Anti-subsymmetric Matrix of n,K;
cluster - M ->  Anti-subsymmetric for Matrix of n,K;
coherence
 for b1 being Matrix of n,K st b1 = - M holds
b1 is Anti-subsymmetric
proof
let N be Matrix of n,K; ::_thesis: ( N = - M implies N is Anti-subsymmetric )
assume A1: N = - M ; ::_thesis: N is Anti-subsymmetric
A2: Indices M = [:(Seg n),(Seg n):] by MATRIX_1:24;
let i, j, k, l be Nat; :: according to MATRIX17:def_2 ::_thesis: ( [i,j] in Indices N & k = (n + 1) - j & l = (n + 1) - i implies N * (i,j) = - (N * (k,l)) )
assume that
A3: [i,j] in Indices N and
A4: ( k = (n + 1) - j & l = (n + 1) - i ) ; ::_thesis: N * (i,j) = - (N * (k,l))
A5: Indices (- M) = [:(Seg n),(Seg n):] by MATRIX_1:24;
then  ( i in Seg n & j in Seg n ) by A1, A3, ZFMISC_1:87;
then  ( k in Seg n & l in Seg n ) by A4, Lm1;
then A6: [k,l] in [:(Seg n),(Seg n):] by ZFMISC_1:87;
(- M) * (i,j) = - (M * (i,j)) by A1, A2, A3, A5, MATRIX_3:def_2
.= - (- (M * (k,l))) by A1, A2, A3, A5, A4, Def2
.= - ((- M) * (k,l)) by A2, A6, MATRIX_3:def_2 ;
hence  N * (i,j) = - (N * (k,l)) by A1; ::_thesis: verum
end;
end;

registration
let n be Nat;
let K be Field;
let M1, M2 be Anti-subsymmetric Matrix of n,K;
clusterM1 + M2 ->  Anti-subsymmetric for Matrix of n,K;
coherence
 for b1 being Matrix of n,K st b1 = M1 + M2 holds
b1 is Anti-subsymmetric
proof
let M be Matrix of n,K; ::_thesis: ( M = M1 + M2 implies M is Anti-subsymmetric )
assume A1: M = M1 + M2 ; ::_thesis: M is Anti-subsymmetric
let i, j, k, l be Nat; :: according to MATRIX17:def_2 ::_thesis: ( [i,j] in Indices M & k = (n + 1) - j & l = (n + 1) - i implies M * (i,j) = - (M * (k,l)) )
assume that
A2: [i,j] in Indices M and
A3: ( k = (n + 1) - j & l = (n + 1) - i ) ; ::_thesis: M * (i,j) = - (M * (k,l))
A4: Indices M = [:(Seg n),(Seg n):] by MATRIX_1:24;
 ( (n + 1) - j in Seg n & (n + 1) - i in Seg n ) by A2, A4, Lm2;
then A5: [k,l] in [:(Seg n),(Seg n):] by A3, ZFMISC_1:87;
A6: ( Indices M1 = [:(Seg n),(Seg n):] & Indices M2 = [:(Seg n),(Seg n):] ) by MATRIX_1:24;
(M1 + M2) * (i,j) = (M1 * (i,j)) + (M2 * (i,j)) by A2, A4, A6, MATRIX_3:def_3
.= (- (M1 * (k,l))) + (M2 * (i,j)) by A2, A4, A6, A3, Def2
.= (- (M1 * (k,l))) + (- (M2 * (k,l))) by A2, A4, A6, A3, Def2
.= - ((M1 * (k,l)) + (M2 * (k,l))) by RLVECT_1:31
.= - ((M1 + M2) * (k,l)) by A6, A5, MATRIX_3:def_3 ;
hence  M * (i,j) = - (M * (k,l)) by A1; ::_thesis: verum
end;
end;

registration
let n be Nat;
let K be Field;
let a be Element of K;
let M be Anti-subsymmetric Matrix of n,K;
clustera * M ->  Anti-subsymmetric for Matrix of n,K;
coherence
 for b1 being Matrix of n,K st b1 = a * M holds
b1 is Anti-subsymmetric
proof
let M1 be Matrix of n,K; ::_thesis: ( M1 = a * M implies M1 is Anti-subsymmetric )
assume A1: M1 = a * M ; ::_thesis: M1 is Anti-subsymmetric
A2: Indices M = [:(Seg n),(Seg n):] by MATRIX_1:24;
let i, j, k, l be Nat; :: according to MATRIX17:def_2 ::_thesis: ( [i,j] in Indices M1 & k = (n + 1) - j & l = (n + 1) - i implies M1 * (i,j) = - (M1 * (k,l)) )
assume that
A3: [i,j] in Indices M1 and
A4: ( k = (n + 1) - j & l = (n + 1) - i ) ; ::_thesis: M1 * (i,j) = - (M1 * (k,l))
 Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24;
then  ( k in Seg n & l in Seg n ) by A3, A4, Lm2;
then A5: [k,l] in [:(Seg n),(Seg n):] by ZFMISC_1:87;
A6: [i,j] in Indices M by A2, A3, MATRIX_1:24;
then (a * M) * (i,j) = a * (M * (i,j)) by MATRIX_3:def_5
.= a * (- (M * (k,l))) by A4, A6, Def2
.= - (a * (M * (k,l))) by VECTSP_1:8
.= - ((a * M) * (k,l)) by A2, A5, MATRIX_3:def_5 ;
hence  M1 * (i,j) = - (M1 * (k,l)) by A1; ::_thesis: verum
end;
end;

registration
let n be Nat;
let K be Field;
let M1, M2 be Anti-subsymmetric Matrix of n,K;
clusterK287(K,M1,M2) ->  Anti-subsymmetric for Matrix of n,K;
coherence
 for b1 being Matrix of n,K st b1 = M1 - M2 holds
b1 is Anti-subsymmetric
proof
 M1 - M2 = M1 + (- M2) ;
hence  for b1 being Matrix of n,K st b1 = M1 - M2 holds
b1 is Anti-subsymmetric ; ::_thesis: verum
end;
end;

registration
let n be Nat;
let K be Field;
let M be Anti-subsymmetric Matrix of n,K;
clusterM @  ->  Anti-subsymmetric for Matrix of n,K;
coherence
 for b1 being Matrix of n,K st b1 = M @ holds
b1 is Anti-subsymmetric
proof
let M1 be Matrix of n,K; ::_thesis: ( M1 = M @ implies M1 is Anti-subsymmetric )
assume A1: M1 = M @ ; ::_thesis: M1 is Anti-subsymmetric
A2: Indices M = [:(Seg n),(Seg n):] by MATRIX_1:24;
let i, j, k, l be Nat; :: according to MATRIX17:def_2 ::_thesis: ( [i,j] in Indices M1 & k = (n + 1) - j & l = (n + 1) - i implies M1 * (i,j) = - (M1 * (k,l)) )
assume that
A3: [i,j] in Indices M1 and
A4: ( k = (n + 1) - j & l = (n + 1) - i ) ; ::_thesis: M1 * (i,j) = - (M1 * (k,l))
 [i,j] in [:(Seg n),(Seg n):] by A3, MATRIX_1:24;
then A5: ( i in Seg n & j in Seg n ) by ZFMISC_1:87;
then A6: [j,i] in [:(Seg n),(Seg n):] by ZFMISC_1:87;
 ( (n + 1) - j in Seg n & (n + 1) - i in Seg n ) by A5, Lm1;
then A7: ( [((n + 1) - i),((n + 1) - j)] in [:(Seg n),(Seg n):] & [((n + 1) - j),((n + 1) - i)] in [:(Seg n),(Seg n):] ) by ZFMISC_1:87;
thus M1 * (i,j) = M * (j,i) by A1, A2, A6, MATRIX_1:def_6
.= - (M * (l,k)) by A4, A6, A2, Def2
.= - (M1 * (k,l)) by A1, A7, A2, A4, MATRIX_1:def_6 ; ::_thesis: verum
end;
end;

begin

definition
let K be Field;
let n be Nat;
let M be Matrix of n,K;
attrM is central_symmetric  means :Def3: :: MATRIX17:def 3
 for i, j, k, l being Nat st [i,j] in Indices M & k = (n + 1) - i & l = (n + 1) - j holds
M * (i,j) = M * (k,l);
end;

:: deftheorem Def3 defines central_symmetric MATRIX17:def_3_:_
 for K being Field
for n being Nat
for M being Matrix of n,K holds
( M is central_symmetric iff for i, j, k, l being Nat st [i,j] in Indices M & k = (n + 1) - i & l = (n + 1) - j holds
M * (i,j) = M * (k,l) );

registration
let n be Nat;
let K be Field;
let a be Element of K;
cluster(n,n) --> a ->  central_symmetric for Matrix of n,K;
coherence
 for b1 being Matrix of n,K st b1 = (n,n) --> a holds
b1 is central_symmetric
proof
let M be Matrix of n,K; ::_thesis: ( M = (n,n) --> a implies M is central_symmetric )
assume A1: M = (n,n) --> a ; ::_thesis: M is central_symmetric
let i, j, k, l be Nat; :: according to MATRIX17:def_3 ::_thesis: ( [i,j] in Indices M & k = (n + 1) - i & l = (n + 1) - j implies M * (i,j) = M * (k,l) )
assume that
A2: [i,j] in Indices M and
A3: ( k = (n + 1) - i & l = (n + 1) - j ) ; ::_thesis: M * (i,j) = M * (k,l)
A4: Indices M = [:(Seg n),(Seg n):] by MATRIX_1:24;
 ( k in Seg n & l in Seg n ) by A3, A2, A4, Lm2;
then  [k,l] in [:(Seg n),(Seg n):] by ZFMISC_1:87;
then  M * (k,l) = a by A1, A4, MATRIX_2:1;
hence  M * (i,j) = M * (k,l) by A1, A2, MATRIX_2:1; ::_thesis: verum
end;
end;

registration
let n be Nat;
let K be Field;
cluster Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular central_symmetric for Matrix of n,n, the carrier of K;
existence
 ex b1 being Matrix of n,K st b1 is central_symmetric
proof
take  (n,n) --> (0. K) ; ::_thesis: (n,n) --> (0. K) is central_symmetric
thus  (n,n) --> (0. K) is central_symmetric ; ::_thesis: verum
end;
end;

registration
let n be Nat;
let K be Field;
let M be central_symmetric Matrix of n,K;
cluster - M ->  central_symmetric for Matrix of n,K;
coherence
 for b1 being Matrix of n,K st b1 = - M holds
b1 is central_symmetric
proof
let N be Matrix of n,K; ::_thesis: ( N = - M implies N is central_symmetric )
assume A1: N = - M ; ::_thesis: N is central_symmetric
A2: Indices M = [:(Seg n),(Seg n):] by MATRIX_1:24;
let i, j, k, l be Nat; :: according to MATRIX17:def_3 ::_thesis: ( [i,j] in Indices N & k = (n + 1) - i & l = (n + 1) - j implies N * (i,j) = N * (k,l) )
assume that
A3: [i,j] in Indices N and
A4: ( k = (n + 1) - i & l = (n + 1) - j ) ; ::_thesis: N * (i,j) = N * (k,l)
A5: Indices (- M) = [:(Seg n),(Seg n):] by MATRIX_1:24;
then  ( i in Seg n & j in Seg n ) by A1, A3, ZFMISC_1:87;
then  ( k in Seg n & l in Seg n ) by A4, Lm1;
then A6: [k,l] in [:(Seg n),(Seg n):] by ZFMISC_1:87;
(- M) * (i,j) = - (M * (i,j)) by A1, A2, A3, A5, MATRIX_3:def_2
.= - (M * (k,l)) by A1, A2, A3, A5, A4, Def3
.= (- M) * (k,l) by A2, A6, MATRIX_3:def_2 ;
hence  N * (i,j) = N * (k,l) by A1; ::_thesis: verum
end;
end;

registration
let n be Nat;
let K be Field;
let M1, M2 be central_symmetric Matrix of n,K;
clusterM1 + M2 ->  central_symmetric for Matrix of n,K;
coherence
 for b1 being Matrix of n,K st b1 = M1 + M2 holds
b1 is central_symmetric
proof
let M be Matrix of n,K; ::_thesis: ( M = M1 + M2 implies M is central_symmetric )
assume A1: M = M1 + M2 ; ::_thesis: M is central_symmetric
let i, j, k, l be Nat; :: according to MATRIX17:def_3 ::_thesis: ( [i,j] in Indices M & k = (n + 1) - i & l = (n + 1) - j implies M * (i,j) = M * (k,l) )
assume that
A2: [i,j] in Indices M and
A3: ( k = (n + 1) - i & l = (n + 1) - j ) ; ::_thesis: M * (i,j) = M * (k,l)
A4: Indices M = [:(Seg n),(Seg n):] by MATRIX_1:24;
 ( (n + 1) - j in Seg n & (n + 1) - i in Seg n ) by A2, A4, Lm2;
then A5: [k,l] in [:(Seg n),(Seg n):] by A3, ZFMISC_1:87;
A6: ( Indices M1 = [:(Seg n),(Seg n):] & Indices M2 = [:(Seg n),(Seg n):] ) by MATRIX_1:24;
(M1 + M2) * (i,j) = (M1 * (i,j)) + (M2 * (i,j)) by A2, A4, A6, MATRIX_3:def_3
.= (M1 * (k,l)) + (M2 * (i,j)) by A2, A4, A6, A3, Def3
.= (M1 * (k,l)) + (M2 * (k,l)) by A2, A4, A6, A3, Def3
.= (M1 + M2) * (k,l) by A6, A5, MATRIX_3:def_3 ;
hence  M * (i,j) = M * (k,l) by A1; ::_thesis: verum
end;
end;

registration
let n be Nat;
let K be Field;
let a be Element of K;
let M be central_symmetric Matrix of n,K;
clustera * M ->  central_symmetric for Matrix of n,K;
coherence
 for b1 being Matrix of n,K st b1 = a * M holds
b1 is central_symmetric
proof
let M1 be Matrix of n,K; ::_thesis: ( M1 = a * M implies M1 is central_symmetric )
assume A1: M1 = a * M ; ::_thesis: M1 is central_symmetric
A2: Indices M = [:(Seg n),(Seg n):] by MATRIX_1:24;
let i, j, k, l be Nat; :: according to MATRIX17:def_3 ::_thesis: ( [i,j] in Indices M1 & k = (n + 1) - i & l = (n + 1) - j implies M1 * (i,j) = M1 * (k,l) )
assume that
A3: [i,j] in Indices M1 and
A4: ( k = (n + 1) - i & l = (n + 1) - j ) ; ::_thesis: M1 * (i,j) = M1 * (k,l)
 Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24;
then  ( k in Seg n & l in Seg n ) by A3, A4, Lm2;
then A5: [k,l] in [:(Seg n),(Seg n):] by ZFMISC_1:87;
A6: [i,j] in Indices M by A2, A3, MATRIX_1:24;
then (a * M) * (i,j) = a * (M * (i,j)) by MATRIX_3:def_5
.= a * (M * (k,l)) by A4, A6, Def3
.= (a * M) * (k,l) by A2, A5, MATRIX_3:def_5 ;
hence  M1 * (i,j) = M1 * (k,l) by A1; ::_thesis: verum
end;
end;

registration
let n be Nat;
let K be Field;
let M1, M2 be central_symmetric Matrix of n,K;
clusterK287(K,M1,M2) ->  central_symmetric for Matrix of n,K;
coherence
 for b1 being Matrix of n,K st b1 = M1 - M2 holds
b1 is central_symmetric
proof
 M1 - M2 = M1 + (- M2) ;
hence  for b1 being Matrix of n,K st b1 = M1 - M2 holds
b1 is central_symmetric ; ::_thesis: verum
end;
end;

registration
let n be Nat;
let K be Field;
let M be central_symmetric Matrix of n,K;
clusterM @  ->  central_symmetric for Matrix of n,K;
coherence
 for b1 being Matrix of n,K st b1 = M @ holds
b1 is central_symmetric
proof
let M1 be Matrix of n,K; ::_thesis: ( M1 = M @ implies M1 is central_symmetric )
assume A1: M1 = M @ ; ::_thesis: M1 is central_symmetric
A2: Indices M = [:(Seg n),(Seg n):] by MATRIX_1:24;
let i, j, k, l be Nat; :: according to MATRIX17:def_3 ::_thesis: ( [i,j] in Indices M1 & k = (n + 1) - i & l = (n + 1) - j implies M1 * (i,j) = M1 * (k,l) )
assume that
A3: [i,j] in Indices M1 and
A4: ( k = (n + 1) - i & l = (n + 1) - j ) ; ::_thesis: M1 * (i,j) = M1 * (k,l)
 [i,j] in [:(Seg n),(Seg n):] by A3, MATRIX_1:24;
then A5: ( i in Seg n & j in Seg n ) by ZFMISC_1:87;
then A6: [j,i] in [:(Seg n),(Seg n):] by ZFMISC_1:87;
 ( (n + 1) - j in Seg n & (n + 1) - i in Seg n ) by A5, Lm1;
then A7: ( [((n + 1) - i),((n + 1) - j)] in [:(Seg n),(Seg n):] & [((n + 1) - j),((n + 1) - i)] in [:(Seg n),(Seg n):] ) by ZFMISC_1:87;
thus M1 * (i,j) = M * (j,i) by A1, A2, A6, MATRIX_1:def_6
.= M * (l,k) by A4, A6, A2, Def3
.= M1 * (k,l) by A1, A7, A2, A4, MATRIX_1:def_6 ; ::_thesis: verum
end;
end;

registration
let n be Nat;
let K be Field;
cluster symmetric subsymmetric  ->  central_symmetric for Matrix of n,n, the carrier of K;
coherence
 for b1 being Matrix of n,K st b1 is symmetric & b1 is subsymmetric holds
b1 is central_symmetric
proof
let M1 be Matrix of n,K; ::_thesis: ( M1 is symmetric & M1 is subsymmetric implies M1 is central_symmetric )
assume that
A1: M1 is symmetric and
A2: M1 is subsymmetric ; ::_thesis: M1 is central_symmetric
A3: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24;
let i, j, k, l be Nat; :: according to MATRIX17:def_3 ::_thesis: ( [i,j] in Indices M1 & k = (n + 1) - i & l = (n + 1) - j implies M1 * (i,j) = M1 * (k,l) )
assume that
A4: [i,j] in Indices M1 and
A5: ( k = (n + 1) - i & l = (n + 1) - j ) ; ::_thesis: M1 * (i,j) = M1 * (k,l)
 ( k in Seg n & l in Seg n ) by A3, A4, A5, Lm2;
then A6: ( [k,l] in [:(Seg n),(Seg n):] & [l,k] in [:(Seg n),(Seg n):] ) by ZFMISC_1:87;
thus M1 * (i,j) = M1 * (l,k) by A2, A4, A5, Def1
.= (M1 @) * (k,l) by A6, A3, MATRIX_1:def_6
.= M1 * (k,l) by A1, MATRIX_6:def_5 ; ::_thesis: verum
end;
end;

begin

Lm3:  for n, i, j being Nat st i in Seg n & j in Seg n & i + j <> n + 1 holds
((i + j) - 1) mod n in Seg n
proof
let n, i, j be Nat; ::_thesis: ( i in Seg n & j in Seg n & i + j <> n + 1 implies ((i + j) - 1) mod n in Seg n )
assume B0: ( i in Seg n & j in Seg n ) ; ::_thesis: ( not i + j <> n + 1 or ((i + j) - 1) mod n in Seg n )
assume  i + j <> n + 1 ; ::_thesis: ((i + j) - 1) mod n in Seg n
percasesthen  ( i + j < n + 1 or i + j > n + 1 ) by XXREAL_0:1;
supposeA4: i + j < n + 1 ; ::_thesis: ((i + j) - 1) mod n in Seg n
 ( 1 <= i & 1 <= j ) by B0, FINSEQ_1:1;
then  1 + 1 <= i + j by XREAL_1:7;
then A5: (1 + 1) - 1 <= (i + j) - 1 by XREAL_1:9;
A6: (i + j) - 1 < (n + 1) - 1 by A4, XREAL_1:9;
A7: ((i + j) - 1) mod n = (i + j) - 1 by A5, A6, NAT_D:63;
 ((i + j) - 1) mod n in NAT by A5, A7, INT_1:3;
hence  ((i + j) - 1) mod n in Seg n by A5, A7, A6; ::_thesis: verum
end;
supposeA10: i + j > n + 1 ; ::_thesis: ((i + j) - 1) mod n in Seg n
 (i + j) - n > (n + 1) - n by A10, XREAL_1:9;
then A11: ((i + j) - n) - 1 > 1 - 1 by XREAL_1:9;
A12: ((i + j) - n) - 1 >= 0 + 1 by A11, INT_1:7;
 ( i <= n & j <= n ) by B0, FINSEQ_1:1;
then  i + j <= n + n by XREAL_1:7;
then  (i + j) - n <= (n + n) - n by XREAL_1:9;
then A13: ((i + j) - n) - 1 <= n - 1 by XREAL_1:9;
 n - 1 < n by XREAL_1:44;
then A14: ((i + j) - n) - 1 < n by A13, XXREAL_0:2;
A15: (((i + j) - n) - 1) mod n = ((i + j) - n) - 1 by A11, A14, NAT_D:63;
A16: (((i + j) - n) - 1) mod n in NAT by A11, A15, INT_1:3;
((i + j) - 1) mod n = ((((i + j) - 1) - n) + n) mod n
.= (((((i + j) - 1) - n) mod n) + (n mod n)) mod n by NAT_D:66
.= ((((i + j) - 1) - n) + 0) mod n by A15, INT_1:50 ;
hence  ((i + j) - 1) mod n in Seg n by A14, A15, A12, A16; ::_thesis: verum
end;
end;
end;

Lm4:  for n, i, j being Nat st [i,j] in [:(Seg n),(Seg n):] & i + j <> n + 1 holds
((i + j) - 1) mod n in Seg n
proof
let n, i, j be Nat; ::_thesis: ( [i,j] in [:(Seg n),(Seg n):] & i + j <> n + 1 implies ((i + j) - 1) mod n in Seg n )
assume that
A1: [i,j] in [:(Seg n),(Seg n):] and
A2: i + j <> n + 1 ; ::_thesis: ((i + j) - 1) mod n in Seg n
 ( i in Seg n & j in Seg n ) by A1, ZFMISC_1:87;
hence  ((i + j) - 1) mod n in Seg n by A2, Lm3; ::_thesis: verum
end;

definition
let K be set ;
let M be Matrix of K;
let p be FinSequence;
predM is_symmetry_circulant_about p means :Def4: :: MATRIX17:def 4
( len p = width M & ( for i, j being Nat st [i,j] in Indices M & i + j <> (len p) + 1 holds
M * (i,j) = p . (((i + j) - 1) mod (len p)) ) & ( for i, j being Nat st [i,j] in Indices M & i + j = (len p) + 1 holds
M * (i,j) = p . (len p) ) );
end;

:: deftheorem Def4 defines is_symmetry_circulant_about MATRIX17:def_4_:_
 for K being set
for M being Matrix of K
for p being FinSequence holds
( M is_symmetry_circulant_about p iff ( len p = width M & ( for i, j being Nat st [i,j] in Indices M & i + j <> (len p) + 1 holds
M * (i,j) = p . (((i + j) - 1) mod (len p)) ) & ( for i, j being Nat st [i,j] in Indices M & i + j = (len p) + 1 holds
M * (i,j) = p . (len p) ) ) );

theorem T1: :: MATRIX17:2
for n being Nat
for K being Field
for a being Element of K holds (n,n) --> a is_symmetry_circulant_about n |-> a
proof
let n be Nat; ::_thesis: for K being Field
for a being Element of K holds (n,n) --> a is_symmetry_circulant_about n |-> a
let K be Field; ::_thesis: for a being Element of K holds (n,n) --> a is_symmetry_circulant_about n |-> a
let a be Element of K; ::_thesis: (n,n) --> a is_symmetry_circulant_about n |-> a
set p = n |-> a;
set M = (n,n) --> a;
A1: ( width ((n,n) --> a) = n & len (n |-> a) = n ) by CARD_1:def_7, MATRIX_1:24;
hence  len (n |-> a) = width ((n,n) --> a) ; :: according to MATRIX17:def_4 ::_thesis: ( ( for i, j being Nat st [i,j] in Indices ((n,n) --> a) & i + j <> (len (n |-> a)) + 1 holds
((n,n) --> a) * (i,j) = (n |-> a) . (((i + j) - 1) mod (len (n |-> a))) ) & ( for i, j being Nat st [i,j] in Indices ((n,n) --> a) & i + j = (len (n |-> a)) + 1 holds
((n,n) --> a) * (i,j) = (n |-> a) . (len (n |-> a)) ) )
A2: Indices ((n,n) --> a) = [:(Seg n),(Seg n):] by MATRIX_1:24;
thus  for i, j being Nat st [i,j] in Indices ((n,n) --> a) & i + j <> (len (n |-> a)) + 1 holds
((n,n) --> a) * (i,j) = (n |-> a) . (((i + j) - 1) mod (len (n |-> a))) ::_thesis: for i, j being Nat st [i,j] in Indices ((n,n) --> a) & i + j = (len (n |-> a)) + 1 holds
((n,n) --> a) * (i,j) = (n |-> a) . (len (n |-> a))
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices ((n,n) --> a) & i + j <> (len (n |-> a)) + 1 implies ((n,n) --> a) * (i,j) = (n |-> a) . (((i + j) - 1) mod (len (n |-> a))) )
assume that
A4: [i,j] in Indices ((n,n) --> a) and
A5: i + j <> (len (n |-> a)) + 1 ; ::_thesis: ((n,n) --> a) * (i,j) = (n |-> a) . (((i + j) - 1) mod (len (n |-> a)))
 ((Seg n) --> a) . (((i + j) - 1) mod (len (n |-> a))) = a by FUNCOP_1:7, A1, A2, A4, A5, Lm4;
hence  ((n,n) --> a) * (i,j) = (n |-> a) . (((i + j) - 1) mod (len (n |-> a))) by A4, MATRIX_2:1; ::_thesis: verum
end;
let i, j be Nat; ::_thesis: ( [i,j] in Indices ((n,n) --> a) & i + j = (len (n |-> a)) + 1 implies ((n,n) --> a) * (i,j) = (n |-> a) . (len (n |-> a)) )
assume that
A6: [i,j] in Indices ((n,n) --> a) and
A7: i + j = (len (n |-> a)) + 1 ; ::_thesis: ((n,n) --> a) * (i,j) = (n |-> a) . (len (n |-> a))
 ( i in Seg n & j in Seg n ) by A2, A6, ZFMISC_1:87;
then  ( 1 <= i & 1 <= j ) by FINSEQ_1:1;
then  1 + 1 <= i + j by XREAL_1:7;
then  ((len (n |-> a)) + 1) - 1 >= (1 + 1) - 1 by A7, XREAL_1:9;
then A8: len (n |-> a) in Seg (len (n |-> a)) ;
 ((Seg n) --> a) . (len (n |-> a)) = a by A1, A8, FUNCOP_1:7;
hence  ((n,n) --> a) * (i,j) = (n |-> a) . (len (n |-> a)) by A6, MATRIX_2:1; ::_thesis: verum
end;

theorem T2: :: MATRIX17:3
for n being Nat
for K being Field
for a being Element of K
for p being FinSequence of K
for M1 being Matrix of n,K st M1 is_symmetry_circulant_about p holds
a * M1 is_symmetry_circulant_about a * p
proof
let n be Nat; ::_thesis: for K being Field
for a being Element of K
for p being FinSequence of K
for M1 being Matrix of n,K st M1 is_symmetry_circulant_about p holds
a * M1 is_symmetry_circulant_about a * p
let K be Field; ::_thesis: for a being Element of K
for p being FinSequence of K
for M1 being Matrix of n,K st M1 is_symmetry_circulant_about p holds
a * M1 is_symmetry_circulant_about a * p
let a be Element of K; ::_thesis: for p being FinSequence of K
for M1 being Matrix of n,K st M1 is_symmetry_circulant_about p holds
a * M1 is_symmetry_circulant_about a * p
let p be FinSequence of K; ::_thesis: for M1 being Matrix of n,K st M1 is_symmetry_circulant_about p holds
a * M1 is_symmetry_circulant_about a * p
let M1 be Matrix of n,K; ::_thesis: ( M1 is_symmetry_circulant_about p implies a * M1 is_symmetry_circulant_about a * p )
assume A3: M1 is_symmetry_circulant_about p ; ::_thesis: a * M1 is_symmetry_circulant_about a * p
then A2: len p = width M1 by Def4;
A1: Indices (a * M1) = [:(Seg n),(Seg n):] by MATRIX_1:24;
A4: width M1 = n by MATRIX_1:24;
then A5: dom p = Seg n by A2, FINSEQ_1:def_3;
A6: dom (a * p) = Seg (len (a * p)) by FINSEQ_1:def_3;
A7: len (a * p) = len p by MATRIXR1:16;
A8: for i, j being Nat st [i,j] in Indices (a * M1) & i + j <> (len (a * p)) + 1 holds
(a * M1) * (i,j) = (a * p) . (((i + j) - 1) mod (len (a * p)))
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * M1) & i + j <> (len (a * p)) + 1 implies (a * M1) * (i,j) = (a * p) . (((i + j) - 1) mod (len (a * p))) )
assume that
A9: [i,j] in Indices (a * M1) and
A10: i + j <> (len (a * p)) + 1 ; ::_thesis: (a * M1) * (i,j) = (a * p) . (((i + j) - 1) mod (len (a * p)))
A11: ((i + j) - 1) mod n in Seg n by A1, A2, A4, A9, A10, A7, Lm4;
A12: [i,j] in Indices M1 by A1, A9, MATRIX_1:24;
then (a * M1) * (i,j) = a * (M1 * (i,j)) by MATRIX_3:def_5
.= (a multfield) . (M1 * (i,j)) by FVSUM_1:49
.= (a multfield) . (p . (((i + j) - 1) mod (len p))) by A3, A12, A10, A7, Def4
.= (a multfield) . (p /. (((i + j) - 1) mod (len p))) by A2, A4, A5, A11, PARTFUN1:def_6
.= a * (p /. (((i + j) - 1) mod (len p))) by FVSUM_1:49
.= (a * p) /. (((i + j) - 1) mod (len p)) by A2, A4, A5, A11, POLYNOM1:def_1
.= (a * p) . (((i + j) - 1) mod (len p)) by A2, A4, A6, A7, A11, PARTFUN1:def_6 ;
hence  (a * M1) * (i,j) = (a * p) . (((i + j) - 1) mod (len (a * p))) by MATRIXR1:16; ::_thesis: verum
end;
A13: for i, j being Nat st [i,j] in Indices (a * M1) & i + j = (len (a * p)) + 1 holds
(a * M1) * (i,j) = (a * p) . (len (a * p))
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * M1) & i + j = (len (a * p)) + 1 implies (a * M1) * (i,j) = (a * p) . (len (a * p)) )
assume that
A14: [i,j] in Indices (a * M1) and
A15: i + j = (len (a * p)) + 1 ; ::_thesis: (a * M1) * (i,j) = (a * p) . (len (a * p))
 ( i in Seg n & j in Seg n ) by A1, A14, ZFMISC_1:87;
then  ( 1 <= i & 1 <= j ) by FINSEQ_1:1;
then  1 + 1 <= i + j by XREAL_1:7;
then A16: ((len (a * p)) + 1) - 1 >= (1 + 1) - 1 by A15, XREAL_1:9;
A17: len (a * p) in Seg (len (a * p)) by A16;
then A18: len p in dom (a * p) by A7, FINSEQ_1:def_3;
A19: len p in dom p by A7, A17, FINSEQ_1:def_3;
A20: [i,j] in Indices M1 by A1, A14, MATRIX_1:24;
then (a * M1) * (i,j) = a * (M1 * (i,j)) by MATRIX_3:def_5
.= (a multfield) . (M1 * (i,j)) by FVSUM_1:49
.= (a multfield) . (p . (len p)) by A3, A20, A15, A7, Def4
.= (a multfield) . (p /. (len p)) by A19, PARTFUN1:def_6
.= a * (p /. (len p)) by FVSUM_1:49
.= (a * p) /. (len p) by A19, POLYNOM1:def_1
.= (a * p) . (len p) by A18, PARTFUN1:def_6 ;
hence  (a * M1) * (i,j) = (a * p) . (len (a * p)) by MATRIXR1:16; ::_thesis: verum
end;
A21: ( width (a * M1) = n & len (a * p) = len p ) by MATRIXR1:16, MATRIX_1:24;
 len p = n by A2, MATRIX_1:24;
hence  a * M1 is_symmetry_circulant_about a * p by A21, A8, A13, Def4; ::_thesis: verum
end;

theorem T4: :: MATRIX17:4
for n being Nat
for K being Field
for p being FinSequence of K
for M1 being Matrix of n,K st M1 is_symmetry_circulant_about p holds
- M1 is_symmetry_circulant_about - p
proof
let n be Nat; ::_thesis: for K being Field
for p being FinSequence of K
for M1 being Matrix of n,K st M1 is_symmetry_circulant_about p holds
- M1 is_symmetry_circulant_about - p
let K be Field; ::_thesis: for p being FinSequence of K
for M1 being Matrix of n,K st M1 is_symmetry_circulant_about p holds
- M1 is_symmetry_circulant_about - p
let p be FinSequence of K; ::_thesis: for M1 being Matrix of n,K st M1 is_symmetry_circulant_about p holds
- M1 is_symmetry_circulant_about - p
let M1 be Matrix of n,K; ::_thesis: ( M1 is_symmetry_circulant_about p implies - M1 is_symmetry_circulant_about - p )
assume A5: M1 is_symmetry_circulant_about p ; ::_thesis: - M1 is_symmetry_circulant_about - p
then A4: len p = width M1 by Def4;
A2: width M1 = n by MATRIX_1:24;
A3: Indices (- M1) = [:(Seg n),(Seg n):] by MATRIX_1:24;
 p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:92;
then A6: - p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:113;
then A7: ( width (- M1) = n & len (- p) = len p ) by CARD_1:def_7, MATRIX_1:24;
A8: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A9: for i, j being Nat st [i,j] in Indices (- M1) & i + j <> (len p) + 1 holds
(- M1) * (i,j) = (- p) . (((i + j) - 1) mod (len (- p)))
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (- M1) & i + j <> (len p) + 1 implies (- M1) * (i,j) = (- p) . (((i + j) - 1) mod (len (- p))) )
assume that
A10: [i,j] in Indices (- M1) and
A11: i + j <> (len p) + 1 ; ::_thesis: (- M1) * (i,j) = (- p) . (((i + j) - 1) mod (len (- p)))
 ((i + j) - 1) mod n in Seg n by A2, A4, A3, A10, A11, Lm4;
then A12: ((i + j) - 1) mod (len p) in dom p by A4, A2, FINSEQ_1:def_3;
(- M1) * (i,j) = - (M1 * (i,j)) by A8, A3, A10, MATRIX_3:def_2
.= (comp K) . (M1 * (i,j)) by VECTSP_1:def_13
.= (comp K) . (p . (((i + j) - 1) mod (len p))) by A5, A8, A3, A10, A11, Def4
.= (- p) . (((i + j) - 1) mod (len p)) by A12, FUNCT_1:13 ;
hence  (- M1) * (i,j) = (- p) . (((i + j) - 1) mod (len (- p))) by A6, CARD_1:def_7; ::_thesis: verum
end;
 for i, j being Nat st [i,j] in Indices (- M1) & i + j = (len p) + 1 holds
(- M1) * (i,j) = (- p) . (len (- p))
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (- M1) & i + j = (len p) + 1 implies (- M1) * (i,j) = (- p) . (len (- p)) )
assume that
A13: [i,j] in Indices (- M1) and
A14: i + j = (len p) + 1 ; ::_thesis: (- M1) * (i,j) = (- p) . (len (- p))
 ( i in Seg n & j in Seg n ) by A3, A13, ZFMISC_1:87;
then  ( 1 <= i & 1 <= j ) by FINSEQ_1:1;
then  1 + 1 <= i + j by XREAL_1:7;
then  ((len p) + 1) - 1 >= (1 + 1) - 1 by A14, XREAL_1:9;
then  len p in Seg (len p) ;
then A15: len p in dom p by FINSEQ_1:def_3;
(- M1) * (i,j) = - (M1 * (i,j)) by A8, A3, A13, MATRIX_3:def_2
.= (comp K) . (M1 * (i,j)) by VECTSP_1:def_13
.= (comp K) . (p . (len p)) by A5, A8, A3, A13, A14, Def4
.= (- p) . (len p) by A15, FUNCT_1:13 ;
hence  (- M1) * (i,j) = (- p) . (len (- p)) by A6, CARD_1:def_7; ::_thesis: verum
end;
hence  - M1 is_symmetry_circulant_about - p by A4, A2, A7, A9, Def4; ::_thesis: verum
end;

theorem T3: :: MATRIX17:5
for n being Nat
for K being Field
for p, q being FinSequence of K
for M1, M2 being Matrix of n,K st M1 is_symmetry_circulant_about p & M2 is_symmetry_circulant_about q holds
M1 + M2 is_symmetry_circulant_about p + q
proof
let n be Nat; ::_thesis: for K being Field
for p, q being FinSequence of K
for M1, M2 being Matrix of n,K st M1 is_symmetry_circulant_about p & M2 is_symmetry_circulant_about q holds
M1 + M2 is_symmetry_circulant_about p + q
let K be Field; ::_thesis: for p, q being FinSequence of K
for M1, M2 being Matrix of n,K st M1 is_symmetry_circulant_about p & M2 is_symmetry_circulant_about q holds
M1 + M2 is_symmetry_circulant_about p + q
let p, q be FinSequence of K; ::_thesis: for M1, M2 being Matrix of n,K st M1 is_symmetry_circulant_about p & M2 is_symmetry_circulant_about q holds
M1 + M2 is_symmetry_circulant_about p + q
let M1, M2 be Matrix of n,K; ::_thesis: ( M1 is_symmetry_circulant_about p & M2 is_symmetry_circulant_about q implies M1 + M2 is_symmetry_circulant_about p + q )
assume A3: M1 is_symmetry_circulant_about p ; ::_thesis: ( not M2 is_symmetry_circulant_about q or M1 + M2 is_symmetry_circulant_about p + q )
A2: len p = width M1 by A3, Def4;
A4: Indices M2 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A5: Indices (M1 + M2) = [:(Seg n),(Seg n):] by MATRIX_1:24;
A6: width M1 = n by MATRIX_1:24;
then A7: dom p = Seg n by A2, FINSEQ_1:def_3;
assume A9: M2 is_symmetry_circulant_about q ; ::_thesis: M1 + M2 is_symmetry_circulant_about p + q
then A8: len q = width M2 by Def4;
A10: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A11: n in NAT by ORDINAL1:def_12;
A12: width M2 = n by MATRIX_1:24;
then  dom q = Seg n by A8, FINSEQ_1:def_3;
then A13: dom (p + q) = dom p by A7, POLYNOM1:1;
then A14: len (p + q) = n by A7, A11, FINSEQ_1:def_3;
A15: width (M1 + M2) = n by MATRIX_1:24;
A16: dom (p + q) = Seg (len (p + q)) by FINSEQ_1:def_3;
A17: for i, j being Nat st [i,j] in Indices (M1 + M2) & i + j <> (len (p + q)) + 1 holds
(M1 + M2) * (i,j) = (p + q) . (((i + j) - 1) mod (len (p + q)))
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 + M2) & i + j <> (len (p + q)) + 1 implies (M1 + M2) * (i,j) = (p + q) . (((i + j) - 1) mod (len (p + q))) )
assume that
A18: [i,j] in Indices (M1 + M2) and
A19: i + j <> (len (p + q)) + 1 ; ::_thesis: (M1 + M2) * (i,j) = (p + q) . (((i + j) - 1) mod (len (p + q)))
A20: ((i + j) - 1) mod (len (p + q)) in dom (p + q) by A5, A16, A19, A18, A13, A7, Lm4;
(M1 + M2) * (i,j) = (M1 * (i,j)) + (M2 * (i,j)) by A10, A5, A18, MATRIX_3:def_3
.= the addF of K . ((M1 * (i,j)),(q . (((i + j) - 1) mod (len (p + q))))) by A9, A4, A5, A8, A12, A18, A19, A14, Def4
.= the addF of K . ((p . (((i + j) - 1) mod (len (p + q)))),(q . (((i + j) - 1) mod (len (p + q))))) by A3, A2, A6, A10, A5, A14, A18, A19, Def4
.= (p + q) . (((i + j) - 1) mod (len (p + q))) by A20, FUNCOP_1:22 ;
hence  (M1 + M2) * (i,j) = (p + q) . (((i + j) - 1) mod (len (p + q))) ; ::_thesis: verum
end;
 for i, j being Nat st [i,j] in Indices (M1 + M2) & i + j = (len (p + q)) + 1 holds
(M1 + M2) * (i,j) = (p + q) . (len (p + q))
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 + M2) & i + j = (len (p + q)) + 1 implies (M1 + M2) * (i,j) = (p + q) . (len (p + q)) )
assume that
A21: [i,j] in Indices (M1 + M2) and
A22: i + j = (len (p + q)) + 1 ; ::_thesis: (M1 + M2) * (i,j) = (p + q) . (len (p + q))
 ( i in Seg n & j in Seg n ) by A5, A21, ZFMISC_1:87;
then  ( 1 <= i & 1 <= j ) by FINSEQ_1:1;
then  1 + 1 <= i + j by XREAL_1:7;
then  ((len (p + q)) + 1) - 1 >= (1 + 1) - 1 by A22, XREAL_1:9;
then  len (p + q) in Seg (len (p + q)) ;
then A23: len (p + q) in dom (p + q) by FINSEQ_1:def_3;
(M1 + M2) * (i,j) = (M1 * (i,j)) + (M2 * (i,j)) by A10, A5, A21, MATRIX_3:def_3
.= the addF of K . ((M1 * (i,j)),(q . (len (p + q)))) by A9, A8, A12, A14, A4, A5, A21, A22, Def4
.= the addF of K . ((p . (len (p + q))),(q . (len (p + q)))) by A2, A3, A10, A6, A5, A14, A21, A22, Def4
.= (p + q) . (len (p + q)) by A23, FUNCOP_1:22 ;
hence  (M1 + M2) * (i,j) = (p + q) . (len (p + q)) ; ::_thesis: verum
end;
hence  M1 + M2 is_symmetry_circulant_about p + q by A15, A14, A17, Def4; ::_thesis: verum
end;

definition
let K be set ;
let M be Matrix of K;
attrM is symmetry_circulant  means :Def5: :: MATRIX17:def 5
 ex p being FinSequence of K st
( len p = width M & M is_symmetry_circulant_about p );
end;

:: deftheorem Def5 defines symmetry_circulant MATRIX17:def_5_:_
 for K being set
for M being Matrix of K holds
( M is symmetry_circulant iff ex p being FinSequence of K st
( len p = width M & M is_symmetry_circulant_about p ) );

definition
let K be non empty set ;
let p be FinSequence of K;
attrp is first-symmetry-of-circulant  means :Def6: :: MATRIX17:def 6
 ex M being Matrix of len p,K st M is_symmetry_circulant_about p;
end;

:: deftheorem Def6 defines first-symmetry-of-circulant MATRIX17:def_6_:_
 for K being non empty set
for p being FinSequence of K holds
( p is first-symmetry-of-circulant iff ex M being Matrix of len p,K st M is_symmetry_circulant_about p );

definition
let K be non empty set ;
let p be FinSequence of K;
assume A1: p is first-symmetry-of-circulant ;
func SCirc p ->  Matrix of len p,K means :Def7: :: MATRIX17:def 7
it is_symmetry_circulant_about p;
existence
 ex b1 being Matrix of len p,K st b1 is_symmetry_circulant_about p by A1, Def6;
uniqueness
 for b1, b2 being Matrix of len p,K st b1 is_symmetry_circulant_about p & b2 is_symmetry_circulant_about p holds
b1 = b2
proof
let M1, M2 be Matrix of len p,K; ::_thesis: ( M1 is_symmetry_circulant_about p & M2 is_symmetry_circulant_about p implies M1 = M2 )
assume that
A2: M1 is_symmetry_circulant_about p and
A3: M2 is_symmetry_circulant_about p ; ::_thesis: M1 = M2
A4: Indices M1 = Indices M2 by MATRIX_1:26;
 for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) = M2 * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices M1 implies M1 * (i,j) = M2 * (i,j) )
assume A5: [i,j] in Indices M1 ; ::_thesis: M1 * (i,j) = M2 * (i,j)
percases ( i + j <> (len p) + 1 or i + j = (len p) + 1 ) ;
supposeA6: i + j <> (len p) + 1 ; ::_thesis: M1 * (i,j) = M2 * (i,j)
then  M1 * (i,j) = p . (((i + j) - 1) mod (len p)) by A5, A2, Def4;
hence  M1 * (i,j) = M2 * (i,j) by A3, A4, A5, A6, Def4; ::_thesis: verum
end;
supposeA7: i + j = (len p) + 1 ; ::_thesis: M1 * (i,j) = M2 * (i,j)
then  M1 * (i,j) = p . (len p) by A2, A5, Def4;
hence  M1 * (i,j) = M2 * (i,j) by A3, A4, A5, A7, Def4; ::_thesis: verum
end;
end;
end;
hence  M1 = M2 by MATRIX_1:27; ::_thesis: verum
end;
end;

:: deftheorem Def7 defines SCirc MATRIX17:def_7_:_
 for K being non empty set
for p being FinSequence of K st p is first-symmetry-of-circulant holds
for b3 being Matrix of len p,K holds
( b3 = SCirc p iff b3 is_symmetry_circulant_about p );

registration
let n be Nat;
let K be Field;
let a be Element of K;
cluster(n,n) --> a ->  symmetry_circulant for Matrix of n,K;
coherence
 for b1 being Matrix of n,K st b1 = (n,n) --> a holds
b1 is symmetry_circulant
proof
set p = n |-> a;
A1: ( width ((n,n) --> a) = n & len (n |-> a) = n ) by CARD_1:def_7, MATRIX_1:24;
 (n,n) --> a is_symmetry_circulant_about n |-> a by T1;
hence  for b1 being Matrix of n,K st b1 = (n,n) --> a holds
b1 is symmetry_circulant by A1, Def5; ::_thesis: verum
end;
end;

registration
let n be Nat;
let K be Field;
cluster Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular symmetry_circulant for Matrix of n,n, the carrier of K;
existence
 ex b1 being Matrix of n,K st b1 is symmetry_circulant
proof
take  (n,n) --> (0. K) ; ::_thesis: (n,n) --> (0. K) is symmetry_circulant
thus  (n,n) --> (0. K) is symmetry_circulant ; ::_thesis: verum
end;
end;


theorem T5: :: MATRIX17:6
for n being Nat
for D being non empty set
for A being Matrix of n,D
for p being FinSequence of D st 0 < n & A is_symmetry_circulant_about p holds
A @ is_symmetry_circulant_about p
proof
let n be Nat; ::_thesis: for D being non empty set
for A being Matrix of n,D
for p being FinSequence of D st 0 < n & A is_symmetry_circulant_about p holds
A @ is_symmetry_circulant_about p
let D be non empty set ; ::_thesis: for A being Matrix of n,D
for p being FinSequence of D st 0 < n & A is_symmetry_circulant_about p holds
A @ is_symmetry_circulant_about p
let A be Matrix of n,D; ::_thesis: for p being FinSequence of D st 0 < n & A is_symmetry_circulant_about p holds
A @ is_symmetry_circulant_about p
let p be FinSequence of D; ::_thesis: ( 0 < n & A is_symmetry_circulant_about p implies A @ is_symmetry_circulant_about p )
assume that
A2: 0 < n and
A4: A is_symmetry_circulant_about p ; ::_thesis: A @ is_symmetry_circulant_about p
A3: len p = width A by A4, Def4;
 ( width A = n & len A = n ) by MATRIX_1:24;
then A5: width (A @) = len p by A2, A3, MATRIX_2:10;
A6: for i, j being Nat st [i,j] in Indices (A @) & i + j <> (len p) + 1 holds
(A @) * (i,j) = p . (((i + j) - 1) mod (len p))
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (A @) & i + j <> (len p) + 1 implies (A @) * (i,j) = p . (((i + j) - 1) mod (len p)) )
A7: Indices A = [:(Seg n),(Seg n):] by MATRIX_1:24;
assume that
A8: [i,j] in Indices (A @) and
A9: i + j <> (len p) + 1 ; ::_thesis: (A @) * (i,j) = p . (((i + j) - 1) mod (len p))
 [i,j] in Indices A by A8, MATRIX_1:26;
then  ( i in Seg n & j in Seg n ) by A7, ZFMISC_1:87;
then A10: [j,i] in Indices A by A7, ZFMISC_1:87;
then  (A @) * (i,j) = A * (j,i) by MATRIX_1:def_6;
hence  (A @) * (i,j) = p . (((i + j) - 1) mod (len p)) by A4, A10, A9, Def4; ::_thesis: verum
end;
 for i, j being Nat st [i,j] in Indices (A @) & i + j = (len p) + 1 holds
(A @) * (i,j) = p . (len p)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (A @) & i + j = (len p) + 1 implies (A @) * (i,j) = p . (len p) )
A11: Indices A = [:(Seg n),(Seg n):] by MATRIX_1:24;
assume that
A12: [i,j] in Indices (A @) and
A13: i + j = (len p) + 1 ; ::_thesis: (A @) * (i,j) = p . (len p)
 [i,j] in Indices A by A12, MATRIX_1:26;
then  ( i in Seg n & j in Seg n ) by A11, ZFMISC_1:87;
then A14: [j,i] in Indices A by A11, ZFMISC_1:87;
then  (A @) * (i,j) = A * (j,i) by MATRIX_1:def_6;
hence  (A @) * (i,j) = p . (len p) by A4, A13, A14, Def4; ::_thesis: verum
end;
hence  A @ is_symmetry_circulant_about p by A5, A6, Def4; ::_thesis: verum
end;

registration
let n be Nat;
let K be Field;
let a be Element of K;
let M1 be symmetry_circulant Matrix of n,K;
clustera * M1 ->  symmetry_circulant for Matrix of n,K;
coherence
 for b1 being Matrix of n,K st b1 = a * M1 holds
b1 is symmetry_circulant
proof
consider p being FinSequence of K such that
A2: len p = width M1 and
A3: M1 is_symmetry_circulant_about p by Def5;
A4: ( width (a * M1) = n & len (a * p) = len p ) by MATRIXR1:16, MATRIX_1:24;
 a * M1 is_symmetry_circulant_about a * p by A3, T2;
then  ex q being FinSequence of K st
( len q = width (a * M1) & a * M1 is_symmetry_circulant_about q ) by A2, A4, MATRIX_1:24;
hence  for b1 being Matrix of n,K st b1 = a * M1 holds
b1 is symmetry_circulant by Def5; ::_thesis: verum
end;
end;

registration
let n be Nat;
let K be Field;
let M1, M2 be symmetry_circulant Matrix of n,K;
clusterM1 + M2 ->  symmetry_circulant for Matrix of n,K;
coherence
 for b1 being Matrix of n,K st b1 = M1 + M2 holds
b1 is symmetry_circulant
proof
let M be Matrix of n,K; ::_thesis: ( M = M1 + M2 implies M is symmetry_circulant )
assume A1: M = M1 + M2 ; ::_thesis: M is symmetry_circulant
consider p being FinSequence of K such that
A2: len p = width M1 and
A3: M1 is_symmetry_circulant_about p by Def5;
 width M1 = n by MATRIX_1:24;
then A7: dom p = Seg n by A2, FINSEQ_1:def_3;
consider q being FinSequence of K such that
A8: len q = width M2 and
A9: M2 is_symmetry_circulant_about q by Def5;
A11: n in NAT by ORDINAL1:def_12;
 width M2 = n by MATRIX_1:24;
then  dom q = Seg n by A8, FINSEQ_1:def_3;
then  dom (p + q) = dom p by A7, POLYNOM1:1;
then A14: len (p + q) = n by A7, A11, FINSEQ_1:def_3;
 width (M1 + M2) = n by MATRIX_1:24;
then  ex r being FinSequence of K st
( len r = width (M1 + M2) & M1 + M2 is_symmetry_circulant_about r ) by A14, A3, A9, T3;
hence  M is symmetry_circulant by A1, Def5; ::_thesis: verum
end;
end;

registration
let n be Nat;
let K be Field;
let M1 be symmetry_circulant Matrix of n,K;
cluster - M1 ->  symmetry_circulant for Matrix of n,K;
coherence
 for b1 being Matrix of n,K st b1 = - M1 holds
b1 is symmetry_circulant
proof
let N be Matrix of n,K; ::_thesis: ( N = - M1 implies N is symmetry_circulant )
assume A1: N = - M1 ; ::_thesis: N is symmetry_circulant
consider p being FinSequence of K such that
A4: len p = width M1 and
A5: M1 is_symmetry_circulant_about p by Def5;
 p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:92;
then  - p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:113;
then A7: ( width (- M1) = n & len (- p) = len p ) by CARD_1:def_7, MATRIX_1:24;
 - M1 is_symmetry_circulant_about - p by A5, T4;
then  ex r being FinSequence of K st
( len r = width (- M1) & - M1 is_symmetry_circulant_about r ) by A4, A7, MATRIX_1:24;
hence  N is symmetry_circulant by A1, Def5; ::_thesis: verum
end;
end;

registration
let n be Nat;
let K be Field;
let M1, M2 be symmetry_circulant Matrix of n,K;
clusterK287(K,M1,M2) ->  symmetry_circulant for Matrix of n,K;
coherence
 for b1 being Matrix of n,K st b1 = M1 - M2 holds
b1 is symmetry_circulant
proof
 M1 - M2 = M1 + (- M2) ;
hence  for b1 being Matrix of n,K st b1 = M1 - M2 holds
b1 is symmetry_circulant ; ::_thesis: verum
end;
end;

theorem :: MATRIX17:7
for n being Nat
for D being non empty set
for A being Matrix of n,D st A is symmetry_circulant & n > 0 holds
A @ is symmetry_circulant
proof
let n be Nat; ::_thesis: for D being non empty set
for A being Matrix of n,D st A is symmetry_circulant & n > 0 holds
A @ is symmetry_circulant
let D be non empty set ; ::_thesis: for A being Matrix of n,D st A is symmetry_circulant & n > 0 holds
A @ is symmetry_circulant
let A be Matrix of n,D; ::_thesis: ( A is symmetry_circulant & n > 0 implies A @ is symmetry_circulant )
assume that
A1: A is symmetry_circulant and
A2: n > 0 ; ::_thesis: A @ is symmetry_circulant
consider p being FinSequence of D such that
A3: len p = width A and
A4: A is_symmetry_circulant_about p by A1, Def5;
 ( width A = n & len A = n ) by MATRIX_1:24;
then  width (A @) = len p by A2, A3, MATRIX_2:10;
then consider p being FinSequence of D such that
A15: ( len p = width (A @) & A @ is_symmetry_circulant_about p ) by A2, A4, T5;
take  p ; :: according to MATRIX17:def_5 ::_thesis: ( len p = width (A @) & A @ is_symmetry_circulant_about p )
thus  ( len p = width (A @) & A @ is_symmetry_circulant_about p ) by A15; ::_thesis: verum
end;

theorem Th4: :: MATRIX17:8
for K being Field
for p being FinSequence of K st p is first-symmetry-of-circulant holds
- p is first-symmetry-of-circulant
proof
let K be Field; ::_thesis: for p being FinSequence of K st p is first-symmetry-of-circulant holds
- p is first-symmetry-of-circulant
let p be FinSequence of K; ::_thesis: ( p is first-symmetry-of-circulant implies - p is first-symmetry-of-circulant )
set n = len p;
assume  p is first-symmetry-of-circulant ; ::_thesis: - p is first-symmetry-of-circulant
then consider M1 being Matrix of len p,K such that
A1: M1 is_symmetry_circulant_about p by Def6;
 p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:92;
then  - p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:113;
then A5: len (- p) = len p by CARD_1:def_7;
 - M1 is_symmetry_circulant_about - p by A1, T4;
then consider M2 being Matrix of len (- p),K such that
A15: M2 is_symmetry_circulant_about - p by A5;
take  M2 ; :: according to MATRIX17:def_6 ::_thesis: M2 is_symmetry_circulant_about - p
thus  M2 is_symmetry_circulant_about - p by A15; ::_thesis: verum
end;

theorem :: MATRIX17:9
for K being Field
for p being FinSequence of K st p is first-symmetry-of-circulant holds
SCirc (- p) = - (SCirc p)
proof
let K be Field; ::_thesis: for p being FinSequence of K st p is first-symmetry-of-circulant holds
SCirc (- p) = - (SCirc p)
let p be FinSequence of K; ::_thesis: ( p is first-symmetry-of-circulant implies SCirc (- p) = - (SCirc p) )
set n = len p;
A1: ( len (SCirc p) = len p & width (SCirc p) = len p ) by MATRIX_1:24;
A2: Indices (SCirc p) = [:(Seg (len p)),(Seg (len p)):] by MATRIX_1:24;
 p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:92;
then  - p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:113;
then A3: len (- p) = len p by CARD_1:def_7;
assume A4: p is first-symmetry-of-circulant ; ::_thesis: SCirc (- p) = - (SCirc p)
then  - p is first-symmetry-of-circulant by Th4;
then A5: SCirc (- p) is_symmetry_circulant_about - p by Def7;
A6: SCirc p is_symmetry_circulant_about p by A4, Def7;
A7: for i, j being Nat st [i,j] in Indices (SCirc p) holds
(SCirc (- p)) * (i,j) = - ((SCirc p) * (i,j))
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (SCirc p) implies (SCirc (- p)) * (i,j) = - ((SCirc p) * (i,j)) )
assume A8: [i,j] in Indices (SCirc p) ; ::_thesis: (SCirc (- p)) * (i,j) = - ((SCirc p) * (i,j))
now__::_thesis:_(SCirc_(-_p))_*_(i,j)_=_-_((SCirc_p)_*_(i,j))
percases ( i + j <> (len p) + 1 or i + j = (len p) + 1 ) ;
supposeA9: i + j <> (len p) + 1 ; ::_thesis: (SCirc (- p)) * (i,j) = - ((SCirc p) * (i,j))
 ((i + j) - 1) mod (len p) in Seg (len p) by A2, A8, A9, Lm4;
then A10: ((i + j) - 1) mod (len p) in dom p by FINSEQ_1:def_3;
 [i,j] in Indices (SCirc (- p)) by A3, A8, MATRIX_1:26;
then (SCirc (- p)) * (i,j) = (- p) . (((i + j) - 1) mod (len (- p))) by A5, A9, A3, Def4
.= (comp K) . (p . (((i + j) - 1) mod (len p))) by A3, A10, FUNCT_1:13
.= (comp K) . ((SCirc p) * (i,j)) by A6, A8, A9, Def4
.= - ((SCirc p) * (i,j)) by VECTSP_1:def_13 ;
hence  (SCirc (- p)) * (i,j) = - ((SCirc p) * (i,j)) ; ::_thesis: verum
end;
supposeA11: i + j = (len p) + 1 ; ::_thesis: (SCirc (- p)) * (i,j) = - ((SCirc p) * (i,j))
 ( i in Seg (len p) & j in Seg (len p) ) by A2, A8, ZFMISC_1:87;
then  ( 1 <= i & 1 <= j ) by FINSEQ_1:1;
then  1 + 1 <= i + j by XREAL_1:7;
then  ((len p) + 1) - 1 >= (1 + 1) - 1 by A11, XREAL_1:9;
then  len p in Seg (len p) ;
then A13: len p in dom p by FINSEQ_1:def_3;
 [i,j] in Indices (SCirc (- p)) by A3, A8, MATRIX_1:26;
then (SCirc (- p)) * (i,j) = (- p) . (len (- p)) by A5, A11, A3, Def4
.= (comp K) . (p . (len p)) by A3, A13, FUNCT_1:13
.= (comp K) . ((SCirc p) * (i,j)) by A6, A8, A11, Def4
.= - ((SCirc p) * (i,j)) by VECTSP_1:def_13 ;
hence  (SCirc (- p)) * (i,j) = - ((SCirc p) * (i,j)) ; ::_thesis: verum
end;
end;
end;
hence  (SCirc (- p)) * (i,j) = - ((SCirc p) * (i,j)) ; ::_thesis: verum
end;
 ( len (SCirc (- p)) = len p & width (SCirc (- p)) = len p ) by A3, MATRIX_1:24;
hence  SCirc (- p) = - (SCirc p) by A1, A7, MATRIX_3:def_2; ::_thesis: verum
end;

theorem Th6: :: MATRIX17:10
for K being Field
for p, q being FinSequence of K st p is first-symmetry-of-circulant & q is first-symmetry-of-circulant & len p = len q holds
p + q is first-symmetry-of-circulant
proof
let K be Field; ::_thesis: for p, q being FinSequence of K st p is first-symmetry-of-circulant & q is first-symmetry-of-circulant & len p = len q holds
p + q is first-symmetry-of-circulant
let p, q be FinSequence of K; ::_thesis: ( p is first-symmetry-of-circulant & q is first-symmetry-of-circulant & len p = len q implies p + q is first-symmetry-of-circulant )
set n = len p;
assume that
A1: p is first-symmetry-of-circulant and
A2: q is first-symmetry-of-circulant and
A3: len p = len q ; ::_thesis: p + q is first-symmetry-of-circulant
consider M2 being Matrix of len p,K such that
A4: M2 is_symmetry_circulant_about q by A2, A3, Def6;
A5: dom p = Seg (len p) by FINSEQ_1:def_3;
 dom q = Seg (len p) by A3, FINSEQ_1:def_3;
then  dom (p + q) = dom p by A5, POLYNOM1:1;
then A7: len (p + q) = len p by A5, FINSEQ_1:def_3;
consider M1 being Matrix of len p,K such that
A8: M1 is_symmetry_circulant_about p by A1, Def6;
 width (M1 + M2) = len p by MATRIX_1:24;
then consider M3 being Matrix of len (p + q),K such that
 len (p + q) = width M3 and
A23: M3 is_symmetry_circulant_about p + q by A7, A4, A8, T3;
take  M3 ; :: according to MATRIX17:def_6 ::_thesis: M3 is_symmetry_circulant_about p + q
thus  M3 is_symmetry_circulant_about p + q by A23; ::_thesis: verum
end;

theorem Th7: :: MATRIX17:11
for K being Field
for p, q being FinSequence of K st len p = len q & p is first-symmetry-of-circulant & q is first-symmetry-of-circulant holds
SCirc (p + q) = (SCirc p) + (SCirc q)
proof
let K be Field; ::_thesis: for p, q being FinSequence of K st len p = len q & p is first-symmetry-of-circulant & q is first-symmetry-of-circulant holds
SCirc (p + q) = (SCirc p) + (SCirc q)
let p, q be FinSequence of K; ::_thesis: ( len p = len q & p is first-symmetry-of-circulant & q is first-symmetry-of-circulant implies SCirc (p + q) = (SCirc p) + (SCirc q) )
set n = len p;
assume that
A1: len p = len q and
A2: p is first-symmetry-of-circulant and
A3: q is first-symmetry-of-circulant ; ::_thesis: SCirc (p + q) = (SCirc p) + (SCirc q)
A4: ( SCirc q is_symmetry_circulant_about q & Indices (SCirc p) = Indices (SCirc q) ) by A1, A3, Def7, MATRIX_1:26;
 p + q is first-symmetry-of-circulant by A1, A2, A3, Th6;
then A5: SCirc (p + q) is_symmetry_circulant_about p + q by Def7;
A6: dom p = Seg (len p) by FINSEQ_1:def_3;
A7: SCirc p is_symmetry_circulant_about p by A2, Def7;
A8: dom (p + q) = Seg (len (p + q)) by FINSEQ_1:def_3;
A9: Indices (SCirc p) = [:(Seg (len p)),(Seg (len p)):] by MATRIX_1:24;
 dom q = Seg (len p) by A1, FINSEQ_1:def_3;
then  dom (p + q) = dom p by A6, POLYNOM1:1;
then A10: len (p + q) = len p by A6, FINSEQ_1:def_3;
then A11: Indices (SCirc p) = Indices (SCirc (p + q)) by MATRIX_1:26;
A12: for i, j being Nat st [i,j] in Indices (SCirc p) holds
(SCirc (p + q)) * (i,j) = ((SCirc p) * (i,j)) + ((SCirc q) * (i,j))
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (SCirc p) implies (SCirc (p + q)) * (i,j) = ((SCirc p) * (i,j)) + ((SCirc q) * (i,j)) )
assume A13: [i,j] in Indices (SCirc p) ; ::_thesis: (SCirc (p + q)) * (i,j) = ((SCirc p) * (i,j)) + ((SCirc q) * (i,j))
now__::_thesis:_(SCirc_(p_+_q))_*_(i,j)_=_((SCirc_p)_*_(i,j))_+_((SCirc_q)_*_(i,j))
percases ( i + j <> (len (p + q)) + 1 or i + j = (len (p + q)) + 1 ) ;
supposeA14: i + j <> (len (p + q)) + 1 ; ::_thesis: (SCirc (p + q)) * (i,j) = ((SCirc p) * (i,j)) + ((SCirc q) * (i,j))
A15: ((i + j) - 1) mod (len p) in Seg (len p) by A9, A13, A14, A10, Lm4;
(SCirc (p + q)) * (i,j) = (p + q) . (((i + j) - 1) mod (len (p + q))) by A5, A11, A13, A14, Def4
.= the addF of K . ((p . (((i + j) - 1) mod (len (p + q)))),(q . (((i + j) - 1) mod (len (p + q))))) by A8, A10, A15, FUNCOP_1:22
.= the addF of K . (((SCirc p) * (i,j)),(q . (((i + j) - 1) mod (len q)))) by A1, A10, A7, A13, A14, Def4
.= ((SCirc p) * (i,j)) + ((SCirc q) * (i,j)) by A1, A4, A13, A14, A10, Def4 ;
hence  (SCirc (p + q)) * (i,j) = ((SCirc p) * (i,j)) + ((SCirc q) * (i,j)) ; ::_thesis: verum
end;
supposeA16: i + j = (len (p + q)) + 1 ; ::_thesis: (SCirc (p + q)) * (i,j) = ((SCirc p) * (i,j)) + ((SCirc q) * (i,j))
 ( i in Seg (len p) & j in Seg (len p) ) by A9, A13, ZFMISC_1:87;
then  ( 1 <= i & 1 <= j ) by FINSEQ_1:1;
then  1 + 1 <= i + j by XREAL_1:7;
then  ((len (p + q)) + 1) - 1 >= (1 + 1) - 1 by A16, XREAL_1:9;
then  len (p + q) in Seg (len (p + q)) ;
then A17: len (p + q) in dom (p + q) by FINSEQ_1:def_3;
(SCirc (p + q)) * (i,j) = (p + q) . (len (p + q)) by A5, A11, A13, A16, Def4
.= the addF of K . ((p . (len (p + q))),(q . (len (p + q)))) by A17, FUNCOP_1:22
.= the addF of K . (((SCirc p) * (i,j)),(q . (len q))) by A1, A10, A7, A13, A16, Def4
.= ((SCirc p) * (i,j)) + ((SCirc q) * (i,j)) by A4, A13, A16, A1, A10, Def4 ;
hence  (SCirc (p + q)) * (i,j) = ((SCirc p) * (i,j)) + ((SCirc q) * (i,j)) ; ::_thesis: verum
end;
end;
end;
hence  (SCirc (p + q)) * (i,j) = ((SCirc p) * (i,j)) + ((SCirc q) * (i,j)) ; ::_thesis: verum
end;
A18: ( len (SCirc p) = len p & width (SCirc p) = len p ) by MATRIX_1:24;
 ( len (SCirc (p + q)) = len p & width (SCirc (p + q)) = len p ) by A10, MATRIX_1:24;
hence  SCirc (p + q) = (SCirc p) + (SCirc q) by A18, A12, MATRIX_3:def_3; ::_thesis: verum
end;

theorem Th8: :: MATRIX17:12
for K being Field
for a being Element of K
for p being FinSequence of K st p is first-symmetry-of-circulant holds
a * p is first-symmetry-of-circulant
proof
let K be Field; ::_thesis: for a being Element of K
for p being FinSequence of K st p is first-symmetry-of-circulant holds
a * p is first-symmetry-of-circulant
let a be Element of K; ::_thesis: for p being FinSequence of K st p is first-symmetry-of-circulant holds
a * p is first-symmetry-of-circulant
let p be FinSequence of K; ::_thesis: ( p is first-symmetry-of-circulant implies a * p is first-symmetry-of-circulant )
set n = len p;
A1: len (a * p) = len p by MATRIXR1:16;
assume  p is first-symmetry-of-circulant ; ::_thesis: a * p is first-symmetry-of-circulant
then consider M1 being Matrix of len p,K such that
A2: M1 is_symmetry_circulant_about p by Def6;
 a * M1 is_symmetry_circulant_about a * p by A2, T2;
then consider M2 being Matrix of len (a * p),K such that
A19: M2 is_symmetry_circulant_about a * p by A1;
take  M2 ; :: according to MATRIX17:def_6 ::_thesis: M2 is_symmetry_circulant_about a * p
thus  M2 is_symmetry_circulant_about a * p by A19; ::_thesis: verum
end;

theorem Th9: :: MATRIX17:13
for K being Field
for a being Element of K
for p being FinSequence of K st p is first-symmetry-of-circulant holds
SCirc (a * p) = a * (SCirc p)
proof
let K be Field; ::_thesis: for a being Element of K
for p being FinSequence of K st p is first-symmetry-of-circulant holds
SCirc (a * p) = a * (SCirc p)
let a be Element of K; ::_thesis: for p being FinSequence of K st p is first-symmetry-of-circulant holds
SCirc (a * p) = a * (SCirc p)
let p be FinSequence of K; ::_thesis: ( p is first-symmetry-of-circulant implies SCirc (a * p) = a * (SCirc p) )
set n = len p;
A1: len (a * p) = len p by MATRIXR1:16;
assume A2: p is first-symmetry-of-circulant ; ::_thesis: SCirc (a * p) = a * (SCirc p)
then  a * p is first-symmetry-of-circulant by Th8;
then A3: SCirc (a * p) is_symmetry_circulant_about a * p by Def7;
A4: Indices (SCirc p) = [:(Seg (len p)),(Seg (len p)):] by MATRIX_1:24;
A5: SCirc p is_symmetry_circulant_about p by A2, Def7;
A6: for i, j being Nat st [i,j] in Indices (SCirc p) holds
(SCirc (a * p)) * (i,j) = a * ((SCirc p) * (i,j))
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (SCirc p) implies (SCirc (a * p)) * (i,j) = a * ((SCirc p) * (i,j)) )
A7: dom (a * p) = Seg (len (a * p)) by FINSEQ_1:def_3;
assume A8: [i,j] in Indices (SCirc p) ; ::_thesis: (SCirc (a * p)) * (i,j) = a * ((SCirc p) * (i,j))
now__::_thesis:_(SCirc_(a_*_p))_*_(i,j)_=_a_*_((SCirc_p)_*_(i,j))
percases ( i + j <> (len p) + 1 or i + j = (len p) + 1 ) ;
supposeA9: i + j <> (len p) + 1 ; ::_thesis: (SCirc (a * p)) * (i,j) = a * ((SCirc p) * (i,j))
A10: ((i + j) - 1) mod (len p) in Seg (len p) by A4, A8, A9, Lm4;
A11: dom p = Seg (len p) by FINSEQ_1:def_3;
 [i,j] in Indices (SCirc (a * p)) by A1, A8, MATRIX_1:26;
then (SCirc (a * p)) * (i,j) = (a * p) . (((i + j) - 1) mod (len (a * p))) by A1, A3, A9, Def4
.= (a * p) /. (((i + j) - 1) mod (len p)) by A1, A10, A7, PARTFUN1:def_6
.= a * (p /. (((i + j) - 1) mod (len p))) by A10, A11, POLYNOM1:def_1
.= (a multfield) . (p /. (((i + j) - 1) mod (len p))) by FVSUM_1:49
.= (a multfield) . (p . (((i + j) - 1) mod (len p))) by A10, A11, PARTFUN1:def_6
.= (a multfield) . ((SCirc p) * (i,j)) by A5, A8, A9, Def4
.= a * ((SCirc p) * (i,j)) by FVSUM_1:49 ;
hence  (SCirc (a * p)) * (i,j) = a * ((SCirc p) * (i,j)) ; ::_thesis: verum
end;
supposeA12: i + j = (len p) + 1 ; ::_thesis: (SCirc (a * p)) * (i,j) = a * ((SCirc p) * (i,j))
A13: [i,j] in Indices (SCirc (a * p)) by A1, A8, MATRIX_1:26;
 ( i in Seg (len p) & j in Seg (len p) ) by A4, A8, ZFMISC_1:87;
then  ( 1 <= i & 1 <= j ) by FINSEQ_1:1;
then  1 + 1 <= i + j by XREAL_1:7;
then  ((len p) + 1) - 1 >= (1 + 1) - 1 by A12, XREAL_1:9;
then A14: len p in Seg (len p) ;
then A15: len p in dom (a * p) by A1, FINSEQ_1:def_3;
A16: len p in dom p by A14, FINSEQ_1:def_3;
(SCirc (a * p)) * (i,j) = (a * p) . (len (a * p)) by A1, A3, A12, A13, Def4
.= (a * p) /. (len p) by A1, A15, PARTFUN1:def_6
.= a * (p /. (len p)) by A16, POLYNOM1:def_1
.= (a multfield) . (p /. (len p)) by FVSUM_1:49
.= (a multfield) . (p . (len p)) by A16, PARTFUN1:def_6
.= (a multfield) . ((SCirc p) * (i,j)) by A5, A8, A12, Def4
.= a * ((SCirc p) * (i,j)) by FVSUM_1:49 ;
hence  (SCirc (a * p)) * (i,j) = a * ((SCirc p) * (i,j)) ; ::_thesis: verum
end;
end;
end;
hence  (SCirc (a * p)) * (i,j) = a * ((SCirc p) * (i,j)) ; ::_thesis: verum
end;
A17: ( len (SCirc p) = len p & width (SCirc p) = len p ) by MATRIX_1:24;
 ( len (SCirc (a * p)) = len p & width (SCirc (a * p)) = len p ) by A1, MATRIX_1:24;
hence  SCirc (a * p) = a * (SCirc p) by A17, A6, MATRIX_3:def_5; ::_thesis: verum
end;

theorem :: MATRIX17:14
for K being Field
for a, b being Element of K
for p being FinSequence of K st p is first-symmetry-of-circulant holds
(a * (SCirc p)) + (b * (SCirc p)) = SCirc ((a + b) * p)
proof
let K be Field; ::_thesis: for a, b being Element of K
for p being FinSequence of K st p is first-symmetry-of-circulant holds
(a * (SCirc p)) + (b * (SCirc p)) = SCirc ((a + b) * p)
let a, b be Element of K; ::_thesis: for p being FinSequence of K st p is first-symmetry-of-circulant holds
(a * (SCirc p)) + (b * (SCirc p)) = SCirc ((a + b) * p)
let p be FinSequence of K; ::_thesis: ( p is first-symmetry-of-circulant implies (a * (SCirc p)) + (b * (SCirc p)) = SCirc ((a + b) * p) )
A1: len (b * p) = len p by MATRIXR1:16;
A2: p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:92;
assume A3: p is first-symmetry-of-circulant ; ::_thesis: (a * (SCirc p)) + (b * (SCirc p)) = SCirc ((a + b) * p)
then A4: ( a * p is first-symmetry-of-circulant & b * p is first-symmetry-of-circulant ) by Th8;
 ( a * (SCirc p) = SCirc (a * p) & b * (SCirc p) = SCirc (b * p) ) by A3, Th9;
then  (a * (SCirc p)) + (b * (SCirc p)) = SCirc ((a * p) + (b * p)) by A4, A1, Th7, MATRIXR1:16;
hence  (a * (SCirc p)) + (b * (SCirc p)) = SCirc ((a + b) * p) by A2, FVSUM_1:55; ::_thesis: verum
end;

theorem :: MATRIX17:15
for K being Field
for a being Element of K
for p, q being FinSequence of K st p is first-symmetry-of-circulant & q is first-symmetry-of-circulant & len p = len q holds
(a * (SCirc p)) + (a * (SCirc q)) = SCirc (a * (p + q))
proof
let K be Field; ::_thesis: for a being Element of K
for p, q being FinSequence of K st p is first-symmetry-of-circulant & q is first-symmetry-of-circulant & len p = len q holds
(a * (SCirc p)) + (a * (SCirc q)) = SCirc (a * (p + q))
let a be Element of K; ::_thesis: for p, q being FinSequence of K st p is first-symmetry-of-circulant & q is first-symmetry-of-circulant & len p = len q holds
(a * (SCirc p)) + (a * (SCirc q)) = SCirc (a * (p + q))
let p, q be FinSequence of K; ::_thesis: ( p is first-symmetry-of-circulant & q is first-symmetry-of-circulant & len p = len q implies (a * (SCirc p)) + (a * (SCirc q)) = SCirc (a * (p + q)) )
assume that
A1: ( p is first-symmetry-of-circulant & q is first-symmetry-of-circulant ) and
A2: len p = len q ; ::_thesis: (a * (SCirc p)) + (a * (SCirc q)) = SCirc (a * (p + q))
A3: ( len (SCirc p) = len p & width (SCirc p) = len p ) by MATRIX_1:24;
 ( len (SCirc q) = len p & width (SCirc q) = len p ) by A2, MATRIX_1:24;
then (a * (SCirc p)) + (a * (SCirc q)) = a * ((SCirc p) + (SCirc q)) by A3, MATRIX_5:20
.= a * (SCirc (p + q)) by A1, A2, Th7
.= SCirc (a * (p + q)) by A1, A2, Th6, Th9 ;
hence  (a * (SCirc p)) + (a * (SCirc q)) = SCirc (a * (p + q)) ; ::_thesis: verum
end;

theorem :: MATRIX17:16
for K being Field
for a, b being Element of K
for p, q being FinSequence of K st p is first-symmetry-of-circulant & q is first-symmetry-of-circulant & len p = len q holds
(a * (SCirc p)) + (b * (SCirc q)) = SCirc ((a * p) + (b * q))
proof
let K be Field; ::_thesis: for a, b being Element of K
for p, q being FinSequence of K st p is first-symmetry-of-circulant & q is first-symmetry-of-circulant & len p = len q holds
(a * (SCirc p)) + (b * (SCirc q)) = SCirc ((a * p) + (b * q))
let a, b be Element of K; ::_thesis: for p, q being FinSequence of K st p is first-symmetry-of-circulant & q is first-symmetry-of-circulant & len p = len q holds
(a * (SCirc p)) + (b * (SCirc q)) = SCirc ((a * p) + (b * q))
let p, q be FinSequence of K; ::_thesis: ( p is first-symmetry-of-circulant & q is first-symmetry-of-circulant & len p = len q implies (a * (SCirc p)) + (b * (SCirc q)) = SCirc ((a * p) + (b * q)) )
set n = len p;
assume that
A1: p is first-symmetry-of-circulant and
A2: q is first-symmetry-of-circulant and
A3: len p = len q ; ::_thesis: (a * (SCirc p)) + (b * (SCirc q)) = SCirc ((a * p) + (b * q))
A4: ( a * p is first-symmetry-of-circulant & b * q is first-symmetry-of-circulant ) by A1, A2, Th8;
A5: len (b * q) = len p by A3, MATRIXR1:16;
(a * (SCirc p)) + (b * (SCirc q)) = (SCirc (a * p)) + (b * (SCirc q)) by A1, Th9
.= (SCirc (a * p)) + (SCirc (b * q)) by A2, Th9
.= SCirc ((a * p) + (b * q)) by A4, A5, Th7, MATRIXR1:16 ;
hence  (a * (SCirc p)) + (b * (SCirc q)) = SCirc ((a * p) + (b * q)) ; ::_thesis: verum
end;

theorem Th13: :: MATRIX17:17
for n being Nat
for K being Field
for M1 being Matrix of n,K st M1 is symmetry_circulant holds
M1 @ = M1
proof
let n be Nat; ::_thesis: for K being Field
for M1 being Matrix of n,K st M1 is symmetry_circulant holds
M1 @ = M1
let K be Field; ::_thesis: for M1 being Matrix of n,K st M1 is symmetry_circulant holds
M1 @ = M1
let M1 be Matrix of n,K; ::_thesis: ( M1 is symmetry_circulant implies M1 @ = M1 )
assume  M1 is symmetry_circulant ; ::_thesis: M1 @ = M1
then consider p being FinSequence of K such that
 len p = width M1 and
A1: M1 is_symmetry_circulant_about p by Def5;
A2: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A3: ( len M1 = n & width M1 = n ) by MATRIX_1:24;
A4: ( len (M1 @) = n & width (M1 @) = n ) by MATRIX_1:24;
 for i, j being Nat st [i,j] in Indices M1 holds
(M1 @) * (i,j) = M1 * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices M1 implies (M1 @) * (i,j) = M1 * (i,j) )
assume A5: [i,j] in Indices M1 ; ::_thesis: (M1 @) * (i,j) = M1 * (i,j)
percases ( i + j <> (len p) + 1 or i + j = (len p) + 1 ) ;
supposeA6: i + j <> (len p) + 1 ; ::_thesis: (M1 @) * (i,j) = M1 * (i,j)
 ( i in Seg n & j in Seg n ) by A2, A5, ZFMISC_1:87;
then A7: [j,i] in [:(Seg n),(Seg n):] by ZFMISC_1:87;
then (M1 @) * (i,j) = M1 * (j,i) by A2, MATRIX_1:def_6
.= p . (((i + j) - 1) mod (len p)) by A1, A7, A6, A2, Def4 ;
hence  (M1 @) * (i,j) = M1 * (i,j) by A1, A5, A6, Def4; ::_thesis: verum
end;
supposeA8: i + j = (len p) + 1 ; ::_thesis: (M1 @) * (i,j) = M1 * (i,j)
 ( i in Seg n & j in Seg n ) by A5, A2, ZFMISC_1:87;
then A9: [j,i] in [:(Seg n),(Seg n):] by ZFMISC_1:87;
(M1 @) * (i,j) = M1 * (j,i) by A2, A9, MATRIX_1:def_6
.= p . (len p) by A1, A9, A8, A2, Def4 ;
hence  (M1 @) * (i,j) = M1 * (i,j) by A1, A8, A5, Def4; ::_thesis: verum
end;
end;
end;
hence  M1 @ = M1 by A3, A4, MATRIX_1:21; ::_thesis: verum
end;

registration
let n be Nat;
let K be Field;
cluster symmetry_circulant  ->  symmetric for Matrix of n,n, the carrier of K;
coherence
 for b1 being Matrix of n,K st b1 is symmetry_circulant holds
b1 is symmetric
proof
let M be Matrix of n,K; ::_thesis: ( M is symmetry_circulant implies M is symmetric )
assume  M is symmetry_circulant ; ::_thesis: M is symmetric
hence  M @ = M by Th13; :: according to MATRIX_6:def_5 ::_thesis: verum
end;
end;