let K be Field; :: thesis: for A being Matrix of K st ( width A = 0 implies len A = 0 ) holds

dim (Space_of_Solutions_of A) = (width A) - (the_rank_of A)

let A be Matrix of K; :: thesis: ( ( width A = 0 implies len A = 0 ) implies dim (Space_of_Solutions_of A) = (width A) - (the_rank_of A) )

assume A1: ( width A = 0 implies len A = 0 ) ; :: thesis: dim (Space_of_Solutions_of A) = (width A) - (the_rank_of A)

set W = width A;

set L = len A;

reconsider A9 = A as Matrix of len A, width A,K by MATRIX_0:51;

dim (Space_of_Solutions_of A) = (width A) - (the_rank_of A)

let A be Matrix of K; :: thesis: ( ( width A = 0 implies len A = 0 ) implies dim (Space_of_Solutions_of A) = (width A) - (the_rank_of A) )

assume A1: ( width A = 0 implies len A = 0 ) ; :: thesis: dim (Space_of_Solutions_of A) = (width A) - (the_rank_of A)

set W = width A;

set L = len A;

reconsider A9 = A as Matrix of len A, width A,K by MATRIX_0:51;

per cases
( the_rank_of A = 0 or the_rank_of A > 0 )
;

end;

suppose A2:
the_rank_of A = 0
; :: thesis: dim (Space_of_Solutions_of A) = (width A) - (the_rank_of A)

dim ((width A) -VectSp_over K) = width A
by MATRIX13:112;

hence dim (Space_of_Solutions_of A) = (width A) - (the_rank_of A) by A1, A2, Th63; :: thesis: verum

end;hence dim (Space_of_Solutions_of A) = (width A) - (the_rank_of A) by A1, A2, Th63; :: thesis: verum

suppose A3:
the_rank_of A > 0
; :: thesis: dim (Space_of_Solutions_of A) = (width A) - (the_rank_of A)

defpred S_{1}[ set , set ] means for A1 being Matrix of len A, width A,K st A1 = $1 holds

Space_of_Solutions_of A9 = Space_of_Solutions_of A1;

deffunc H_{1}( Matrix of len A, width A,K, Nat, Nat, Element of K) -> Matrix of len A, width A,K = $1;

A4: width A > 0 by A3, MATRIX13:74;

A5: for A1, B1 being Matrix of len A, width A,K st S_{1}[A1,B1] holds

for a being Element of K

for i, j being Nat st j in dom A1 & ( i = j implies a <> - (1_ K) ) holds

S_{1}[ RLine (A1,i,((Line (A1,i)) + (a * (Line (A1,j))))),H_{1}(B1,i,j,a)]
_{1}[A9,A9]
;

consider A1, B1 being Matrix of len A, width A,K, N being finite without_zero Subset of NAT such that

A9: N c= Seg (width A) and

A10: ( the_rank_of A9 = the_rank_of A1 & the_rank_of A9 = card N ) and

A11: ( S_{1}[A1,B1] & Segm (A1,(Seg (card N)),N) = 1. (K,(card N)) )
and

A12: for i being Nat st i in dom A1 & i > card N holds

Line (A1,i) = (width A) |-> (0. K) and

for i, j being Nat st i in Seg (card N) & j in Seg (width A1) & j < (Sgm N) . i holds

A1 * (i,j) = 0. K from MATRIX15:sch 2(A8, A5);

A13: 0 < len A by A3, MATRIX13:74;

then A14: width A1 = width A by MATRIX_0:23;

then A15: card (Seg (width A1)) = width A by FINSEQ_1:57;

then A16: card ((Seg (width A)) \ N) = (width A) - (card N) by A9, A14, CARD_2:44;

set SN = Segm (A1,(Seg (card N)),(Seg (width A1)));

A17: Seg (card N) c= Seg (card N) ;

A18: (width A) -' (card N) = (width A) - (card N) by A9, A14, A15, NAT_1:43, XREAL_1:233;

Sgm (Seg (card N)) = idseq (card N) by FINSEQ_3:48

.= id (Seg (card N)) ;

then A19: Seg (card N) = (Sgm (Seg (card N))) " (Seg (card N)) by A17, FUNCT_2:94;

Sgm (Seg (width A1)) = idseq (width A1) by FINSEQ_3:48

.= id (Seg (width A1)) ;

then N = (Sgm (Seg (width A1))) " N by A9, A14, FUNCT_2:94;

then A20: Segm ((Segm (A1,(Seg (card N)),(Seg (width A1)))),(Seg (card N)),N) = 1. (K,(card N)) by A9, A11, A14, A19, MATRIX13:56;

A21: card (Seg (card N)) = card N by FINSEQ_1:57;

