let n be Element of NAT ; :: thesis: 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; :: thesis: 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; :: thesis: ( M1 is anti-circular & M2 is anti-circular implies M1 + M2 is anti-circular )
assume A1: ( M1 is anti-circular & M2 is anti-circular ) ; :: thesis: M1 + M2 is anti-circular
consider p being FinSequence of K such that
A2: ( len p = width M1 & M1 is_anti-circular_about p ) by A1, Def11;
consider q being FinSequence of K such that
A3: ( len q = width M2 & M2 is_anti-circular_about q ) by A1, Def11;
E1: 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 A4: len (- p) = len p by FINSEQ_1:def 18;
E2: 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 A5: len (- q) = len q by FINSEQ_1:def 18;
A6: ( Indices M1 = [:(Seg n),(Seg n):] & len M1 = n & width M1 = n & Indices M2 = [:(Seg n),(Seg n):] & len M2 = n & width M2 = n & Indices (M1 + M2) = [:(Seg n),(Seg n):] & len (M1 + M2) = n & width (M1 + M2) = n ) by MATRIX_1:25;
A8: ( dom p = Seg n & dom (p + q) = Seg (len (p + q)) & dom p = Seg (len p) & dom q = Seg n & dom (- p) = Seg n & dom (- q) = Seg n ) by A2, A3, A4, A5, A6, FINSEQ_1:def 3;
then A9: dom (p + q) = dom p by POLYNOM1:5;
then A10: len (p + q) = n by A8, FINSEQ_1:def 3;
A11: 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; :: thesis: ( [i,j] in Indices (M1 + M2) & i <= j implies (M1 + M2) * i,j = (p + q) . (((j - i) mod (len (p + q))) + 1) )
assume B1: ( [i,j] in Indices (M1 + M2) & i <= j ) ; :: thesis: (M1 + M2) * i,j = (p + q) . (((j - i) mod (len (p + q))) + 1)
then B23: ( ((j - i) mod (len (p + q))) + 1 in dom p & ((j - i) mod (len (p + q))) + 1 in dom (p + q) & ((j - i) mod (len (p + q))) + 1 in dom q ) by A8, A9, A6, Lm2;
(M1 + M2) * i,j = (M1 * i,j) + (M2 * i,j) by B1, A6, MATRIX_3:def 3
.= the addF of K . (M1 * i,j),(q . (((j - i) mod (len q)) + 1)) by B1, A6, A3, Def10
.= the addF of K . (p . (((j - i) mod (len (p + q))) + 1)),(q . (((j - i) mod (len (p + q))) + 1)) by A2, A3, A6, A10, B1, Def10
.= (p + q) . (((j - i) mod (len (p + q))) + 1) by B23, FUNCOP_1:28 ;
hence (M1 + M2) * i,j = (p + q) . (((j - i) mod (len (p + q))) + 1) ; :: thesis: verum

end;

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; :: thesis: ( [i,j] in Indices (M1 + M2) & i >= j implies (M1 + M2) * i,j = (- (p + q)) . (((j - i) mod (len (p + q))) + 1) )
assume B1: ( [i,j] in Indices (M1 + M2) & i >= j ) ; :: thesis: (M1 + M2) * i,j = (- (p + q)) . (((j - i) mod (len (p + q))) + 1)
B3: dom ((- p) + (- q)) = dom (- p) by A8, POLYNOM1:5;
B23: ( ((j - i) mod (len (p + q))) + 1 in dom p & ((j - i) mod (len (p + q))) + 1 in dom ((- p) + (- q)) & ((j - i) mod (len (p + q))) + 1 in dom (- q) & ((j - i) mod (len (p + q))) + 1 in dom (- p) ) by B3, B1, A8, A9, A6, Lm2;
(M1 + M2) * i,j = (M1 * i,j) + (M2 * i,j) by B1, A6, MATRIX_3:def 3
.= the addF of K . (M1 * i,j),((- q) . (((j - i) mod (len q)) + 1)) by B1, A6, A3, Def10
.= the addF of K . ((- p) . (((j - i) mod (len (p + q))) + 1)),((- q) . (((j - i) mod (len (p + q))) + 1)) by A2, A3, A6, A10, B1, Def10
.= ((- p) + (- q)) . (((j - i) mod (len (p + q))) + 1) by B23, FUNCOP_1:28
.= (- (p + q)) . (((j - i) mod (len (p + q))) + 1) by E1, E2, A2, A6, A3, FVSUM_1:40 ;
hence (M1 + M2) * i,j = (- (p + q)) . (((j - i) mod (len (p + q))) + 1) ; :: thesis: verum

end;

then A12: M1 + M2 is_anti-circular_about p + q by A6, A10, A11, Def10;
set r = p + q;
consider r being FinSequence of K such that
A13: ( len r = width (M1 + M2) & M1 + M2 is_anti-circular_about r ) by A6, A10, A12;
take r ; :: according to MATRIX16:def 10 :: thesis: ( 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 A13; :: thesis: verum