let K be Field; for V1, V2 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for B2 being FinSequence of V2
for v1 being Element of V1
for M being Matrix of len b1, len B2,K st len b1 = 0 holds
(Mx2Tran (M,b1,B2)) . v1 = 0. V2
let V1, V2 be finite-dimensional VectSp of K; for b1 being OrdBasis of V1
for B2 being FinSequence of V2
for v1 being Element of V1
for M being Matrix of len b1, len B2,K st len b1 = 0 holds
(Mx2Tran (M,b1,B2)) . v1 = 0. V2
let b1 be OrdBasis of V1; for B2 being FinSequence of V2
for v1 being Element of V1
for M being Matrix of len b1, len B2,K st len b1 = 0 holds
(Mx2Tran (M,b1,B2)) . v1 = 0. V2
let B2 be FinSequence of V2; for v1 being Element of V1
for M being Matrix of len b1, len B2,K st len b1 = 0 holds
(Mx2Tran (M,b1,B2)) . v1 = 0. V2
let v1 be Element of V1; for M being Matrix of len b1, len B2,K st len b1 = 0 holds
(Mx2Tran (M,b1,B2)) . v1 = 0. V2
let M be Matrix of len b1, len B2,K; ( len b1 = 0 implies (Mx2Tran (M,b1,B2)) . v1 = 0. V2 )
assume A1:
len b1 = 0
; (Mx2Tran (M,b1,B2)) . v1 = 0. V2
set L = LineVec2Mx (v1 |-- b1);
set LM = (LineVec2Mx (v1 |-- b1)) * M;
set LL = Line (((LineVec2Mx (v1 |-- b1)) * M),1);
A2:
( width (LineVec2Mx (v1 |-- b1)) = len (v1 |-- b1) & len (v1 |-- b1) = len b1 )
by MATRIX_0:23, MATRLIN:def 7;
A3:
len M = len b1
by MATRIX_0:def 2;
then
width M = 0
by A1, MATRIX_0:def 3;
then
width ((LineVec2Mx (v1 |-- b1)) * M) = 0
by A2, A3, MATRIX_3:def 4;
then A4:
dom (Line (((LineVec2Mx (v1 |-- b1)) * M),1)) = {}
;
dom (lmlt ((Line (((LineVec2Mx (v1 |-- b1)) * M),1)),B2)) = (dom (Line (((LineVec2Mx (v1 |-- b1)) * M),1))) /\ (dom B2)
by Lm1;
then
lmlt ((Line (((LineVec2Mx (v1 |-- b1)) * M),1)),B2) = <*> the carrier of V2
by A4;
then
Sum (lmlt ((Line (((LineVec2Mx (v1 |-- b1)) * M),1)),B2)) = 0. V2
by RLVECT_1:43;
hence
(Mx2Tran (M,b1,B2)) . v1 = 0. V2
by Def3; verum