let K be Field; for p, q being FinSequence of K st len p = len q & p is first-symmetry-of-circulant & q is first-symmetry-of-circulant holds
SCirc (p + q) = (SCirc p) + (SCirc q)
let p, q be FinSequence of K; ( len p = len q & p is first-symmetry-of-circulant & q is first-symmetry-of-circulant implies SCirc (p + q) = (SCirc p) + (SCirc q) )
set n = len p;
assume that
A1:
len p = len q
and
A2:
p is first-symmetry-of-circulant
and
A3:
q is first-symmetry-of-circulant
; SCirc (p + q) = (SCirc p) + (SCirc q)
A4:
( SCirc q is_symmetry_circulant_about q & Indices (SCirc p) = Indices (SCirc q) )
by A1, A3, Def7, MATRIX_0:26;
p + q is first-symmetry-of-circulant
by A1, A2, A3, Th10;
then A5:
SCirc (p + q) is_symmetry_circulant_about p + q
by Def7;
A6:
dom p = Seg (len p)
by FINSEQ_1:def 3;
A7:
SCirc p is_symmetry_circulant_about p
by A2, Def7;
A8:
dom (p + q) = Seg (len (p + q))
by FINSEQ_1:def 3;
A9:
Indices (SCirc p) = [:(Seg (len p)),(Seg (len p)):]
by MATRIX_0:24;
dom q = Seg (len p)
by A1, FINSEQ_1:def 3;
then
dom (p + q) = dom p
by A6, POLYNOM1:1;
then A10:
len (p + q) = len p
by A6, FINSEQ_1:def 3;
then A11:
Indices (SCirc p) = Indices (SCirc (p + q))
by MATRIX_0:26;
A12:
for i, j being Nat st [i,j] in Indices (SCirc p) holds
(SCirc (p + q)) * (i,j) = ((SCirc p) * (i,j)) + ((SCirc q) * (i,j))
proof
let i,
j be
Nat;
( [i,j] in Indices (SCirc p) implies (SCirc (p + q)) * (i,j) = ((SCirc p) * (i,j)) + ((SCirc q) * (i,j)) )
assume A13:
[i,j] in Indices (SCirc p)
;
(SCirc (p + q)) * (i,j) = ((SCirc p) * (i,j)) + ((SCirc q) * (i,j))
now (SCirc (p + q)) * (i,j) = ((SCirc p) * (i,j)) + ((SCirc q) * (i,j))per cases
( i + j <> (len (p + q)) + 1 or i + j = (len (p + q)) + 1 )
;
suppose A14:
i + j <> (len (p + q)) + 1
;
(SCirc (p + q)) * (i,j) = ((SCirc p) * (i,j)) + ((SCirc q) * (i,j))A15:
((i + j) - 1) mod (len p) in Seg (len p)
by A9, A13, A14, A10, Lm4;
(SCirc (p + q)) * (
i,
j) =
(p + q) . (((i + j) - 1) mod (len (p + q)))
by A5, A11, A13, A14
.=
the
addF of
K . (
(p . (((i + j) - 1) mod (len (p + q)))),
(q . (((i + j) - 1) mod (len (p + q)))))
by A8, A10, A15, FUNCOP_1:22
.=
the
addF of
K . (
((SCirc p) * (i,j)),
(q . (((i + j) - 1) mod (len q))))
by A1, A10, A7, A13, A14
.=
((SCirc p) * (i,j)) + ((SCirc q) * (i,j))
by A1, A4, A13, A14, A10
;
hence
(SCirc (p + q)) * (
i,
j)
= ((SCirc p) * (i,j)) + ((SCirc q) * (i,j))
;
verum end; suppose A16:
i + j = (len (p + q)) + 1
;
(SCirc (p + q)) * (i,j) = ((SCirc p) * (i,j)) + ((SCirc q) * (i,j))
(
i in Seg (len p) &
j in Seg (len p) )
by A9, A13, 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 A16, XREAL_1:9;
then
len (p + q) in Seg (len (p + q))
;
then A17:
len (p + q) in dom (p + q)
by FINSEQ_1:def 3;
(SCirc (p + q)) * (
i,
j) =
(p + q) . (len (p + q))
by A5, A11, A13, A16
.=
the
addF of
K . (
(p . (len (p + q))),
(q . (len (p + q))))
by A17, FUNCOP_1:22
.=
the
addF of
K . (
((SCirc p) * (i,j)),
(q . (len q)))
by A1, A10, A7, A13, A16
.=
((SCirc p) * (i,j)) + ((SCirc q) * (i,j))
by A4, A13, A16, A1, A10
;
hence
(SCirc (p + q)) * (
i,
j)
= ((SCirc p) * (i,j)) + ((SCirc q) * (i,j))
;
verum
hence
(SCirc (p + q)) * (
i,
j)
= ((SCirc p) * (i,j)) + ((SCirc q) * (i,j))
;
verum
end;
A18:
( len (SCirc p) = len p & width (SCirc p) = len p )
by MATRIX_0:24;
( len (SCirc (p + q)) = len p & width (SCirc (p + q)) = len p )
by A10, MATRIX_0:24;
hence
SCirc (p + q) = (SCirc p) + (SCirc q)
by A18, A12, MATRIX_3:def 3; verum