let K be Field; for V1, V2 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for v1 being Element of V1
for M being Matrix of len b1, len b2,K st len b1 > 0 holds
LineVec2Mx (((Mx2Tran (M,b1,b2)) . v1) |-- b2) = (LineVec2Mx (v1 |-- b1)) * M
let V1, V2 be finite-dimensional VectSp of K; for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for v1 being Element of V1
for M being Matrix of len b1, len b2,K st len b1 > 0 holds
LineVec2Mx (((Mx2Tran (M,b1,b2)) . v1) |-- b2) = (LineVec2Mx (v1 |-- b1)) * M
let b1 be OrdBasis of V1; for b2 being OrdBasis of V2
for v1 being Element of V1
for M being Matrix of len b1, len b2,K st len b1 > 0 holds
LineVec2Mx (((Mx2Tran (M,b1,b2)) . v1) |-- b2) = (LineVec2Mx (v1 |-- b1)) * M
let b2 be OrdBasis of V2; for v1 being Element of V1
for M being Matrix of len b1, len b2,K st len b1 > 0 holds
LineVec2Mx (((Mx2Tran (M,b1,b2)) . v1) |-- b2) = (LineVec2Mx (v1 |-- b1)) * M
let v1 be Element of V1; for M being Matrix of len b1, len b2,K st len b1 > 0 holds
LineVec2Mx (((Mx2Tran (M,b1,b2)) . v1) |-- b2) = (LineVec2Mx (v1 |-- b1)) * M
set L = LineVec2Mx (v1 |-- b1);
A1:
( width (LineVec2Mx (v1 |-- b1)) = len (v1 |-- b1) & len (v1 |-- b1) = len b1 )
by MATRIX_0:23, MATRLIN:def 7;
let M be Matrix of len b1, len b2,K; ( len b1 > 0 implies LineVec2Mx (((Mx2Tran (M,b1,b2)) . v1) |-- b2) = (LineVec2Mx (v1 |-- b1)) * M )
assume A2:
len b1 > 0
; LineVec2Mx (((Mx2Tran (M,b1,b2)) . v1) |-- b2) = (LineVec2Mx (v1 |-- b1)) * M
A3:
len M = len b1
by A2, MATRIX_0:23;
set LM = (LineVec2Mx (v1 |-- b1)) * M;
width M = len b2
by A2, MATRIX_0:23;
then
width ((LineVec2Mx (v1 |-- b1)) * M) = len b2
by A1, A3, MATRIX_3:def 4;
then
len (Line (((LineVec2Mx (v1 |-- b1)) * M),1)) = len b2
by CARD_1:def 7;
then A4:
(Sum (lmlt ((Line (((LineVec2Mx (v1 |-- b1)) * M),1)),b2))) |-- b2 = Line (((LineVec2Mx (v1 |-- b1)) * M),1)
by MATRLIN:36;
len (LineVec2Mx (v1 |-- b1)) = 1
by MATRIX_0:23;
then
len ((LineVec2Mx (v1 |-- b1)) * M) = 1
by A1, A3, MATRIX_3:def 4;
hence (LineVec2Mx (v1 |-- b1)) * M =
LineVec2Mx ((Sum (lmlt ((Line (((LineVec2Mx (v1 |-- b1)) * M),1)),b2))) |-- b2)
by A4, MATRIX15:25
.=
LineVec2Mx (((Mx2Tran (M,b1,b2)) . v1) |-- b2)
by Def3
;
verum