let V be free finite-rank Z_Module; :: thesis: for b1, b2 being OrdBasis of V
for f being bilinear-Form of V,V st 0 < rank V holds
BilinearM (f,b2,b2) = ((AutMt ((id V),b2,b1)) * (BilinearM (f,b1,b1))) * ((AutMt ((id V),b2,b1)) @)
let b1, b2 be OrdBasis of V; :: thesis: for f being bilinear-Form of V,V st 0 < rank V holds
BilinearM (f,b2,b2) = ((AutMt ((id V),b2,b1)) * (BilinearM (f,b1,b1))) * ((AutMt ((id V),b2,b1)) @)
let f be bilinear-Form of V,V; :: thesis: ( 0 < rank V implies BilinearM (f,b2,b2) = ((AutMt ((id V),b2,b1)) * (BilinearM (f,b1,b1))) * ((AutMt ((id V),b2,b1)) @) )
assume AS: 0 < rank V ; :: thesis: BilinearM (f,b2,b2) = ((AutMt ((id V),b2,b1)) * (BilinearM (f,b1,b1))) * ((AutMt ((id V),b2,b1)) @)
set n = len b1;
A1: len b1 = rank V by ThRank1;
reconsider IM1 = AutMt ((id V),b2,b1) as Matrix of len b1,INT.Ring by LMThMBF3, A1;
reconsider IM2 = AutMt ((id V),b2,b1) as Matrix of len b1,INT.Ring by LMThMBF3, 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;
X1: ( 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;
thus BilinearM (f,b2,b2) = (AutMt ((id V),b2,b1)) * (BilinearM (f,b1,b2)) by ThMBF2, AS
.= (AutMt ((id V),b2,b1)) * ((BilinearM (f,b1,b1)) * ((AutMt ((id V),b2,b1)) @)) by ThMBF1, AS
.= ((AutMt ((id V),b2,b1)) * (BilinearM (f,b1,b1))) * ((AutMt ((id V),b2,b1)) @) by MATRIX_3:33, X1 ; :: thesis: verum