let n be Nat; for K being Field
for p, q being FinSequence of K
for M1, M2 being Matrix of n,K st M1 is_symmetry_circulant_about p & M2 is_symmetry_circulant_about q holds
M1 + M2 is_symmetry_circulant_about p + q
let K be Field; for p, q being FinSequence of K
for M1, M2 being Matrix of n,K st M1 is_symmetry_circulant_about p & M2 is_symmetry_circulant_about q holds
M1 + M2 is_symmetry_circulant_about p + q
let p, q be FinSequence of K; for M1, M2 being Matrix of n,K st M1 is_symmetry_circulant_about p & M2 is_symmetry_circulant_about q holds
M1 + M2 is_symmetry_circulant_about p + q
let M1, M2 be Matrix of n,K; ( M1 is_symmetry_circulant_about p & M2 is_symmetry_circulant_about q implies M1 + M2 is_symmetry_circulant_about p + q )
assume A3:
M1 is_symmetry_circulant_about p
; ( not M2 is_symmetry_circulant_about q or M1 + M2 is_symmetry_circulant_about p + q )
A2:
len p = width M1
by A3, Def4;
A4:
Indices M2 = [:(Seg n),(Seg n):]
by MATRIX_1:24;
A5:
Indices (M1 + M2) = [:(Seg n),(Seg n):]
by MATRIX_1:24;
A6:
width M1 = n
by MATRIX_1:24;
then A7:
dom p = Seg n
by A2, FINSEQ_1:def 3;
assume A9:
M2 is_symmetry_circulant_about q
; M1 + M2 is_symmetry_circulant_about p + q
then A8:
len q = width M2
by Def4;
A10:
Indices M1 = [:(Seg n),(Seg n):]
by MATRIX_1:24;
A11:
n in NAT
by ORDINAL1:def 12;
A12:
width M2 = n
by MATRIX_1:24;
then
dom q = Seg n
by A8, FINSEQ_1:def 3;
then A13:
dom (p + q) = dom p
by A7, POLYNOM1:1;
then A14:
len (p + q) = n
by A7, A11, FINSEQ_1:def 3;
A15:
width (M1 + M2) = n
by MATRIX_1:24;
A16:
dom (p + q) = Seg (len (p + q))
by FINSEQ_1:def 3;
A17:
for i, j being Nat st [i,j] in Indices (M1 + M2) & i + j <> (len (p + q)) + 1 holds
(M1 + M2) * (i,j) = (p + q) . (((i + j) - 1) mod (len (p + q)))
proof
let i,
j be
Nat;
( [i,j] in Indices (M1 + M2) & i + j <> (len (p + q)) + 1 implies (M1 + M2) * (i,j) = (p + q) . (((i + j) - 1) mod (len (p + q))) )
assume that A18:
[i,j] in Indices (M1 + M2)
and A19:
i + j <> (len (p + q)) + 1
;
(M1 + M2) * (i,j) = (p + q) . (((i + j) - 1) mod (len (p + q)))
A20:
((i + j) - 1) mod (len (p + q)) in dom (p + q)
by A5, A16, A19, A18, A13, A7, Lm4;
(M1 + M2) * (
i,
j) =
(M1 * (i,j)) + (M2 * (i,j))
by A10, A5, A18, MATRIX_3:def 3
.=
the
addF of
K . (
(M1 * (i,j)),
(q . (((i + j) - 1) mod (len (p + q)))))
by A9, A4, A5, A8, A12, A18, A19, A14, Def4
.=
the
addF of
K . (
(p . (((i + j) - 1) mod (len (p + q)))),
(q . (((i + j) - 1) mod (len (p + q)))))
by A3, A2, A6, A10, A5, A14, A18, A19, Def4
.=
(p + q) . (((i + j) - 1) mod (len (p + q)))
by A20, FUNCOP_1:22
;
hence
(M1 + M2) * (
i,
j)
= (p + q) . (((i + j) - 1) mod (len (p + q)))
;
verum
end;
for i, j being Nat st [i,j] in Indices (M1 + M2) & i + j = (len (p + q)) + 1 holds
(M1 + M2) * (i,j) = (p + q) . (len (p + q))
proof
let i,
j be
Nat;
( [i,j] in Indices (M1 + M2) & i + j = (len (p + q)) + 1 implies (M1 + M2) * (i,j) = (p + q) . (len (p + q)) )
assume that A21:
[i,j] in Indices (M1 + M2)
and A22:
i + j = (len (p + q)) + 1
;
(M1 + M2) * (i,j) = (p + q) . (len (p + q))
(
i in Seg n &
j in Seg n )
by A5, A21, ZFMISC_1:87;
then
( 1
<= i & 1
<= j )
by FINSEQ_1:1;
then
1
+ 1
<= i + j
by XREAL_1:7;
then
((len (p + q)) + 1) - 1
>= (1 + 1) - 1
by A22, XREAL_1:9;
then
len (p + q) in Seg (len (p + q))
;
then A23:
len (p + q) in dom (p + q)
by FINSEQ_1:def 3;
(M1 + M2) * (
i,
j) =
(M1 * (i,j)) + (M2 * (i,j))
by A10, A5, A21, MATRIX_3:def 3
.=
the
addF of
K . (
(M1 * (i,j)),
(q . (len (p + q))))
by A9, A8, A12, A14, A4, A5, A21, A22, Def4
.=
the
addF of
K . (
(p . (len (p + q))),
(q . (len (p + q))))
by A2, A3, A10, A6, A5, A14, A21, A22, Def4
.=
(p + q) . (len (p + q))
by A23, FUNCOP_1:22
;
hence
(M1 + M2) * (
i,
j)
= (p + q) . (len (p + q))
;
verum
end;
hence
M1 + M2 is_symmetry_circulant_about p + q
by A15, A14, A17, Def4; verum