let n be Nat; for K being Field holds dim (Space_of_Solutions_of (1. (K,n))) = 0
let K be Field; 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 ;
TARSKI:def 3 ( 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)))
;
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 n |-> (0. K) = fper cases
( n > 0 or n = 0 )
;
suppose A11:
n > 0
;
n |-> (0. K) = f
(1. (K,n)) * X = X
by A4, A8, MATRIXR2:68;
hence n |-> (0. K) =
Col (
X,1)
by A9, A11, Th26
.=
f
by A4, A7, A8, A11, Th26
;
verum 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 A4, MATRIX13:102
;
then
f in {(0. (Space_of_Solutions_of (1. (K,n))))}
by A10, TARSKI:def 1;
hence
x in the
carrier of
((0). (Space_of_Solutions_of (1. (K,n))))
by A5, VECTSP_4:def 3;
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; verum