let V be free finite-rank Z_Module; :: thesis: for b1, b2 being OrdBasis of V
for M being Matrix of rank V,F_Real st M = AutMt ((id V),b1,b2) holds
Det M in INT
let b1, b2 be OrdBasis of V; :: thesis: for M being Matrix of rank V,F_Real st M = AutMt ((id V),b1,b2) holds
Det M in INT
let M be Matrix of rank V,F_Real; :: thesis: ( M = AutMt ((id V),b1,b2) implies Det M in INT )
assume A2: M = AutMt ((id V),b1,b2) ; :: thesis: Det M in INT
per cases ( not 0 < rank V or 0 < rank V ) ;
suppose not 0 < rank V ; :: thesis: Det M in INT
then rank V = 0 ;
then Det M = 1. F_Real by MATRIXR2:41;
hence Det M in INT ; :: thesis: verum
end;
suppose A3: 0 < rank V ; :: thesis: Det M in INT
( len M = rank V & width M = rank V ) by MATRIX_0:24;
then M is Matrix of rank V,INT by A2, A3, MATRIX_0:20;
hence Det M in INT by LmSign1A; :: thesis: verum
end;
end;