let K be Field; :: thesis: 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 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, V2 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_0:23;
then A4: len (A @) = len b2 by A2, MATRIX_0:54;
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_0:23;
len ((len b2) |-> (0. K)) = len b2 by CARD_1:def 7;
then A6: width (LineVec2Mx ((len b2) |-> (0. K))) = len b2 by MATRIX_0:23;
A7: width (ColVec2Mx ((len b2) |-> (0. K))) = 1 by A2, MATRIX_0:23;
A8: len (v1 |-- b1) = len b1 by MATRLIN:def 7;
then A9: ( len (ColVec2Mx (v1 |-- b1)) = len (v1 |-- b1) & width (ColVec2Mx (v1 |-- b1)) = 1 ) by A1, MATRIX_0:23;
A10: len A = len b1 by A1, MATRIX_0:23;
then A11: ( width (A @) = 0 implies len (A @) = 0 ) by A1, A2, A3, MATRIX_0:54;
A12: width (A @) = len b1 by A2, A10, A3, MATRIX_0:54;
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, A10, A3, A5, A8, MATRIX_3:22;
then ColVec2Mx (v1 |-- b1) in Solutions_of ((A @),(ColVec2Mx ((len b2) |-> (0. K)))) by A12, A8, A9, A7;
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, A11, MATRIX15:def 5;
hence v1 |-- b1 in Space_of_Solutions_of (A @) ; :: 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 @)) ;
then v1 |-- b1 in Solutions_of ((A @),((len b2) |-> (0. K))) by A4, A11, 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 A13: ColVec2Mx ((len b2) |-> (0. K)) = ((LineVec2Mx (v1 |-- b1)) * A) @ by A2, A10, A3, A5, A8, MATRIX_3:22;
width ((LineVec2Mx (v1 |-- b1)) * A) = width A by A10, A5, A8, MATRIX_3:def 4;
then (LineVec2Mx (v1 |-- b1)) * A = LineVec2Mx ((len b2) |-> (0. K)) by A2, A3, A6, A13, MATRIX_0:56
.= 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:34;
hence v1 in ker (Mx2Tran (A,b1,b2)) by RANKNULL:10; :: thesis: verum