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 A being Matrix of len b1, len b2,K st len b1 > 0 & len b2 > 0 holds
( v1 in ker (Mx2Tran A,b1,b2) iff v1 |-- b1 in Space_of_Solutions_of (A @ ) )
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 A being Matrix of len b1, len b2,K st len b1 > 0 & len b2 > 0 holds
( v1 in ker (Mx2Tran A,b1,b2) iff v1 |-- b1 in Space_of_Solutions_of (A @ ) )
let b1 be OrdBasis of V1; :: thesis: for b2 being OrdBasis of V2
for v1 being Element of V1
for A being Matrix of len b1, len b2,K st len b1 > 0 & len b2 > 0 holds
( v1 in ker (Mx2Tran A,b1,b2) iff v1 |-- b1 in Space_of_Solutions_of (A @ ) )
let b2 be OrdBasis of V2; :: thesis: for v1 being Element of V1
for A being Matrix of len b1, len b2,K st len b1 > 0 & len b2 > 0 holds
( v1 in ker (Mx2Tran A,b1,b2) iff v1 |-- b1 in Space_of_Solutions_of (A @ ) )
let v1 be Element of V1; :: thesis: for A being Matrix of len b1, len b2,K st len b1 > 0 & len b2 > 0 holds
( v1 in ker (Mx2Tran A,b1,b2) iff v1 |-- b1 in Space_of_Solutions_of (A @ ) )
let A be Matrix of len b1, len b2,K; :: thesis: ( len b1 > 0 & len b2 > 0 implies ( v1 in ker (Mx2Tran A,b1,b2) iff v1 |-- b1 in Space_of_Solutions_of (A @ ) ) )
assume that
A1: len b1 > 0 and
A2: len b2 > 0 ; :: thesis: ( v1 in ker (Mx2Tran A,b1,b2) iff v1 |-- b1 in Space_of_Solutions_of (A @ ) )
set AT = A @ ;
A3: width A = len b2 by A1, MATRIX_1:24;
then A4: len (A @ ) = len b2 by A2, MATRIX_2:12;
set L = LineVec2Mx (v1 |-- b1);
set M = Mx2Tran A,b1,b2;
set SA = Space_of_Solutions_of (A @ );
A5: width (LineVec2Mx (v1 |-- b1)) = len (v1 |-- b1) by MATRIX_1:24;
A6: len ((len b2) |-> (0. K)) = len b2 by FINSEQ_1:def 18;
then A7: width (LineVec2Mx ((len b2) |-> (0. K))) = len b2 by MATRIX_1:24;
A8: width (ColVec2Mx ((len b2) |-> (0. K))) = 1 by A2, A6, MATRIX_1:24;
A9: len (v1 |-- b1) = len b1 by MATRLIN:def 9;
then A10: ( len (ColVec2Mx (v1 |-- b1)) = len (v1 |-- b1) & width (ColVec2Mx (v1 |-- b1)) = 1 ) by A1, MATRIX_1:24;
A11: len A = len b1 by A1, MATRIX_1:24;
then A12: ( width (A @ ) = 0 implies len (A @ ) = 0 ) by A1, A2, A3, MATRIX_2:12;
A13: width (A @ ) = len b1 by A2, A11, A3, MATRIX_2:12;
thus ( v1 in ker (Mx2Tran A,b1,b2) implies v1 |-- b1 in Space_of_Solutions_of (A @ ) ) :: thesis: ( v1 |-- b1 in Space_of_Solutions_of (A @ ) implies v1 in ker (Mx2Tran A,b1,b2) )

proof

assume v1 in ker (Mx2Tran A,b1,b2) ; :: thesis: v1 |-- b1 in Space_of_Solutions_of (A @ )
then (Mx2Tran A,b1,b2) . v1 = 0. V2 by RANKNULL:10;
then (LineVec2Mx (v1 |-- b1)) * A = LineVec2Mx ((0. V2) |-- b2) by A1, Th32
.= LineVec2Mx ((len b2) |-> (0. K)) by Th20 ;
then ColVec2Mx ((len b2) |-> (0. K)) = (A @ ) * (ColVec2Mx (v1 |-- b1)) by A2, A11, A3, A5, A9, MATRIX_3:24;
then ColVec2Mx (v1 |-- b1) in Solutions_of (A @ ),(ColVec2Mx ((len b2) |-> (0. K))) by A13, A9, A10, A8;
then v1 |-- b1 in Solutions_of (A @ ),((len b2) |-> (0. K)) ;
then v1 |-- b1 in the carrier of (Space_of_Solutions_of (A @ )) by A4, A12, MATRIX15:def 5;
hence v1 |-- b1 in Space_of_Solutions_of (A @ ) by STRUCT_0:def 5; :: thesis: verum

end;

assume v1 |-- b1 in Space_of_Solutions_of (A @ ) ; :: thesis: v1 in ker (Mx2Tran A,b1,b2)
then v1 |-- b1 in the carrier of (Space_of_Solutions_of (A @ )) by STRUCT_0:def 5;
then v1 |-- b1 in Solutions_of (A @ ),((len b2) |-> (0. K)) by A4, A12, MATRIX15:def 5;
then ex f being FinSequence of K st
( f = v1 |-- b1 & ColVec2Mx f in Solutions_of (A @ ),(ColVec2Mx ((len b2) |-> (0. K))) ) ;
then ex X being Matrix of K st
( X = ColVec2Mx (v1 |-- b1) & len X = width (A @ ) & width X = width (ColVec2Mx ((len b2) |-> (0. K))) & ColVec2Mx ((len b2) |-> (0. K)) = (A @ ) * X ) ;
then A14: ColVec2Mx ((len b2) |-> (0. K)) = ((LineVec2Mx (v1 |-- b1)) * A) @ by A2, A11, A3, A5, A9, MATRIX_3:24;
width ((LineVec2Mx (v1 |-- b1)) * A) = width A by A11, A5, A9, MATRIX_3:def 4;
then (LineVec2Mx (v1 |-- b1)) * A = LineVec2Mx ((len b2) |-> (0. K)) by A2, A3, A7, A14, MATRIX_2:14
.= LineVec2Mx ((0. V2) |-- b2) by Th20 ;
then LineVec2Mx ((0. V2) |-- b2) = LineVec2Mx (((Mx2Tran A,b1,b2) . v1) |-- b2) by A1, Th32;
then (0. V2) |-- b2 = Line (LineVec2Mx (((Mx2Tran A,b1,b2) . v1) |-- b2)),1 by MATRIX15:25
.= ((Mx2Tran A,b1,b2) . v1) |-- b2 by MATRIX15:25 ;
then (Mx2Tran A,b1,b2) . v1 = 0. V2 by MATRLIN:39;
hence v1 in ker (Mx2Tran A,b1,b2) by RANKNULL:10; :: thesis: verum