let V be free finite-rank Z_Module; for b1, b2 being OrdBasis of V
for f being bilinear-Form of V,V holds |.(Det (BilinearM (f,b2,b2))).| = |.(Det (BilinearM (f,b1,b1))).|
let b1, b2 be OrdBasis of V; for f being bilinear-Form of V,V holds |.(Det (BilinearM (f,b2,b2))).| = |.(Det (BilinearM (f,b1,b1))).|
let f be bilinear-Form of V,V; |.(Det (BilinearM (f,b2,b2))).| = |.(Det (BilinearM (f,b1,b1))).|
set n = len b1;
A1:
len b1 = rank V
by ThRank1;
A2:
len b2 = rank V
by ThRank1;
reconsider B1 = BilinearM (f,b1,b1) as Matrix of len b1,INT.Ring ;
reconsider B2 = BilinearM (f,b2,b2) as Matrix of len b1,INT.Ring by A1, A2;
per cases
( rank V = 0 or rank V > 0 )
;
suppose ZZ:
rank V > 0
;
|.(Det (BilinearM (f,b2,b2))).| = |.(Det (BilinearM (f,b1,b1))).|then B2:
BilinearM (
f,
b2,
b2)
= ((AutMt ((id V),b2,b1)) * (BilinearM (f,b1,b1))) * ((AutMt ((id V),b2,b1)) @)
by ThMBF3;
reconsider IM1 =
AutMt (
(id V),
b2,
b1) as
Matrix of
len b1,
INT.Ring by A1, LMThMBF3;
reconsider IM2 =
AutMt (
(id V),
b2,
b1) as
Matrix of
len b1,
INT.Ring by A1, LMThMBF3;
reconsider M1 =
IM1 @ as
Matrix of
len b1,
INT.Ring ;
reconsider M2 =
IM2 as
Matrix of
len b1,
INT.Ring ;
len b1 >= 1
+ 0
by A1, ZZ, NAT_1:13;
then X1:
Det IM1 = Det M1
by MATRIX_7:37;
reconsider M2B1 =
M2 * B1 as
Matrix of
len b1,
INT.Ring ;
Det B2 =
(Det M2B1) * (Det M1)
by B2, MATRIX11:62, ZZ, A1
.=
((Det M2) * (Det B1)) * (Det M1)
by ZZ, A1, MATRIX11:62
;
hence |.(Det (BilinearM (f,b2,b2))).| =
|.((Det M2) * (Det B1)).| * |.(Det M1).|
by A1, A2, COMPLEX1:65
.=
|.((Det M2) * (Det B1)).| * 1
by A1, X1, ThSign1
.=
|.(Det M2).| * |.(Det B1).|
by COMPLEX1:65
.=
|.(Det B1).| * 1
by A1, ThSign1
.=
|.(Det (BilinearM (f,b1,b1))).|
;
verum end;