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 that
A1: [i,j] in Indices M1 and
A2: i = j and
A3: M1 is anti-circular ; :: thesis: M1 * (i,j) = 0. K
consider p being FinSequence of K such that
A4: len p = width M1 and
A5: M1 is_anti-circular_about p by A3;
A6: M1 * (i,j) = p . (((j - i) mod (len p)) + 1) by A1, A2, A5;
A7: width M1 = n by MATRIX_0:24;
p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:92;
then - p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:113;
then len (- p) = len p by CARD_1:def 7;
then ( Indices M1 = [:(Seg n),(Seg n):] & dom (- p) = Seg n ) by A4, A7, FINSEQ_1:def 3, MATRIX_0:24;
then A8: ((j - i) mod (len p)) + 1 in dom (- p) by A1, A4, A7, Lm3;
M1 * (i,j) = (- p) . (((j - i) mod (len p)) + 1) by A1, A2, A5
.= (comp K) . (p . (((j - i) mod (len p)) + 1)) by A8, FUNCT_1:12
.= - (M1 * (i,j)) by A6, VECTSP_1:def 13 ;
then (M1 * (i,j)) + (M1 * (i,j)) = 0. K by RLVECT_1:5;
then ((1_ K) * (M1 * (i,j))) + (M1 * (i,j)) = 0. K ;
then ((1_ K) * (M1 * (i,j))) + ((1_ K) * (M1 * (i,j))) = 0. K ;
then ( (1_ K) + (1_ K) <> 0. K & ((1_ K) + (1_ K)) * (M1 * (i,j)) = 0. K ) by VECTSP_1:def 7, VECTSP_1:def 19;
hence M1 * (i,j) = 0. K by VECTSP_1:12; :: thesis: verum