let V1, V2 be free finite-rank Z_Module; for b1 being OrdBasis of V1
for b2, b3 being OrdBasis of V2
for f being bilinear-Form of V1,V2 st 0 < rank V1 holds
BilinearM (f,b1,b3) = (BilinearM (f,b1,b2)) * ((AutMt ((id V2),b3,b2)) @)
let b1 be OrdBasis of V1; for b2, b3 being OrdBasis of V2
for f being bilinear-Form of V1,V2 st 0 < rank V1 holds
BilinearM (f,b1,b3) = (BilinearM (f,b1,b2)) * ((AutMt ((id V2),b3,b2)) @)
let b2, b3 be OrdBasis of V2; for f being bilinear-Form of V1,V2 st 0 < rank V1 holds
BilinearM (f,b1,b3) = (BilinearM (f,b1,b2)) * ((AutMt ((id V2),b3,b2)) @)
let f be bilinear-Form of V1,V2; ( 0 < rank V1 implies BilinearM (f,b1,b3) = (BilinearM (f,b1,b2)) * ((AutMt ((id V2),b3,b2)) @) )
assume AS:
0 < rank V1
; BilinearM (f,b1,b3) = (BilinearM (f,b1,b2)) * ((AutMt ((id V2),b3,b2)) @)
set n = len b2;
A2:
len b2 = rank V2
by ThRank1;
A3:
len b3 = rank V2
by ThRank1;
reconsider IM1 = AutMt ((id V2),b3,b2) as Matrix of len b2,INT.Ring by LMThMBF3, A2;
reconsider M1 = IM1 @ as Matrix of len b2,INT.Ring ;
set M2 = (BilinearM (f,b1,b2)) * M1;
B1:
( len M1 = len b2 & width M1 = len b2 & Indices M1 = [:(Seg (len b2)),(Seg (len b2)):] )
by MATRIX_0:24;
F1:
( len IM1 = len b2 & width IM1 = len b2 & Indices IM1 = [:(Seg (len b2)),(Seg (len b2)):] )
by MATRIX_0:24;
B2:
0 < len b1
by AS, ThRank1;
then B3:
( len (BilinearM (f,b1,b2)) = len b1 & width (BilinearM (f,b1,b2)) = len b2 )
by MATRIX_0:23;
C1:
width (BilinearM (f,b1,b2)) = len M1
by B1, B2, MATRIX_0:23;
( len ((BilinearM (f,b1,b2)) * M1) = len b1 & width ((BilinearM (f,b1,b2)) * M1) = len b2 )
by B1, B3, MATRIX_3:def 4;
then reconsider M2 = (BilinearM (f,b1,b2)) * M1 as Matrix of len b1, len b2,INT.Ring by B2, MATRIX_0:20;
set FM1 = M1;
set FBM = BilinearM (f,b1,b2);
for i, j being Nat st [i,j] in Indices (BilinearM (f,b1,b3)) holds
(BilinearM (f,b1,b3)) * (i,j) = M2 * (i,j)
proof
let i,
j be
Nat;
( [i,j] in Indices (BilinearM (f,b1,b3)) implies (BilinearM (f,b1,b3)) * (i,j) = M2 * (i,j) )
assume
[i,j] in Indices (BilinearM (f,b1,b3))
;
(BilinearM (f,b1,b3)) * (i,j) = M2 * (i,j)
then B6:
[i,j] in [:(Seg (len b1)),(Seg (len b3)):]
by B2, MATRIX_0:23;
then B7:
(
i in Seg (len b1) &
j in Seg (len b3) )
by ZFMISC_1:87;
then B8:
(
i in dom b1 &
j in dom b3 )
by FINSEQ_1:def 3;
then B9:
(BilinearM (f,b1,b3)) * (
i,
j)
= f . (
(b1 /. i),
(b3 /. j))
by defBilinearM;
[i,j] in Indices M2
by B2, B6, A2, A3, MATRIX_0:23;
then B11:
M2 * (
i,
j)
= (Line ((BilinearM (f,b1,b2)),i)) "*" (Col (M1,j))
by C1, MATRIX_3:def 4;
B12:
len (Line ((BilinearM (f,b1,b2)),i)) = len b2
by B3, MATRIX_0:def 7;
B13:
now for k being Nat st k in Seg (len b2) holds
(Line ((BilinearM (f,b1,b2)),i)) . k = f . ((b1 /. i),(b2 /. k))let k be
Nat;
( k in Seg (len b2) implies (Line ((BilinearM (f,b1,b2)),i)) . k = f . ((b1 /. i),(b2 /. k)) )assume B131:
k in Seg (len b2)
;
(Line ((BilinearM (f,b1,b2)),i)) . k = f . ((b1 /. i),(b2 /. k))then B132:
k in Seg (width (BilinearM (f,b1,b2)))
by B2, MATRIX_0:23;
B81:
k in dom b2
by FINSEQ_1:def 3, B131;
thus (Line ((BilinearM (f,b1,b2)),i)) . k =
(BilinearM (f,b1,b2)) * (
i,
k)
by B132, MATRIX_0:def 7
.=
f . (
(b1 /. i),
(b2 /. k))
by B8, B81, defBilinearM
;
verum end;
B14:
len (Col (M1,j)) = len b2
by B1, MATRIX_0:def 8;
B135:
j in Seg (len b2)
by B6, A2, A3, ZFMISC_1:87;
B15:
now for k being Nat st 1 <= k & k <= len (Col (M1,j)) holds
(Col (M1,j)) . k = ((b3 /. j) |-- b2) . klet k be
Nat;
( 1 <= k & k <= len (Col (M1,j)) implies (Col (M1,j)) . k = ((b3 /. j) |-- b2) . k )assume
( 1
<= k &
k <= len (Col (M1,j)) )
;
(Col (M1,j)) . k = ((b3 /. j) |-- b2) . kthen B131:
k in Seg (len b2)
by FINSEQ_1:1, B14;
then B132:
k in dom M1
by B1, FINSEQ_1:def 3;
B132A:
j in dom IM1
by B135, F1, FINSEQ_1:def 3;
Y1:
[j,k] in Indices IM1
by F1, B131, B135, ZFMISC_1:87;
then consider p being
FinSequence of
INT such that B133:
(
p = IM1 . j &
IM1 * (
j,
k)
= p . k )
by MATRIX_0:def 5;
B81A:
j in dom b3
by B7, FINSEQ_1:def 3;
X0:
(Col (M1,j)) . k =
M1 * (
k,
j)
by B132, MATRIX_0:def 8
.=
(AutMt ((id V2),b3,b2)) * (
j,
k)
by Y1, MATRIX_0:def 6
;
IM1 . j =
(AutMt ((id V2),b3,b2)) /. j
by B132A, PARTFUN1:def 6
.=
((id V2) . (b3 /. j)) |-- b2
by B81A, Def8
;
hence
(Col (M1,j)) . k = ((b3 /. j) |-- b2) . k
by B133, X0;
verum end;
len (Col (M1,j)) = len ((b3 /. j) |-- b2)
by B14, Def7;
hence
(BilinearM (f,b1,b3)) * (
i,
j)
= M2 * (
i,
j)
by B9, B11, B12, B13, B14, B15, LMThMBF1X, FINSEQ_1:def 17;
verum
end;
hence
BilinearM (f,b1,b3) = (BilinearM (f,b1,b2)) * ((AutMt ((id V2),b3,b2)) @)
by MATRIX_0:27, A2, A3; verum