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_0:24;
A2: Indices (SCirc p) = [:(Seg (len p)),(Seg (len p)):] by MATRIX_0: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 Th8;
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))

per cases ( i + j <> (len p) + 1 or i + j = (len p) + 1 ) ;

suppose A9: 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_0:26;
then (SCirc (- p)) * (i,j) = (- p) . (((i + j) - 1) mod (len (- p))) by A5, A9, A3
.= (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
.= - ((SCirc p) * (i,j)) by VECTSP_1:def 13 ;
hence (SCirc (- p)) * (i,j) = - ((SCirc p) * (i,j)) ; :: thesis: verum

end;

suppose A11: 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 A12: len p in dom p by FINSEQ_1:def 3;
[i,j] in Indices (SCirc (- p)) by A3, A8, MATRIX_0:26;
then (SCirc (- p)) * (i,j) = (- p) . (len (- p)) by A5, A11, A3
.= (comp K) . (p . (len p)) by A3, A12, FUNCT_1:13
.= (comp K) . ((SCirc p) * (i,j)) by A6, A8, A11
.= - ((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_0:24;
hence SCirc (- p) = - (SCirc p) by A1, A7, MATRIX_3:def 2; :: thesis: verum