let n be Element of NAT ; :: thesis: for K being Field
for a being Element of K
for M1 being Matrix of n,K st M1 is anti-circular holds
a * M1 is anti-circular
let K be Field; :: thesis: for a being Element of K
for M1 being Matrix of n,K st M1 is anti-circular holds
a * M1 is anti-circular
let a be Element of K; :: thesis: for M1 being Matrix of n,K st M1 is anti-circular holds
a * M1 is anti-circular
let M1 be Matrix of n,K; :: thesis: ( M1 is anti-circular implies a * M1 is anti-circular )
assume A1: M1 is anti-circular ; :: thesis: a * 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 ) by MATRIX_1:25;
A5: ( Indices (a * M1) = [:(Seg n),(Seg n):] & len (a * M1) = n & width (a * M1) = n ) by MATRIX_1:25;
A6: ( len (a * p) = len p & len p = n ) by A2, MATRIXR1:16, MATRIX_1:25;
A7: ( dom p = Seg n & dom (a * p) = Seg (len (a * p)) & dom p = Seg (len p) ) by A2, A4, FINSEQ_1:def 3;
A8: for i, j being Nat st [i,j] in Indices (a * M1) & i <= j holds
(a * M1) * i,j = (a * p) . (((j - i) mod (len (a * p))) + 1)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (a * M1) & i <= j implies (a * M1) * i,j = (a * p) . (((j - i) mod (len (a * p))) + 1) )
assume B1: ( [i,j] in Indices (a * M1) & i <= j ) ; :: thesis: (a * M1) * i,j = (a * p) . (((j - i) mod (len (a * p))) + 1)
then B2: [i,j] in Indices M1 by A5, MATRIX_1:25;
B3: ((j - i) mod n) + 1 in Seg n by B1, A5, Lm2;
then B23: ( ((j - i) mod (len p)) + 1 in dom (a * p) & ((j - i) mod (len p)) + 1 in dom p ) by A4, A7, A2, MATRIXR1:16;
(a * M1) * i,j = a * (M1 * i,j) by B2, MATRIX_3:def 5
.= (a multfield ) . (M1 * i,j) by FVSUM_1:61
.= (a multfield ) . (p . (((j - i) mod (len p)) + 1)) by B1, B2, A2, Def10
.= (a multfield ) . (p /. (((j - i) mod (len p)) + 1)) by B3, A4, A7, A2, PARTFUN1:def 8
.= a * (p /. (((j - i) mod (len p)) + 1)) by FVSUM_1:61
.= (a * p) /. (((j - i) mod (len p)) + 1) by B3, A4, A7, A2, POLYNOM1:def 2
.= (a * p) . (((j - i) mod (len p)) + 1) by B23, PARTFUN1:def 8 ;
hence (a * M1) * i,j = (a * p) . (((j - i) mod (len (a * p))) + 1) by MATRIXR1:16; :: thesis: verum

end;

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

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (a * M1) & i >= j implies (a * M1) * i,j = (- (a * p)) . (((j - i) mod (len (a * p))) + 1) )
assume B1: ( [i,j] in Indices (a * M1) & i >= j ) ; :: thesis: (a * M1) * i,j = (- (a * p)) . (((j - i) mod (len (a * p))) + 1)
then B2: [i,j] in Indices M1 by A5, MATRIX_1:25;
B3: ((j - i) mod n) + 1 in Seg n by B1, A5, Lm2;
D: ( p is Element of n -tuples_on the carrier of K & a * p is Element of n -tuples_on the carrier of K ) by A6, FINSEQ_2:110;
then - p is Element of (len p) -tuples_on the carrier of K by A6, FINSEQ_2:133;
then len (- p) = len p by FINSEQ_1:def 18;
then B7: ( dom (- p) = Seg n & dom (- p) = dom p ) by A7, FINSEQ_1:def 3;
len (a * (- p)) = len (- p) by MATRIXR1:16;
then B8: dom (a * (- p)) = Seg (len (- p)) by FINSEQ_1:def 3
.= dom (- p) by FINSEQ_1:def 3 ;
(a * M1) * i,j = a * (M1 * i,j) by B2, MATRIX_3:def 5
.= (a multfield ) . (M1 * i,j) by FVSUM_1:61
.= (a multfield ) . ((- p) . (((j - i) mod (len p)) + 1)) by B1, B2, A2, Def10
.= (a multfield ) . ((- p) /. (((j - i) mod (len p)) + 1)) by B3, A4, A2, B7, PARTFUN1:def 8
.= a * ((- p) /. (((j - i) mod (len p)) + 1)) by FVSUM_1:61
.= (a * (- p)) /. (((j - i) mod (len p)) + 1) by B3, A4, A2, B7, POLYNOM1:def 2
.= (a * (- p)) . (((j - i) mod (len p)) + 1) by B3, A4, A2, B7, B8, PARTFUN1:def 8
.= (a * ((- (1_ K)) * p)) . (((j - i) mod (len p)) + 1) by D, FVSUM_1:72
.= ((a * (- (1_ K))) * p) . (((j - i) mod (len p)) + 1) by D, FVSUM_1:67
.= ((- (a * (1_ K))) * p) . (((j - i) mod (len p)) + 1) by VECTSP_1:40
.= ((- a) * p) . (((j - i) mod (len p)) + 1) by VECTSP_1:def 16
.= ((- ((1_ K) * a)) * p) . (((j - i) mod (len p)) + 1) by VECTSP_1:def 16
.= (((- (1_ K)) * a) * p) . (((j - i) mod (len p)) + 1) by VECTSP_1:41
.= ((- (1_ K)) * (a * p)) . (((j - i) mod (len p)) + 1) by D, FVSUM_1:67
.= (- (a * p)) . (((j - i) mod (len p)) + 1) by D, FVSUM_1:72 ;
hence (a * M1) * i,j = (- (a * p)) . (((j - i) mod (len (a * p))) + 1) by MATRIXR1:16; :: thesis: verum

end;

then A9: a * M1 is_anti-circular_about a * p by A5, A6, A8, Def10;
set q = a * p;
consider q being FinSequence of K such that
A11: ( len q = width (a * M1) & a * M1 is_anti-circular_about q ) by A5, A6, A9;
take q ; :: according to MATRIX16:def 10 :: thesis: ( len q = width (a * M1) & a * M1 is_anti-circular_about q )
thus ( len q = width (a * M1) & a * M1 is_anti-circular_about q ) by A11; :: thesis: verum