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
p + q is first-line-of-anti-circular
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 p + q is first-line-of-anti-circular )
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
; p + q is first-line-of-anti-circular
consider M2 being Matrix of len p,K such that
A4:
M2 is_anti-circular_about q
by A2, A3;
A5:
width M2 = len p
by MATRIX_0:24;
A6:
dom p = Seg (len p)
by FINSEQ_1:def 3;
len q = width M2
by A4;
then
dom q = Seg (len p)
by A5, FINSEQ_1:def 3;
then A7:
dom (p + q) = dom p
by A6, POLYNOM1:1;
then A8:
len (p + q) = len p
by A6, FINSEQ_1:def 3;
consider M1 being Matrix of len p,K such that
A9:
M1 is_anti-circular_about p
by A1;
A10:
Indices M1 = [:(Seg (len p)),(Seg (len p)):]
by MATRIX_0:24;
set M3 = M1 + M2;
A11:
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 A12:
len (- q) = len q
by CARD_1:def 7;
A13:
Indices M2 = [:(Seg (len p)),(Seg (len p)):]
by MATRIX_0:24;
A14:
Indices (M1 + M2) = [:(Seg (len p)),(Seg (len p)):]
by MATRIX_0:24;
A15:
dom (p + q) = Seg (len (p + q))
by FINSEQ_1:def 3;
A16:
for i, j being Nat st [i,j] in Indices (M1 + M2) & i <= j holds
(M1 + M2) * (i,j) = (p + q) . (((j - i) mod (len (p + q))) + 1)
proof
let i,
j be
Nat;
( [i,j] in Indices (M1 + M2) & i <= j implies (M1 + M2) * (i,j) = (p + q) . (((j - i) mod (len (p + q))) + 1) )
assume that A17:
[i,j] in Indices (M1 + M2)
and A18:
i <= j
;
(M1 + M2) * (i,j) = (p + q) . (((j - i) mod (len (p + q))) + 1)
A19:
((j - i) mod (len (p + q))) + 1
in dom (p + q)
by A14, A6, A15, A7, A17, Lm3;
(M1 + M2) * (
i,
j) =
(M1 * (i,j)) + (M2 * (i,j))
by A10, A14, A17, MATRIX_3:def 3
.=
the
addF of
K . (
(M1 * (i,j)),
(q . (((j - i) mod (len q)) + 1)))
by A4, A13, A14, A17, A18
.=
the
addF of
K . (
(p . (((j - i) mod (len (p + q))) + 1)),
(q . (((j - i) mod (len (p + q))) + 1)))
by A3, A9, A10, A14, A8, A17, A18
.=
(p + q) . (((j - i) mod (len (p + q))) + 1)
by A19, FUNCOP_1:22
;
hence
(M1 + M2) * (
i,
j)
= (p + q) . (((j - i) mod (len (p + q))) + 1)
;
verum
end;
A20:
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 A21:
len (- p) = len p
by CARD_1:def 7;
then A22:
dom (- p) = Seg (len p)
by FINSEQ_1:def 3;
A23:
for i, j being Nat st [i,j] in Indices (M1 + M2) & i >= j holds
(M1 + M2) * (i,j) = (- (p + q)) . (((j - i) mod (len (p + q))) + 1)
proof
let i,
j be
Nat;
( [i,j] in Indices (M1 + M2) & i >= j implies (M1 + M2) * (i,j) = (- (p + q)) . (((j - i) mod (len (p + q))) + 1) )
assume that A24:
[i,j] in Indices (M1 + M2)
and A25:
i >= j
;
(M1 + M2) * (i,j) = (- (p + q)) . (((j - i) mod (len (p + q))) + 1)
(
dom (- p) = Seg (len p) &
dom (- q) = Seg (len q) )
by A21, A12, FINSEQ_1:def 3;
then
dom ((- p) + (- q)) = dom (- p)
by A3, POLYNOM1:1;
then A26:
((j - i) mod (len (p + q))) + 1
in dom ((- p) + (- q))
by A14, A6, A15, A22, A7, A24, Lm3;
(M1 + M2) * (
i,
j) =
(M1 * (i,j)) + (M2 * (i,j))
by A10, A14, A24, MATRIX_3:def 3
.=
the
addF of
K . (
(M1 * (i,j)),
((- q) . (((j - i) mod (len q)) + 1)))
by A4, A13, A14, A24, A25
.=
the
addF of
K . (
((- p) . (((j - i) mod (len p)) + 1)),
((- q) . (((j - i) mod (len q)) + 1)))
by A9, A10, A14, A24, A25
.=
((- p) + (- q)) . (((j - i) mod (len (p + q))) + 1)
by A3, A8, A26, FUNCOP_1:22
.=
(- (p + q)) . (((j - i) mod (len (p + q))) + 1)
by A3, A20, A11, FVSUM_1:31
;
hence
(M1 + M2) * (
i,
j)
= (- (p + q)) . (((j - i) mod (len (p + q))) + 1)
;
verum
end;
width (M1 + M2) = len p
by MATRIX_0:24;
then
len (p + q) = width (M1 + M2)
by A6, A7, FINSEQ_1:def 3;
then
( len (M1 + M2) = len p & M1 + M2 is_anti-circular_about p + q )
by A16, A23, MATRIX_0:24;
then consider M3 being Matrix of len (p + q),K such that
len (p + q) = len M3
and
A27:
M3 is_anti-circular_about p + q
by A8;
take
M3
; MATRIX16:def 11 M3 is_anti-circular_about p + q
thus
M3 is_anti-circular_about p + q
by A27; verum