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
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 A1: len b1 > 0 ; :: thesis: LineVec2Mx (((Mx2Tran M,b1,b2) . v1) |-- b2) = (LineVec2Mx (v1 |-- b1)) * M
set L = LineVec2Mx (v1 |-- b1);
set LM = (LineVec2Mx (v1 |-- b1)) * M;
( len (LineVec2Mx (v1 |-- b1)) = 1 & width (LineVec2Mx (v1 |-- b1)) = len (v1 |-- b1) & len (v1 |-- b1) = len b1 & len M = len b1 & width M = len b2 ) by A1, MATRIX_1:24, MATRLIN:def 9;
then A2: ( len ((LineVec2Mx (v1 |-- b1)) * M) = 1 & width ((LineVec2Mx (v1 |-- b1)) * M) = len b2 ) by MATRIX_3:def 4;
then A3: len (Line ((LineVec2Mx (v1 |-- b1)) * M),1) = len b2 by FINSEQ_1:def 18;
(Sum (lmlt (Line ((LineVec2Mx (v1 |-- b1)) * M),1),b2)) |-- b2 = Line ((LineVec2Mx (v1 |-- b1)) * M),1 by A3, MATRLIN:41;
hence (LineVec2Mx (v1 |-- b1)) * M = LineVec2Mx ((Sum (lmlt (Line ((LineVec2Mx (v1 |-- b1)) * M),1),b2)) |-- b2) by A2, MATRIX15:25
.= LineVec2Mx (((Mx2Tran M,b1,b2) . v1) |-- b2) by Def3 ;
:: thesis: verum