let K be Field; :: thesis: for V2, V1 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 V2, V1 be finite-dimensional VectSp of K; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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_1:23, MATRLIN:def 7;
let M be Matrix of len b1, len b2,K; :: thesis: ( len b1 > 0 implies LineVec2Mx (((Mx2Tran (M,b1,b2)) . v1) |-- b2) = (LineVec2Mx (v1 |-- b1)) * M )
assume A2: len b1 > 0 ; :: thesis: LineVec2Mx (((Mx2Tran (M,b1,b2)) . v1) |-- b2) = (LineVec2Mx (v1 |-- b1)) * M
A3: len M = len b1 by A2, MATRIX_1:23;
set LM = (LineVec2Mx (v1 |-- b1)) * M;
width M = len b2 by A2, MATRIX_1: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_1: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 ;
:: thesis: verum