let V be free finite-rank Z_Module; for b1, b2 being OrdBasis of V
for f being bilinear-FrForm of V,V st 0 < rank V holds
BilinearM (f,b2,b2) = ((inttorealM (AutMt ((id V),b2,b1))) * (BilinearM (f,b1,b1))) * ((inttorealM (AutMt ((id V),b2,b1))) @)
let b1, b2 be OrdBasis of V; for f being bilinear-FrForm of V,V st 0 < rank V holds
BilinearM (f,b2,b2) = ((inttorealM (AutMt ((id V),b2,b1))) * (BilinearM (f,b1,b1))) * ((inttorealM (AutMt ((id V),b2,b1))) @)
let f be bilinear-FrForm of V,V; ( 0 < rank V implies BilinearM (f,b2,b2) = ((inttorealM (AutMt ((id V),b2,b1))) * (BilinearM (f,b1,b1))) * ((inttorealM (AutMt ((id V),b2,b1))) @) )
set I = inttorealM (AutMt ((id V),b2,b1));
assume AS:
0 < rank V
; BilinearM (f,b2,b2) = ((inttorealM (AutMt ((id V),b2,b1))) * (BilinearM (f,b1,b1))) * ((inttorealM (AutMt ((id V),b2,b1))) @)
set n = len b1;
A1:
len b1 = rank V
by ZMATRLIN:49;
reconsider IM1 = AutMt ((id V),b2,b1) as Matrix of len b1,INT.Ring by ZMATRLIN:50, A1;
reconsider IM2 = AutMt ((id V),b2,b1) as Matrix of len b1,INT.Ring by ZMATRLIN:50, A1;
reconsider M1 = IM1 @ as Matrix of len b1,INT.Ring ;
reconsider M2 = IM2 as Matrix of len b1,INT.Ring ;
Y1:
width IM1 = len b1
by MATRIX_0:24;
Yb:
width (BilinearM (f,b1,b1)) = len b1
by MATRIX_0:24;
( width (AutMt ((id V),b2,b1)) = len (BilinearM (f,b1,b1)) & width (BilinearM (f,b1,b1)) = len ((AutMt ((id V),b2,b1)) @) )
by MATRIX_0:def 2, Y1, Yb;
then X1:
( width (inttorealM (AutMt ((id V),b2,b1))) = len (BilinearM (f,b1,b1)) & width (BilinearM (f,b1,b1)) = len ((inttorealM (AutMt ((id V),b2,b1))) @) )
by ZMATRLIN:6;
thus BilinearM (f,b2,b2) =
(inttorealM (AutMt ((id V),b2,b1))) * (BilinearM (f,b1,b2))
by ThMBF2, AS
.=
(inttorealM (AutMt ((id V),b2,b1))) * ((BilinearM (f,b1,b1)) * ((inttorealM (AutMt ((id V),b2,b1))) @))
by ThMBF1, AS
.=
((inttorealM (AutMt ((id V),b2,b1))) * (BilinearM (f,b1,b1))) * ((inttorealM (AutMt ((id V),b2,b1))) @)
by MATRIX_3:33, X1
; verum