let n be Element of NAT ; for K being Field
for M1, M2 being Matrix of n,K st M1 is anti-circular & M2 is anti-circular holds
M1 + M2 is anti-circular
let K be Field; for M1, M2 being Matrix of n,K st M1 is anti-circular & M2 is anti-circular holds
M1 + M2 is anti-circular
let M1, M2 be Matrix of n,K; ( M1 is anti-circular & M2 is anti-circular implies M1 + M2 is anti-circular )
assume that
A1:
M1 is anti-circular
and
A2:
M2 is anti-circular
; M1 + M2 is anti-circular
consider p being FinSequence of K such that
A3:
len p = width M1
and
A4:
M1 is_anti-circular_about p
by A1, Def10;
A5:
width M1 = n
by MATRIX_1:25;
then A6:
dom p = Seg n
by A3, FINSEQ_1:def 3;
consider q being FinSequence of K such that
A7:
len q = width M2
and
A8:
M2 is_anti-circular_about q
by A2, Def10;
A9:
dom (p + q) = Seg (len (p + q))
by FINSEQ_1:def 3;
A10:
width M2 = n
by MATRIX_1:25;
then
dom q = Seg n
by A7, FINSEQ_1:def 3;
then A11:
dom (p + q) = dom p
by A6, POLYNOM1:5;
then A12:
len (p + q) = n
by A6, FINSEQ_1:def 3;
A13:
p is Element of (len p) -tuples_on the carrier of K
by FINSEQ_2:110;
then
- p is Element of (len p) -tuples_on the carrier of K
by FINSEQ_2:133;
then
len (- p) = len p
by FINSEQ_1:def 18;
then A14:
dom (- p) = Seg n
by A3, A5, FINSEQ_1:def 3;
A15:
Indices M2 = [:(Seg n),(Seg n):]
by MATRIX_1:25;
A16:
Indices (M1 + M2) = [:(Seg n),(Seg n):]
by MATRIX_1:25;
set r = p + q;
A17:
Indices M1 = [:(Seg n),(Seg n):]
by MATRIX_1:25;
A18:
q is Element of (len q) -tuples_on the carrier of K
by FINSEQ_2:110;
then
- q is Element of (len q) -tuples_on the carrier of K
by FINSEQ_2:133;
then
len (- q) = len q
by FINSEQ_1:def 18;
then A19:
dom (- q) = Seg n
by A7, A10, FINSEQ_1:def 3;
A20:
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 A21:
[i,j] in Indices (M1 + M2)
and A22:
i >= j
;
(M1 + M2) * i,j = (- (p + q)) . (((j - i) mod (len (p + q))) + 1)
dom ((- p) + (- q)) = dom (- p)
by A14, A19, POLYNOM1:5;
then A23:
((j - i) mod (len (p + q))) + 1
in dom ((- p) + (- q))
by A16, A6, A9, A14, A11, A21, Lm3;
(M1 + M2) * i,
j =
(M1 * i,j) + (M2 * i,j)
by A17, A16, A21, MATRIX_3:def 3
.=
the
addF of
K . (M1 * i,j),
((- q) . (((j - i) mod (len q)) + 1))
by A8, A15, A16, A21, A22, Def9
.=
the
addF of
K . ((- p) . (((j - i) mod (len (p + q))) + 1)),
((- q) . (((j - i) mod (len (p + q))) + 1))
by A3, A4, A7, A17, A5, A10, A16, A12, A21, A22, Def9
.=
((- p) + (- q)) . (((j - i) mod (len (p + q))) + 1)
by A23, FUNCOP_1:28
.=
(- (p + q)) . (((j - i) mod (len (p + q))) + 1)
by A3, A7, A13, A18, A5, A10, FVSUM_1:40
;
hence
(M1 + M2) * i,
j = (- (p + q)) . (((j - i) mod (len (p + q))) + 1)
;
verum
end;
A24:
width (M1 + M2) = n
by MATRIX_1:25;
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 A25:
[i,j] in Indices (M1 + M2)
and A26:
i <= j
;
(M1 + M2) * i,j = (p + q) . (((j - i) mod (len (p + q))) + 1)
A27:
((j - i) mod (len (p + q))) + 1
in dom (p + q)
by A16, A6, A9, A11, A25, Lm3;
(M1 + M2) * i,
j =
(M1 * i,j) + (M2 * i,j)
by A17, A16, A25, MATRIX_3:def 3
.=
the
addF of
K . (M1 * i,j),
(q . (((j - i) mod (len q)) + 1))
by A8, A15, A16, A25, A26, Def9
.=
the
addF of
K . (p . (((j - i) mod (len (p + q))) + 1)),
(q . (((j - i) mod (len (p + q))) + 1))
by A3, A4, A7, A17, A5, A10, A16, A12, A25, A26, Def9
.=
(p + q) . (((j - i) mod (len (p + q))) + 1)
by A27, FUNCOP_1:28
;
hence
(M1 + M2) * i,
j = (p + q) . (((j - i) mod (len (p + q))) + 1)
;
verum
end;
then
M1 + M2 is_anti-circular_about p + q
by A24, A12, A20, Def9;
then consider r being FinSequence of K such that
A28:
( len r = width (M1 + M2) & M1 + M2 is_anti-circular_about r )
by A24, A12;
take
r
; MATRIX16:def 10 ( len r = width (M1 + M2) & M1 + M2 is_anti-circular_about r )
thus
( len r = width (M1 + M2) & M1 + M2 is_anti-circular_about r )
by A28; verum