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 A1: M1 is_symmetry_circulant_about p ; :: thesis: a * M1 is_symmetry_circulant_about a * p

then A2: len p = width M1 ;

A3: Indices (a * M1) = [:(Seg n),(Seg n):] by MATRIX_0:24;

A4: width M1 = n by MATRIX_0: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)))

(a * M1) * (i,j) = (a * p) . (len (a * p))

len p = n by A2, MATRIX_0:24;

hence a * M1 is_symmetry_circulant_about a * p by A21, A8, A13; :: thesis: verum

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 A1: M1 is_symmetry_circulant_about p ; :: thesis: a * M1 is_symmetry_circulant_about a * p

then A2: len p = width M1 ;

A3: Indices (a * M1) = [:(Seg n),(Seg n):] by MATRIX_0:24;

A4: width M1 = n by MATRIX_0: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

A13:
for i, j being Nat st [i,j] in Indices (a * M1) & i + j = (len (a * p)) + 1 holds
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 A3, A2, A4, A9, A10, A7, Lm4;

A12: [i,j] in Indices M1 by A3, A9, MATRIX_0: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 A1, A12, A10, A7

.= (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;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 A3, A2, A4, A9, A10, A7, Lm4;

A12: [i,j] in Indices M1 by A3, A9, MATRIX_0: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 A1, A12, A10, A7

.= (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

(a * M1) * (i,j) = (a * p) . (len (a * p))

proof

A21:
( width (a * M1) = n & len (a * p) = len p )
by MATRIXR1:16, MATRIX_0:24;
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 A3, 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 A3, A14, MATRIX_0: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 A1, A20, A15, A7

.= (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;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 A3, 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 A3, A14, MATRIX_0: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 A1, A20, A15, A7

.= (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

len p = n by A2, MATRIX_0:24;

hence a * M1 is_symmetry_circulant_about a * p by A21, A8, A13; :: thesis: verum