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 Th12;
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_0: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))

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

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

end;

suppose A12: 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_0: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
.= (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
.= 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_0:24;
( len (SCirc (a * p)) = len p & width (SCirc (a * p)) = len p ) by A1, MATRIX_0:24;
hence SCirc (a * p) = a * (SCirc p) by A17, A6, MATRIX_3:def 5; :: thesis: verum