let V be free finite-rank Z_Module; :: thesis: for b1, b2 being OrdBasis of V
for f being bilinear-FrForm of V,V holds Det (BilinearM (f,b2,b2)) = Det (BilinearM (f,b1,b1))
let b1, b2 be OrdBasis of V; :: thesis: for f being bilinear-FrForm of V,V holds Det (BilinearM (f,b2,b2)) = Det (BilinearM (f,b1,b1))
let f be bilinear-FrForm of V,V; :: thesis: Det (BilinearM (f,b2,b2)) = Det (BilinearM (f,b1,b1))
set n = len b1;
A1: len b1 = rank V by ZMATRLIN:49;
A2: len b2 = rank V by ZMATRLIN:49;
reconsider B1 = BilinearM (f,b1,b1) as Matrix of len b1,F_Real ;
reconsider B2 = BilinearM (f,b2,b2) as Matrix of len b1,F_Real by A1, A2;
reconsider I1 = AutMt ((id V),b2,b1) as Matrix of len b1,INT.Ring by A1, ZMATRLIN:50;
set I = inttorealM I1;
per cases ( rank V = 0 or rank V > 0 ) ;
suppose rank V = 0 ; :: thesis: Det (BilinearM (f,b2,b2)) = Det (BilinearM (f,b1,b1))
hence Det (BilinearM (f,b2,b2)) = Det (BilinearM (f,b1,b1)) by A1, A2, MATRIX_0:45; :: thesis: verum
end;
suppose ZZ: rank V > 0 ; :: thesis: Det (BilinearM (f,b2,b2)) = Det (BilinearM (f,b1,b1))
then B2: BilinearM (f,b2,b2) = ((inttorealM I1) * (BilinearM (f,b1,b1))) * ((inttorealM I1) @) by ThMBF3;
set M1 = (inttorealM I1) @ ;
set M2 = inttorealM I1;
( width (inttorealM I1) = len b1 & len (inttorealM I1) = len b1 & width B1 = len b1 & len B1 = len b1 ) by MATRIX_0:24;
then ( width (inttorealM I1) = len B1 & len (inttorealM I1) > 0 & len B1 > 0 ) by ZZ, ZMATRLIN:49;
then reconsider M2B1 = (inttorealM I1) * B1 as Matrix of len b1,F_Real by MATRIX_4:64;
X2: ( ( Det (inttorealM I1) = 1 & Det ((inttorealM I1) @) = 1 ) or ( Det (inttorealM I1) = - 1 & Det ((inttorealM I1) @) = - 1 ) ) by A1, ThSign2;
thus Det (BilinearM (f,b2,b2)) = Det B2 by A1, ZMATRLIN:49
.= (Det M2B1) * (Det ((inttorealM I1) @)) by A1, B2, ZZ, MATRIX11:62
.= ((Det (inttorealM I1)) * (Det B1)) * (Det ((inttorealM I1) @)) by ZZ, A1, MATRIX11:62
.= Det (BilinearM (f,b1,b1)) by X2 ; :: thesis: verum
end;
end;