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