let V be free finite-rank Z_Module; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: verum