let V be free finite-rank Z_Module; :: thesis: for b1 being OrdBasis of V st rank V > 0 holds
AutMt ((id V),b1,b1) = 1. (INT.Ring,(rank V))
let b1 be OrdBasis of V; :: thesis: ( rank V > 0 implies AutMt ((id V),b1,b1) = 1. (INT.Ring,(rank V)) )
assume AS: rank V > 0 ; :: thesis: AutMt ((id V),b1,b1) = 1. (INT.Ring,(rank V))
B0: len b1 = rank V by ThRank1;
B1: len (AutMt ((id V),b1,b1)) = rank V by B0, Def8;
B3: width (AutMt ((id V),b1,b1)) = rank V by AS, B0, Th39;
P1: len (AutMt ((id V),b1,b1)) = len (1. (INT.Ring,(rank V))) by B1, MATRIX_0:24;
P4: dom (AutMt ((id V),b1,b1)) = Seg (len (AutMt ((id V),b1,b1))) by FINSEQ_1:def 3
.= dom (1. (INT.Ring,(rank V))) by P1, FINSEQ_1:def 3 ;
P2: width (AutMt ((id V),b1,b1)) = width (1. (INT.Ring,(rank V))) by B3, MATRIX_0:24;
P5: Indices (AutMt ((id V),b1,b1)) = Indices (1. (INT.Ring,(rank V))) by B3, P4, MATRIX_0:24;
X2: now :: thesis: for i, j being Nat st [i,j] in Indices (AutMt ((id V),b1,b1)) holds
( ( i <> j implies (AutMt ((id V),b1,b1)) * (i,j) = 0 ) & ( i = j implies (AutMt ((id V),b1,b1)) * (i,j) = 1 ) )
let i, j be Nat; :: thesis: ( [i,j] in Indices (AutMt ((id V),b1,b1)) implies ( ( i <> j implies (AutMt ((id V),b1,b1)) * (i,j) = 0 ) & ( i = j implies (AutMt ((id V),b1,b1)) * (i,j) = 1 ) ) )
assume X20: [i,j] in Indices (AutMt ((id V),b1,b1)) ; :: thesis: ( ( i <> j implies (AutMt ((id V),b1,b1)) * (i,j) = 0 ) & ( i = j implies (AutMt ((id V),b1,b1)) * (i,j) = 1 ) )
then X21: ( i in dom (AutMt ((id V),b1,b1)) & j in Seg (width (AutMt ((id V),b1,b1))) ) by ZFMISC_1:87;
dom (AutMt ((id V),b1,b1)) = Seg (len (AutMt ((id V),b1,b1))) by FINSEQ_1:def 3
.= Seg (len b1) by Def8
.= dom b1 by FINSEQ_1:def 3 ;
then X23: i in dom b1 by X20, ZFMISC_1:87;
width (AutMt ((id V),b1,b1)) = len b1 by Th39, AS, B0;
then Y23: j in dom b1 by X21, FINSEQ_1:def 3;
X25: (AutMt ((id V),b1,b1)) /. i = ((id V) . (b1 /. i)) |-- b1 by Def8, X23;
consider q being FinSequence of INT such that
X26: ( q = (AutMt ((id V),b1,b1)) . i & (AutMt ((id V),b1,b1)) * (i,j) = q . j ) by MATRIX_0:def 5, X20;
X27: (AutMt ((id V),b1,b1)) * (i,j) = ((b1 /. i) |-- b1) . j by X21, X25, X26, PARTFUN1:def 6;
thus ( i <> j implies (AutMt ((id V),b1,b1)) * (i,j) = 0 ) by X23, X27, Y23, LmSign31X; :: thesis: ( i = j implies (AutMt ((id V),b1,b1)) * (i,j) = 1 )
thus ( i = j implies (AutMt ((id V),b1,b1)) * (i,j) = 1 ) by X23, X27, LmSign31X; :: thesis: verum
end;
for i, j being Nat st [i,j] in Indices (AutMt ((id V),b1,b1)) holds
(AutMt ((id V),b1,b1)) * (i,j) = (1. (INT.Ring,(rank V))) * (i,j)
proof
let i, j be Nat; :: thesis: ( [i,j] in Indices (AutMt ((id V),b1,b1)) implies (AutMt ((id V),b1,b1)) * (i,j) = (1. (INT.Ring,(rank V))) * (i,j) )
assume P6: [i,j] in Indices (AutMt ((id V),b1,b1)) ; :: thesis: (AutMt ((id V),b1,b1)) * (i,j) = (1. (INT.Ring,(rank V))) * (i,j)
per cases ( i <> j or i = j ) ;
suppose P8: i <> j ; :: thesis: (AutMt ((id V),b1,b1)) * (i,j) = (1. (INT.Ring,(rank V))) * (i,j)
then (1. (INT.Ring,(rank V))) * (i,j) = 0. INT.Ring by P5, P6, MATRIX_1:def 3;
hence (AutMt ((id V),b1,b1)) * (i,j) = (1. (INT.Ring,(rank V))) * (i,j) by P6, P8, X2; :: thesis: verum
end;
suppose P10: i = j ; :: thesis: (AutMt ((id V),b1,b1)) * (i,j) = (1. (INT.Ring,(rank V))) * (i,j)
then (1. (INT.Ring,(rank V))) * (i,j) = 1. INT.Ring by P5, P6, MATRIX_1:def 3;
hence (AutMt ((id V),b1,b1)) * (i,j) = (1. (INT.Ring,(rank V))) * (i,j) by P6, P10, X2; :: thesis: verum
end;
end;
end;
hence AutMt ((id V),b1,b1) = 1. (INT.Ring,(rank V)) by P1, P2, EQ40; :: thesis: verum