let K be Field; for p, q being FinSequence of K st p is first-line-of-anti-circular & q is first-line-of-anti-circular & len p = len q holds
ACirc (p + q) = (ACirc p) + (ACirc q)
let p, q be FinSequence of K; ( p is first-line-of-anti-circular & q is first-line-of-anti-circular & len p = len q implies ACirc (p + q) = (ACirc p) + (ACirc q) )
set n = len p;
assume that
A1:
p is first-line-of-anti-circular
and
A2:
q is first-line-of-anti-circular
and
A3:
len p = len q
; ACirc (p + q) = (ACirc p) + (ACirc q)
A4:
dom p = Seg (len p)
by FINSEQ_1:def 3;
dom q = Seg (len p)
by A3, FINSEQ_1:def 3;
then A5:
dom (p + q) = dom p
by A4, POLYNOM1:1;
then A6:
len (p + q) = len p
by A4, FINSEQ_1:def 3;
then A7:
Indices (ACirc p) = Indices (ACirc (p + q))
by MATRIX_0:26;
A8:
Indices (ACirc p) = Indices (ACirc q)
by A3, MATRIX_0:26;
A9:
dom (p + q) = Seg (len (p + q))
by FINSEQ_1:def 3;
A10:
p is Element of (len p) -tuples_on the carrier of K
by FINSEQ_2:92;
then
- p is Element of (len p) -tuples_on the carrier of K
by FINSEQ_2:113;
then A11:
len (- p) = len p
by CARD_1:def 7;
A12:
Indices (ACirc p) = [:(Seg (len p)),(Seg (len p)):]
by MATRIX_0:24;
p + q is first-line-of-anti-circular
by A1, A2, A3, Th60;
then A13:
ACirc (p + q) is_anti-circular_about p + q
by Def12;
A14:
ACirc q is_anti-circular_about q
by A2, Def12;
A15:
q is Element of (len q) -tuples_on the carrier of K
by FINSEQ_2:92;
then
- q is Element of (len q) -tuples_on the carrier of K
by FINSEQ_2:113;
then A16:
len (- q) = len q
by CARD_1:def 7;
A17:
ACirc p is_anti-circular_about p
by A1, Def12;
A18:
Indices (ACirc q) = [:(Seg (len p)),(Seg (len p)):]
by A3, MATRIX_0:24;
A19:
for i, j being Nat st [i,j] in Indices (ACirc p) holds
(ACirc (p + q)) * (i,j) = ((ACirc p) * (i,j)) + ((ACirc q) * (i,j))
proof
let i,
j be
Nat;
( [i,j] in Indices (ACirc p) implies (ACirc (p + q)) * (i,j) = ((ACirc p) * (i,j)) + ((ACirc q) * (i,j)) )
assume A20:
[i,j] in Indices (ACirc p)
;
(ACirc (p + q)) * (i,j) = ((ACirc p) * (i,j)) + ((ACirc q) * (i,j))
then A21:
((j - i) mod (len p)) + 1
in Seg (len p)
by A12, Lm3;
now ( ( i <= j & (ACirc (p + q)) * (i,j) = ((ACirc p) * (i,j)) + ((ACirc q) * (i,j)) ) or ( i >= j & (ACirc (p + q)) * (i,j) = ((ACirc p) * (i,j)) + ((ACirc q) * (i,j)) ) )per cases
( i <= j or i >= j )
;
case A22:
i <= j
;
(ACirc (p + q)) * (i,j) = ((ACirc p) * (i,j)) + ((ACirc q) * (i,j))then (ACirc (p + q)) * (
i,
j) =
(p + q) . (((j - i) mod (len (p + q))) + 1)
by A13, A7, A20
.=
the
addF of
K . (
(p . (((j - i) mod (len (p + q))) + 1)),
(q . (((j - i) mod (len (p + q))) + 1)))
by A9, A6, A21, FUNCOP_1:22
.=
the
addF of
K . (
((ACirc p) * (i,j)),
(q . (((j - i) mod (len q)) + 1)))
by A3, A6, A17, A20, A22
.=
((ACirc p) * (i,j)) + ((ACirc q) * (i,j))
by A14, A8, A20, A22
;
hence
(ACirc (p + q)) * (
i,
j)
= ((ACirc p) * (i,j)) + ((ACirc q) * (i,j))
;
verum end; case A23:
i >= j
;
(ACirc (p + q)) * (i,j) = ((ACirc p) * (i,j)) + ((ACirc q) * (i,j))A24:
dom (- p) = Seg (len p)
by A11, FINSEQ_1:def 3;
dom (- q) = Seg (len q)
by A16, FINSEQ_1:def 3;
then
(
dom p = Seg (len p) &
dom ((- p) + (- q)) = dom (- p) )
by A3, A24, FINSEQ_1:def 3, POLYNOM1:1;
then A25:
((j - i) mod (len (p + q))) + 1
in dom ((- p) + (- q))
by A9, A5, A12, A20, A24, Lm3;
(ACirc (p + q)) * (
i,
j) =
(- (p + q)) . (((j - i) mod (len (p + q))) + 1)
by A13, A7, A20, A23
.=
((- p) + (- q)) . (((j - i) mod (len (p + q))) + 1)
by A3, A10, A15, FVSUM_1:31
.=
the
addF of
K . (
((- p) . (((j - i) mod (len (p + q))) + 1)),
((- q) . (((j - i) mod (len (p + q))) + 1)))
by A25, FUNCOP_1:22
.=
the
addF of
K . (
((ACirc p) * (i,j)),
((- q) . (((j - i) mod (len q)) + 1)))
by A3, A6, A17, A20, A23
.=
((ACirc p) * (i,j)) + ((ACirc q) * (i,j))
by A14, A12, A18, A20, A23
;
hence
(ACirc (p + q)) * (
i,
j)
= ((ACirc p) * (i,j)) + ((ACirc q) * (i,j))
;
verum end;
hence
(ACirc (p + q)) * (
i,
j)
= ((ACirc p) * (i,j)) + ((ACirc q) * (i,j))
;
verum
end;
A26:
( len (ACirc p) = len p & width (ACirc p) = len p )
by MATRIX_0:24;
( len (ACirc (p + q)) = len p & width (ACirc (p + q)) = len p )
by A6, MATRIX_0:24;
hence
ACirc (p + q) = (ACirc p) + (ACirc q)
by A26, A19, MATRIX_3:def 3; verum