let K be Field; for p, q being FinSequence of K st len p = len q & p is first-col-of-circulant & q is first-col-of-circulant holds
CCirc (p + q) = (CCirc p) + (CCirc q)
let p, q be FinSequence of K; ( len p = len q & p is first-col-of-circulant & q is first-col-of-circulant implies CCirc (p + q) = (CCirc p) + (CCirc q) )
set n = len p;
assume that
A1:
len p = len q
and
A2:
p is first-col-of-circulant
and
A3:
q is first-col-of-circulant
; CCirc (p + q) = (CCirc p) + (CCirc q)
A4:
( CCirc q is_col_circulant_about q & Indices (CCirc p) = Indices (CCirc q) )
by A1, A3, Def8, MATRIX_0:26;
p + q is first-col-of-circulant
by A1, A2, A3, Th37;
then A5:
CCirc (p + q) is_col_circulant_about p + q
by Def8;
A6:
dom p = Seg (len p)
by FINSEQ_1:def 3;
A7:
CCirc p is_col_circulant_about p
by A2, Def8;
A8:
dom (p + q) = Seg (len (p + q))
by FINSEQ_1:def 3;
A9:
Indices (CCirc 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 (CCirc p) = Indices (CCirc (p + q))
by MATRIX_0:26;
A12:
for i, j being Nat st [i,j] in Indices (CCirc p) holds
(CCirc (p + q)) * (i,j) = ((CCirc p) * (i,j)) + ((CCirc q) * (i,j))
proof
let i,
j be
Nat;
( [i,j] in Indices (CCirc p) implies (CCirc (p + q)) * (i,j) = ((CCirc p) * (i,j)) + ((CCirc q) * (i,j)) )
assume A13:
[i,j] in Indices (CCirc p)
;
(CCirc (p + q)) * (i,j) = ((CCirc p) * (i,j)) + ((CCirc q) * (i,j))
then A14:
((i - j) mod (len p)) + 1
in Seg (len p)
by A9, Lm3;
(CCirc (p + q)) * (
i,
j) =
(p + q) . (((i - j) mod (len (p + q))) + 1)
by A5, A11, A13
.=
the
addF of
K . (
(p . (((i - j) mod (len (p + q))) + 1)),
(q . (((i - j) mod (len (p + q))) + 1)))
by A8, A10, A14, FUNCOP_1:22
.=
the
addF of
K . (
((CCirc p) * (i,j)),
(q . (((i - j) mod (len q)) + 1)))
by A1, A10, A7, A13
.=
((CCirc p) * (i,j)) + ((CCirc q) * (i,j))
by A4, A13
;
hence
(CCirc (p + q)) * (
i,
j)
= ((CCirc p) * (i,j)) + ((CCirc q) * (i,j))
;
verum
end;
A15:
( len (CCirc p) = len p & width (CCirc p) = len p )
by MATRIX_0:24;
( len (CCirc (p + q)) = len p & width (CCirc (p + q)) = len p )
by A10, MATRIX_0:24;
hence
CCirc (p + q) = (CCirc p) + (CCirc q)
by A15, A12, MATRIX_3:def 3; verum