let K be Field; for A being Matrix of K st Space_of_Solutions_of A = (width A) -VectSp_over K holds
the_rank_of A = 0
let A be Matrix of K; ( Space_of_Solutions_of A = (width A) -VectSp_over K implies the_rank_of A = 0 )
assume A1:
Space_of_Solutions_of A = (width A) -VectSp_over K
; the_rank_of A = 0
assume
the_rank_of A <> 0
; contradiction
then consider i, j being Nat such that
A2:
[i,j] in Indices A
and
A3:
A * (i,j) <> 0. K
by MATRIX13:94;
A4:
j in Seg (width A)
by A2, ZFMISC_1:87;
then A5:
width A <> 0
;
set L = Line ((1. (K,(width A))),j);
A6:
width (1. (K,(width A))) = width A
by MATRIX_0:24;
then A7:
dom (Line ((1. (K,(width A))),j)) = Seg (width A)
by FINSEQ_2:124;
A8:
Indices (1. (K,(width A))) = [:(Seg (width A)),(Seg (width A)):]
by MATRIX_0:24;
A9:
now for k being Nat st k in dom (Line ((1. (K,(width A))),j)) & k <> j holds
0. K = (Line ((1. (K,(width A))),j)) . klet k be
Nat;
( k in dom (Line ((1. (K,(width A))),j)) & k <> j implies 0. K = (Line ((1. (K,(width A))),j)) . k )assume that A10:
k in dom (Line ((1. (K,(width A))),j))
and A11:
k <> j
;
0. K = (Line ((1. (K,(width A))),j)) . k
[j,k] in Indices (1. (K,(width A)))
by A4, A7, A8, A10, ZFMISC_1:87;
hence 0. K =
(1. (K,(width A))) * (
j,
k)
by A11, MATRIX_1:def 3
.=
(Line ((1. (K,(width A))),j)) . k
by A6, A7, A10, MATRIX_0:def 7
;
verum end;
A12:
dom (Line (A,i)) = Seg (width A)
by FINSEQ_2:124;
[j,j] in Indices (1. (K,(width A)))
by A4, A8, ZFMISC_1:87;
then 1_ K =
(1. (K,(width A))) * (j,j)
by MATRIX_1:def 3
.=
(Line ((1. (K,(width A))),j)) . j
by A4, A6, MATRIX_0:def 7
;
then A13: Sum (mlt ((Line ((1. (K,(width A))),j)),(Line (A,i)))) =
(Line (A,i)) . j
by A4, A7, A12, A9, MATRIX_3:17
.=
A * (i,j)
by A4, MATRIX_0:def 7
;
A14:
ColVec2Mx ((len A) |-> (0. K)) = 0. (K,(len A),1)
by Th32;
A15:
i in dom A
by A2, ZFMISC_1:87;
Line ((1. (K,(width A))),j) in (width A) -tuples_on the carrier of K
by A6;
then
Line ((1. (K,(width A))),j) in the carrier of (Space_of_Solutions_of A)
by A1, MATRIX13:102;
then
Line ((1. (K,(width A))),j) in Solutions_of (A,((len A) |-> (0. K)))
by Def5, A5;
then consider f being FinSequence of K such that
A16:
f = Line ((1. (K,(width A))),j)
and
A17:
ColVec2Mx f in Solutions_of (A,(ColVec2Mx ((len A) |-> (0. K))))
;
consider X being Matrix of K such that
A18:
X = ColVec2Mx f
and
A19:
len X = width A
and
width X = width (ColVec2Mx ((len A) |-> (0. K)))
and
A20:
A * X = ColVec2Mx ((len A) |-> (0. K))
by A17;
A21:
1 in Seg 1
;
A22:
dom A = Seg (len A)
by FINSEQ_1:def 3;
then
len A <> 0
by A2, ZFMISC_1:87;
then
Indices (ColVec2Mx ((len A) |-> (0. K))) = [:(Seg (len A)),(Seg 1):]
by A14, MATRIX_0:23;
then A23:
[i,1] in Indices (ColVec2Mx ((len A) |-> (0. K)))
by A15, A22, A21, ZFMISC_1:87;
then (Line (A,i)) "*" (Col (X,1)) =
(0. (K,(len A),1)) * (i,1)
by A19, A20, A14, MATRIX_3:def 4
.=
0. K
by A14, A23, MATRIX_3:1
;
then 0. K =
(Col (X,1)) "*" (Line (A,i))
by FVSUM_1:90
.=
Sum (mlt (f,(Line (A,i))))
by A18, A19, Th26, A5
;
hence
contradiction
by A3, A16, A13; verum