let n be Nat; :: thesis: for K being Field holds dim (Space_of_Solutions_of (1. (K,n))) = 0
let K be Field; :: thesis: dim (Space_of_Solutions_of (1. (K,n))) = 0
set ONE = 1. (K,n);
set SS = Space_of_Solutions_of (1. (K,n));
A1: the carrier of (Space_of_Solutions_of (1. (K,n))) c= the carrier of ((0). (Space_of_Solutions_of (1. (K,n))))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (Space_of_Solutions_of (1. (K,n))) or x in the carrier of ((0). (Space_of_Solutions_of (1. (K,n)))) )
assume A2: x in the carrier of (Space_of_Solutions_of (1. (K,n))) ; :: thesis: x in the carrier of ((0). (Space_of_Solutions_of (1. (K,n))))
A3: len (1. (K,n)) = n by MATRIX_0:24;
A4: width (1. (K,n)) = n by MATRIX_0:24;
then ( width (1. (K,n)) = 0 implies len (1. (K,n)) = 0 ) by MATRIX_0:24;
then x in Solutions_of ((1. (K,n)),(n |-> (0. K))) by A2, A3, Def5;
then consider f being FinSequence of K such that
A5: f = x and
A6: ColVec2Mx f in Solutions_of ((1. (K,n)),(ColVec2Mx (n |-> (0. K)))) ;
consider X being Matrix of K such that
A7: X = ColVec2Mx f and
A8: len X = width (1. (K,n)) and
width X = width (ColVec2Mx (n |-> (0. K))) and
A9: (1. (K,n)) * X = ColVec2Mx (n |-> (0. K)) by A6;
A10: now :: thesis: n |-> (0. K) = f
per cases ( n > 0 or n = 0 ) ;
suppose A11: n > 0 ; :: thesis: n |-> (0. K) = f
(1. (K,n)) * X = X by ;
hence n |-> (0. K) = Col (X,1) by
.= f by A4, A7, A8, A11, Th26 ;
:: thesis: verum
end;
suppose A12: n = 0 ; :: thesis: f = n |-> (0. K)
then f = {} by ;
hence f = n |-> (0. K) by A12; :: thesis: verum
end;
end;
end;
0. (Space_of_Solutions_of (1. (K,n))) = 0. ((width (1. (K,n))) -VectSp_over K) by VECTSP_4:11
.= n |-> (0. K) by ;
then f in {(0. (Space_of_Solutions_of (1. (K,n))))} by ;
hence x in the carrier of ((0). (Space_of_Solutions_of (1. (K,n)))) by ; :: thesis: verum
end;
the carrier of ((0). (Space_of_Solutions_of (1. (K,n)))) c= the carrier of (Space_of_Solutions_of (1. (K,n))) by VECTSP_4:def 2;
then the carrier of (Space_of_Solutions_of (1. (K,n))) = the carrier of ((0). (Space_of_Solutions_of (1. (K,n)))) by A1;
then (0). (Space_of_Solutions_of (1. (K,n))) = (Omega). (Space_of_Solutions_of (1. (K,n))) by VECTSP_4:29;
hence dim (Space_of_Solutions_of (1. (K,n))) = 0 by VECTSP_9:29; :: thesis: verum