A22: Seg (len A1) = dom A1 by FINSEQ_1:def 3;

then A26: Seg (card N) c= Seg (len A1) by FINSEQ_1:5;

width A1 > 0 by A4, A13, MATRIX_0:23;

then A27: Space_of_Solutions_of (Segm (A1,(Seg (card N)),(Seg (width A1)))) = Space_of_Solutions_of A1 by A3, A10, A26, A22, A23, Th66

.= Space_of_Solutions_of A9 by A11 ;

end;Space_of_Solutions_of A9 = Space_of_Solutions_of A1;

deffunc H

A4: width A > 0 by A3, MATRIX13:74;

A5: for A1, B1 being Matrix of len A, width A,K st S

for a being Element of K

for i, j being Nat st j in dom A1 & ( i = j implies a <> - (1_ K) ) holds

S

proof

A8:
S
let A1, B1 be Matrix of len A, width A,K; :: thesis: ( S_{1}[A1,B1] implies for a being Element of K

for i, j being Nat st j in dom A1 & ( i = j implies a <> - (1_ K) ) holds

S_{1}[ RLine (A1,i,((Line (A1,i)) + (a * (Line (A1,j))))),H_{1}(B1,i,j,a)] )

assume A6: S_{1}[A1,B1]
; :: thesis: for a being Element of K

for i, j being Nat st j in dom A1 & ( i = j implies a <> - (1_ K) ) holds

S_{1}[ RLine (A1,i,((Line (A1,i)) + (a * (Line (A1,j))))),H_{1}(B1,i,j,a)]

let a be Element of K; :: thesis: for i, j being Nat st j in dom A1 & ( i = j implies a <> - (1_ K) ) holds

S_{1}[ RLine (A1,i,((Line (A1,i)) + (a * (Line (A1,j))))),H_{1}(B1,i,j,a)]

A7: dom A1 = Seg (len A1) by FINSEQ_1:def 3

.= Seg (len A) by MATRIX_0:def 2 ;

let i, j be Nat; :: thesis: ( j in dom A1 & ( i = j implies a <> - (1_ K) ) implies S_{1}[ RLine (A1,i,((Line (A1,i)) + (a * (Line (A1,j))))),H_{1}(B1,i,j,a)] )

assume ( j in dom A1 & ( i = j implies a <> - (1_ K) ) ) ; :: thesis: S_{1}[ RLine (A1,i,((Line (A1,i)) + (a * (Line (A1,j))))),H_{1}(B1,i,j,a)]

then Space_of_Solutions_of (RLine (A1,i,((Line (A1,i)) + (a * (Line (A1,j)))))) = Space_of_Solutions_of A1 by A4, A7, Th65

.= Space_of_Solutions_of A9 by A6 ;

hence S_{1}[ RLine (A1,i,((Line (A1,i)) + (a * (Line (A1,j))))),H_{1}(B1,i,j,a)]
; :: thesis: verum

end;for i, j being Nat st j in dom A1 & ( i = j implies a <> - (1_ K) ) holds

S

assume A6: S

for i, j being Nat st j in dom A1 & ( i = j implies a <> - (1_ K) ) holds

S

let a be Element of K; :: thesis: for i, j being Nat st j in dom A1 & ( i = j implies a <> - (1_ K) ) holds

S

A7: dom A1 = Seg (len A1) by FINSEQ_1:def 3

.= Seg (len A) by MATRIX_0:def 2 ;

