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:106;
B4:
width A <> 0
by A4;
set L = Line (1. K,(width A)),j;
A5:
width (1. K,(width A)) = width A
by MATRIX_1:25;
then A6:
dom (Line (1. K,(width A)),j) = Seg (width A)
by FINSEQ_2:144;
A7:
Indices (1. K,(width A)) = [:(Seg (width A)),(Seg (width A)):]
by MATRIX_1:25;
A8:
now let 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 A9:
k in dom (Line (1. K,(width A)),j)
and A10:
k <> j
;
0. K = (Line (1. K,(width A)),j) . k
[j,k] in Indices (1. K,(width A))
by A4, A6, A7, A9, ZFMISC_1:106;
hence 0. K =
(1. K,(width A)) * j,
k
by A10, MATRIX_1:def 12
.=
(Line (1. K,(width A)),j) . k
by A5, A6, A9, MATRIX_1:def 8
;
verum end;
A11:
dom (Line A,i) = Seg (width A)
by FINSEQ_2:144;
[j,j] in Indices (1. K,(width A))
by A4, A7, ZFMISC_1:106;
then 1_ K =
(1. K,(width A)) * j,j
by MATRIX_1:def 12
.=
(Line (1. K,(width A)),j) . j
by A4, A5, MATRIX_1:def 8
;
then A12: Sum (mlt (Line (1. K,(width A)),j),(Line A,i)) =
(Line A,i) . j
by A4, A6, A11, A8, MATRIX_3:19
.=
A * i,j
by A4, MATRIX_1:def 8
;
A13:
ColVec2Mx ((len A) |-> (0. K)) = 0. K,(len A),1
by Th32;
A14:
i in dom A
by A2, ZFMISC_1:106;
Line (1. K,(width A)),j in (width A) -tuples_on the carrier of K
by A5;
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 A4, Def5, FINSEQ_1:4, B4;
then consider f being FinSequence of K such that
A15:
f = Line (1. K,(width A)),j
and
A16:
ColVec2Mx f in Solutions_of A,(ColVec2Mx ((len A) |-> (0. K)))
;
consider X being Matrix of K such that
A17:
X = ColVec2Mx f
and
A18:
len X = width A
and
width X = width (ColVec2Mx ((len A) |-> (0. K)))
and
A19:
A * X = ColVec2Mx ((len A) |-> (0. K))
by A16;
A20:
1 in Seg 1
;
A21:
dom A = Seg (len A)
by FINSEQ_1:def 3;
then
len A <> 0
by A2, ZFMISC_1:106;
then
Indices (ColVec2Mx ((len A) |-> (0. K))) = [:(Seg (len A)),(Seg 1):]
by A13, MATRIX_1:24;
then A22:
[i,1] in Indices (ColVec2Mx ((len A) |-> (0. K)))
by A14, A21, A20, ZFMISC_1:106;
then (Line A,i) "*" (Col X,1) =
(0. K,(len A),1) * i,1
by A18, A19, A13, MATRIX_3:def 4
.=
0. K
by A13, A22, MATRIX_3:3
;
then 0. K =
(Col X,1) "*" (Line A,i)
by FVSUM_1:115
.=
Sum (mlt f,(Line A,i))
by A4, A17, A18, Th26, FINSEQ_1:4, B4
;
hence
contradiction
by A3, A15, A12; verum