let K be Fanoian Field; :: thesis: for n, i, j being Nat
for M1 being Matrix of n,K st [i,j] in Indices M1 & i = j & M1 is anti-circular holds
M1 * i,j = 0. K
let n, i, j be Nat; :: thesis: for M1 being Matrix of n,K st [i,j] in Indices M1 & i = j & M1 is anti-circular holds
M1 * i,j = 0. K
let M1 be Matrix of n,K; :: thesis: ( [i,j] in Indices M1 & i = j & M1 is anti-circular implies M1 * i,j = 0. K )
assume A1: ( [i,j] in Indices M1 & i = j & M1 is anti-circular ) ; :: thesis: M1 * i,j = 0. K
consider p being FinSequence of K such that
A2: ( len p = width M1 & M1 is_anti-circular_about p ) by A1, Def11;
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 A5: len (- p) = len p by FINSEQ_1:def 18;
B1: ( len M1 = n & width M1 = n & Indices M1 = [:(Seg n),(Seg n):] ) by MATRIX_1:25;
then A6: ( dom p = Seg n & dom p = Seg (len p) & dom (- p) = Seg n ) by A2, A5, FINSEQ_1:def 3;
A7: ( ((j - i) mod (len p)) + 1 in dom p & ((j - i) mod (len p)) + 1 in dom (- p) ) by A1, B1, A6, Lm2;
A8: M1 * i,j = p . (((j - i) mod (len p)) + 1) by A1, A2, Def10;
A9: M1 * i,j = (- p) . (((j - i) mod (len p)) + 1) by A1, A2, Def10
.= (comp K) . (p . (((j - i) mod (len p)) + 1)) by A7, FUNCT_1:22
.= - (M1 * i,j) by A8, VECTSP_1:def 25 ;
A10: (1_ K) + (1_ K) <> 0. K by VECTSP_1:def 29;
(M1 * i,j) + (M1 * i,j) = 0. K by A9, RLVECT_1:16;
then ((1_ K) * (M1 * i,j)) + (M1 * i,j) = 0. K by VECTSP_1:def 19;
then ((1_ K) * (M1 * i,j)) + ((1_ K) * (M1 * i,j)) = 0. K by VECTSP_1:def 19;
then ((1_ K) + (1_ K)) * (M1 * i,j) = 0. K by VECTSP_1:def 18;
hence M1 * i,j = 0. K by A10, VECTSP_1:44; :: thesis: verum