let n be Element of NAT ; :: thesis: for K being Field
for M1 being Matrix of n,K st M1 is anti-circular holds
- M1 is anti-circular
let K be Field; :: thesis: for M1 being Matrix of n,K st M1 is anti-circular holds
- M1 is anti-circular
let M1 be Matrix of n,K; :: thesis: ( M1 is anti-circular implies - M1 is anti-circular )
assume A1: M1 is anti-circular ; :: thesis: - M1 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;
A4: ( Indices M1 = [:(Seg n),(Seg n):] & len M1 = n & width M1 = n & Indices (- M1) = [:(Seg n),(Seg n):] & len (- M1) = n & width (- M1) = n ) by MATRIX_1:25;
p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:110;
then E1: - p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:133;
then A6: len (- p) = len p by FINSEQ_1:def 18;
then E2: ( dom p = Seg (len p) & dom (- p) = Seg (len p) ) by FINSEQ_1:def 3;
set r = - p;
A7: for i, j being Nat st [i,j] in Indices (- M1) & i <= j holds
(- M1) * i,j = (- p) . (((j - i) mod (len (- p))) + 1)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (- M1) & i <= j implies (- M1) * i,j = (- p) . (((j - i) mod (len (- p))) + 1) )
assume B1: ( [i,j] in Indices (- M1) & i <= j ) ; :: thesis: (- M1) * i,j = (- p) . (((j - i) mod (len (- p))) + 1)
((j - i) mod n) + 1 in Seg n by B1, A4, Lm2;
then B23: ((j - i) mod (len p)) + 1 in dom p by A4, A2, FINSEQ_1:def 3;
(- M1) * i,j = - (M1 * i,j) by B1, A4, MATRIX_3:def 2
.= (comp K) . (M1 * i,j) by VECTSP_1:def 25
.= (comp K) . (p . (((j - i) mod (len p)) + 1)) by B1, A4, A2, Def10
.= (- p) . (((j - i) mod (len p)) + 1) by B23, FUNCT_1:23 ;
hence (- M1) * i,j = (- p) . (((j - i) mod (len (- p))) + 1) by E1, FINSEQ_1:def 18; :: thesis: verum

end;

for i, j being Nat st [i,j] in Indices (- M1) & i >= j holds
(- M1) * i,j = (- (- p)) . (((j - i) mod (len (- p))) + 1)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (- M1) & i >= j implies (- M1) * i,j = (- (- p)) . (((j - i) mod (len (- p))) + 1) )
assume B1: ( [i,j] in Indices (- M1) & i >= j ) ; :: thesis: (- M1) * i,j = (- (- p)) . (((j - i) mod (len (- p))) + 1)
B2: ((j - i) mod n) + 1 in Seg n by B1, A4, Lm2;
(- M1) * i,j = - (M1 * i,j) by B1, A4, MATRIX_3:def 2
.= (comp K) . (M1 * i,j) by VECTSP_1:def 25
.= (comp K) . ((- p) . (((j - i) mod (len p)) + 1)) by B1, A4, A2, Def10
.= (- (- p)) . (((j - i) mod (len p)) + 1) by E2, B2, A4, A2, FUNCT_1:23 ;
hence (- M1) * i,j = (- (- p)) . (((j - i) mod (len (- p))) + 1) by E1, FINSEQ_1:def 18; :: thesis: verum

end;

then A9: - M1 is_anti-circular_about - p by A4, A2, A6, A7, Def10;
consider r being FinSequence of K such that
A10: ( len r = width (- M1) & - M1 is_anti-circular_about r ) by A4, A2, A6, A9;
take r ; :: according to MATRIX16:def 10 :: thesis: ( len r = width (- M1) & - M1 is_anti-circular_about r )
thus ( len r = width (- M1) & - M1 is_anti-circular_about r ) by A10; :: thesis: verum