let i, j be Nat; :: thesis: ( j in dom A1 & ( i = j implies a <> - (1_ K) ) implies S

assume ( j in dom A1 & ( i = j implies a <> - (1_ K) ) ) ; :: thesis: S

then Space_of_Solutions_of (RLine (A1,i,((Line (A1,i)) + (a * (Line (A1,j)))))) = Space_of_Solutions_of A1 by A4, A7, Th65

.= Space_of_Solutions_of A9 by A6 ;

hence S

consider A1, B1 being Matrix of len A, width A,K, N being finite without_zero Subset of NAT such that

A9: N c= Seg (width A) and

A10: ( the_rank_of A9 = the_rank_of A1 & the_rank_of A9 = card N ) and

A11: ( S

A12: for i being Nat st i in dom A1 & i > card N holds

Line (A1,i) = (width A) |-> (0. K) and

for i, j being Nat st i in Seg (card N) & j in Seg (width A1) & j < (Sgm N) . i holds

A1 * (i,j) = 0. K from MATRIX15:sch 2(A8, A5);

A13: 0 < len A by A3, MATRIX13:74;

then A14: width A1 = width A by MATRIX_0:23;

then A15: card (Seg (width A1)) = width A by FINSEQ_1:57;

then A16: card ((Seg (width A)) \ N) = (width A) - (card N) by A9, A14, CARD_2:44;

set SN = Segm (A1,(Seg (card N)),(Seg (width A1)));

A17: Seg (card N) c= Seg (card N) ;

A18: (width A) -' (card N) = (width A) - (card N) by A9, A14, A15, NAT_1:43, XREAL_1:233;

Sgm (Seg (card N)) = idseq (card N) by FINSEQ_3:48

.= id (Seg (card N)) ;

then A19: Seg (card N) = (Sgm (Seg (card N))) " (Seg (card N)) by A17, FUNCT_2:94;

Sgm (Seg (width A1)) = idseq (width A1) by FINSEQ_3:48

.= id (Seg (width A1)) ;

then N = (Sgm (Seg (width A1))) " N by A9, A14, FUNCT_2:94;

then A20: Segm ((Segm (A1,(Seg (card N)),(Seg (width A1)))),(Seg (card N)),N) = 1. (K,(card N)) by A9, A11, A14, A19, MATRIX13:56;

A21: card (Seg (card N)) = card N by FINSEQ_1:57;

A22: Seg (len A1) = dom A1 by FINSEQ_1:def 3;

A23: now :: thesis: for i being Nat st i in (dom A1) \ (Seg (card N)) holds

Line (A1,i) = (width A1) |-> (0. K)

card N <= len A1
by A10, MATRIX13:74;Line (A1,i) = (width A1) |-> (0. K)

let i be Nat; :: thesis: ( i in (dom A1) \ (Seg (card N)) implies Line (A1,i) = (width A1) |-> (0. K) )

assume A24: i in (dom A1) \ (Seg (card N)) ; :: thesis: Line (A1,i) = (width A1) |-> (0. K)

not i in Seg (card N) by A24, XBOOLE_0:def 5;

then A25: ( i < 1 or i > card N ) ;

i in dom A1 by A24, XBOOLE_0:def 5;

hence Line (A1,i) = (width A1) |-> (0. K) by A12, A22, A14, A25, FINSEQ_1:1; :: thesis: verum

end;assume A24: i in (dom A1) \ (Seg (card N)) ; :: thesis: Line (A1,i) = (width A1) |-> (0. K)

not i in Seg (card N) by A24, XBOOLE_0:def 5;

then A25: ( i < 1 or i > card N ) ;

i in dom A1 by A24, XBOOLE_0:def 5;

hence Line (A1,i) = (width A1) |-> (0. K) by A12, A22, A14, A25, FINSEQ_1:1; :: thesis: verum

then A26: Seg (card N) c= Seg (len A1) by FINSEQ_1:5;

width A1 > 0 by A4, A13, MATRIX_0:23;

then A27: Space_of_Solutions_of (Segm (A1,(Seg (card N)),(Seg (width A1)))) = Space_of_Solutions_of A1 by A3, A10, A26, A22, A23, Th66

.= Space_of_Solutions_of A9 by A11 ;

per cases
( (width A) -' (card N) = 0 or (width A) -' (card N) > 0 )
;

end;

suppose A28:
(width A) -' (card N) = 0
; :: thesis: dim (Space_of_Solutions_of A) = (width A) - (the_rank_of A)

then
Segm (A1,(Seg (card N)),(Seg (width A1))) = 1. (K,(card N))
by A9, A11, A14, A21, A18, CARD_2:102;

hence dim (Space_of_Solutions_of A) = (width A) - (the_rank_of A) by A10, A27, A18, A28, Lm8; :: thesis: verum

end;hence dim (Space_of_Solutions_of A) = (width A) - (the_rank_of A) by A10, A27, A18, A28, Lm8; :: thesis: verum

suppose A29:
(width A) -' (card N) > 0
; :: thesis: dim (Space_of_Solutions_of A) = (width A) - (the_rank_of A)

then
((width A) -' (card N)) + 0 > 0
;

then (width A) -' (card N) >= 1 by NAT_1:19;

then A30: Det (1. (K,((width A) -' (card N)))) = 1_ K by MATRIX_7:16;

A31: ( card (Seg ((width A) -' (card N))) = (width A) -' (card N) & 0. K <> 1_ K ) by FINSEQ_1:57;

consider MVectors being Matrix of (width A) -' (card N), width A,K such that

A32: Segm (MVectors,(Seg ((width A) -' (card N))),((Seg (width A)) \ N)) = 1. (K,((width A) -' (card N))) and

Segm (MVectors,(Seg ((width A) -' (card N))),N) = - ((Segm ((Segm (A1,(Seg (card N)),(Seg (width A1)))),(Seg (card N)),((Seg (width A)) \ N))) @) and

A33: Lin (lines MVectors) = Space_of_Solutions_of A9 by A3, A9, A10, A27, A21, A15, A20, A29, Th67;

len MVectors = (width A) -' (card N) by A29, MATRIX_0:23;

then A34: (width A) -' (card N) >= the_rank_of MVectors by MATRIX13:74;

A35: (Seg (width A)) \ N c= Seg (width A) by XBOOLE_1:36;

Indices MVectors = [:(Seg ((width A) -' (card N))),(Seg (width A)):] by A29, MATRIX_0:23;

then A36: [:(Seg ((width A) -' (card N))),((Seg (width A)) \ N):] c= Indices MVectors by A35, ZFMISC_1:95;

reconsider B = lines MVectors as Subset of ((width A) -VectSp_over K) ;

A37: ( dom MVectors = Seg (len MVectors) & len MVectors = (width A) -' (card N) ) by FINSEQ_1:def 3, MATRIX_0:def 2;

EqSegm (MVectors,(Seg ((width A) -' (card N))),((Seg (width A)) \ N)) = 1. (K,((width A) -' (card N))) by A16, A18, A32, FINSEQ_1:57, MATRIX13:def 3;

then A38: (width A) -' (card N) <= the_rank_of MVectors by A16, A18, A36, A30, A31, MATRIX13:def 4;

then MVectors is without_repeated_line by A34, MATRIX13:105, XXREAL_0:1;

then Seg ((width A) -' (card N)),B are_equipotent by A37, WELLORD2:def 4;

then A39: card B = card (Seg ((width A) -' (card N))) by CARD_1:5

.= (width A) -' (card N) by FINSEQ_1:57 ;

the_rank_of MVectors = (width A) -' (card N) by A38, A34, XXREAL_0:1;

then lines MVectors is linearly-independent by MATRIX13:121;

hence dim (Space_of_Solutions_of A) = (width A) - (the_rank_of A) by A10, A18, A33, A39, VECTSP_9:26; :: thesis: verum

end;then (width A) -' (card N) >= 1 by NAT_1:19;

then A30: Det (1. (K,((width A) -' (card N)))) = 1_ K by MATRIX_7:16;

A31: ( card (Seg ((width A) -' (card N))) = (width A) -' (card N) & 0. K <> 1_ K ) by FINSEQ_1:57;

consider MVectors being Matrix of (width A) -' (card N), width A,K such that

A32: Segm (MVectors,(Seg ((width A) -' (card N))),((Seg (width A)) \ N)) = 1. (K,((width A) -' (card N))) and

Segm (MVectors,(Seg ((width A) -' (card N))),N) = - ((Segm ((Segm (A1,(Seg (card N)),(Seg (width A1)))),(Seg (card N)),((Seg (width A)) \ N))) @) and

A33: Lin (lines MVectors) = Space_of_Solutions_of A9 by A3, A9, A10, A27, A21, A15, A20, A29, Th67;

len MVectors = (width A) -' (card N) by A29, MATRIX_0:23;

then A34: (width A) -' (card N) >= the_rank_of MVectors by MATRIX13:74;

A35: (Seg (width A)) \ N c= Seg (width A) by XBOOLE_1:36;

Indices MVectors = [:(Seg ((width A) -' (card N))),(Seg (width A)):] by A29, MATRIX_0:23;

then A36: [:(Seg ((width A) -' (card N))),((Seg (width A)) \ N):] c= Indices MVectors by A35, ZFMISC_1:95;

reconsider B = lines MVectors as Subset of ((width A) -VectSp_over K) ;

A37: ( dom MVectors = Seg (len MVectors) & len MVectors = (width A) -' (card N) ) by FINSEQ_1:def 3, MATRIX_0:def 2;

EqSegm (MVectors,(Seg ((width A) -' (card N))),((Seg (width A)) \ N)) = 1. (K,((width A) -' (card N))) by A16, A18, A32, FINSEQ_1:57, MATRIX13:def 3;

then A38: (width A) -' (card N) <= the_rank_of MVectors by A16, A18, A36, A30, A31, MATRIX13:def 4;

then MVectors is without_repeated_line by A34, MATRIX13:105, XXREAL_0:1;

then Seg ((width A) -' (card N)),B are_equipotent by A37, WELLORD2:def 4;

then A39: card B = card (Seg ((width A) -' (card N))) by CARD_1:5

.= (width A) -' (card N) by FINSEQ_1:57 ;

the_rank_of MVectors = (width A) -' (card N) by A38, A34, XXREAL_0:1;

then lines MVectors is linearly-independent by MATRIX13:121;

hence dim (Space_of_Solutions_of A) = (width A) - (the_rank_of A) by A10, A18, A33, A39, VECTSP_9:26; :: thesis: verum