let n be 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
let K be 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 a be 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 p be 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 M1 be Matrix of n,K; ( M1 is_symmetry_circulant_about p implies a * M1 is_symmetry_circulant_about a * p )
assume A1:
M1 is_symmetry_circulant_about p
; 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
let i,
j be
Nat;
( [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
;
(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;
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;
( [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
;
(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;
verum
end;
A21:
( width (a * M1) = n & len (a * p) = len p )
by MATRIXR1:16, MATRIX_0:24;
len p = n
by A2, MATRIX_0:24;
hence
a * M1 is_symmetry_circulant_about a * p
by A21, A8, A13; verum