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