let V be free finite-rank Z_Module; :: thesis: for b1, b2 being OrdBasis of V
for M being Matrix of rank V,INT.Ring st M = AutMt ((id V),b1,b2) holds
|.(Det M).| = 1
let b1, b2 be OrdBasis of V; :: thesis: for M being Matrix of rank V,INT.Ring st M = AutMt ((id V),b1,b2) holds
|.(Det M).| = 1
let M be Matrix of rank V,INT.Ring; :: thesis: ( M = AutMt ((id V),b1,b2) implies |.(Det M).| = 1 )
assume AS1: M = AutMt ((id V),b1,b2) ; :: thesis: |.(Det M).| = 1
per cases ( rank V = 0 or rank V > 0 ) ;
suppose rank V = 0 ; :: thesis: |.(Det M).| = 1
then Det M = 1. INT.Ring by MATRIXR2:41;
hence |.(Det M).| = 1 by ABSVALUE:def 1; :: thesis: verum
end;
suppose AS2: rank V > 0 ; :: thesis: |.(Det M).| = 1
then as2: rank V >= 1 + 0 by NAT_1:13;
B0: len b1 = rank V by ThRank1;
B1: len (AutMt ((id V),b2,b1)) = len b2 by Def8
.= rank V by ThRank1 ;
len b2 = rank V by ThRank1;
then width (AutMt ((id V),b2,b1)) = len b1 by AS2, Th39;
then reconsider M2 = AutMt ((id V),b2,b1) as Matrix of rank V,INT.Ring by AS2, B0, B1, MATRIX_0:20;
M = AutMt ((id V),b1,b2) by AS1;
then A1: M * M2 = 1. (INT.Ring,(rank V)) by AS2, LmSign3;
reconsider MM2 = M * M2 as Matrix of rank V,INT.Ring ;
A2: (Det M) * (Det M2) = Det MM2 by MATRIX11:62, AS2
.= 1_ INT.Ring by A1, MATRIX_7:16, as2
.= 1. INT.Ring ;
reconsider i = Det M as Integer ;
reconsider j = Det M2 as Integer ;
i * j = 1 by A2;
then ( ( i = 1 & j = 1 ) or ( i = - 1 & j = - 1 ) ) by INT_1:9;
then ( |.i.| = 1 or |.i.| = - (- 1) ) by ABSVALUE:def 1;
hence |.(Det M).| = 1 ; :: thesis: verum
end;
end;