let K be Field; :: thesis: for A being Matrix of K

for N being finite without_zero Subset of NAT st N c= dom A & not N is empty & width A > 0 & ( for i being Nat st i in (dom A) \ N holds

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

Space_of_Solutions_of A = Space_of_Solutions_of (Segm (A,N,(Seg (width A))))

let A be Matrix of K; :: thesis: for N being finite without_zero Subset of NAT st N c= dom A & not N is empty & width A > 0 & ( for i being Nat st i in (dom A) \ N holds

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

Space_of_Solutions_of A = Space_of_Solutions_of (Segm (A,N,(Seg (width A))))

let N be finite without_zero Subset of NAT; :: thesis: ( N c= dom A & not N is empty & width A > 0 & ( for i being Nat st i in (dom A) \ N holds

Line (A,i) = (width A) |-> (0. K) ) implies Space_of_Solutions_of A = Space_of_Solutions_of (Segm (A,N,(Seg (width A)))) )

assume that

A1: N c= dom A and

A2: not N is empty and

A3: width A > 0 and

A4: for i being Nat st i in (dom A) \ N holds

Line (A,i) = (width A) |-> (0. K) ; :: thesis: Space_of_Solutions_of A = Space_of_Solutions_of (Segm (A,N,(Seg (width A))))

set L = (len A) |-> (0. K);

set C = ColVec2Mx ((len A) |-> (0. K));

A5: len ((len A) |-> (0. K)) = len A by CARD_1:def 7;

set S = Segm (A,N,(Seg (width A)));

A6: width (Segm (A,N,(Seg (width A)))) = card (Seg (width A)) by A2, MATRIX_0:23;

then A7: width A = width (Segm (A,N,(Seg (width A)))) by FINSEQ_1:57;

set SS = Space_of_Solutions_of (Segm (A,N,(Seg (width A))));

len (Segm (A,N,(Seg (width A)))) = card N by MATRIX_0:def 2;

then A8: the carrier of (Space_of_Solutions_of (Segm (A,N,(Seg (width A))))) = Solutions_of ((Segm (A,N,(Seg (width A)))),((card N) |-> (0. K))) by A3, A6, Def5;

set SA = Space_of_Solutions_of A;

A9: the carrier of (Space_of_Solutions_of A) = Solutions_of (A,((len A) |-> (0. K))) by A3, Def5;

A10: ColVec2Mx ((len A) |-> (0. K)) = 0. (K,(len A),1) by Th32;

len (ColVec2Mx ((len A) |-> (0. K))) = len ((len A) |-> (0. K)) by MATRIX_0:def 2;

then A11: dom (ColVec2Mx ((len A) |-> (0. K))) = dom A by A5, FINSEQ_3:29;

A12: dom A = Seg (len A) by FINSEQ_1:def 3;

then A13: Seg (len A) <> {} by A1, A2;

then A14: width (ColVec2Mx ((len A) |-> (0. K))) = 1 by Th26;

then A15: card (Seg (width (ColVec2Mx ((len A) |-> (0. K))))) = 1 by FINSEQ_1:57;

.= ColVec2Mx ((card N) |-> (0. K)) by Th32 ;

hence Space_of_Solutions_of A = Space_of_Solutions_of (Segm (A,N,(Seg (width A)))) by A20, A7, A9, A8, VECTSP_4:29; :: thesis: verum

for N being finite without_zero Subset of NAT st N c= dom A & not N is empty & width A > 0 & ( for i being Nat st i in (dom A) \ N holds

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

Space_of_Solutions_of A = Space_of_Solutions_of (Segm (A,N,(Seg (width A))))

let A be Matrix of K; :: thesis: for N being finite without_zero Subset of NAT st N c= dom A & not N is empty & width A > 0 & ( for i being Nat st i in (dom A) \ N holds

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

Space_of_Solutions_of A = Space_of_Solutions_of (Segm (A,N,(Seg (width A))))

let N be finite without_zero Subset of NAT; :: thesis: ( N c= dom A & not N is empty & width A > 0 & ( for i being Nat st i in (dom A) \ N holds

Line (A,i) = (width A) |-> (0. K) ) implies Space_of_Solutions_of A = Space_of_Solutions_of (Segm (A,N,(Seg (width A)))) )

assume that

A1: N c= dom A and

A2: not N is empty and

A3: width A > 0 and

A4: for i being Nat st i in (dom A) \ N holds

Line (A,i) = (width A) |-> (0. K) ; :: thesis: Space_of_Solutions_of A = Space_of_Solutions_of (Segm (A,N,(Seg (width A))))

set L = (len A) |-> (0. K);

set C = ColVec2Mx ((len A) |-> (0. K));

A5: len ((len A) |-> (0. K)) = len A by CARD_1:def 7;

set S = Segm (A,N,(Seg (width A)));

A6: width (Segm (A,N,(Seg (width A)))) = card (Seg (width A)) by A2, MATRIX_0:23;

then A7: width A = width (Segm (A,N,(Seg (width A)))) by FINSEQ_1:57;

set SS = Space_of_Solutions_of (Segm (A,N,(Seg (width A))));

len (Segm (A,N,(Seg (width A)))) = card N by MATRIX_0:def 2;

then A8: the carrier of (Space_of_Solutions_of (Segm (A,N,(Seg (width A))))) = Solutions_of ((Segm (A,N,(Seg (width A)))),((card N) |-> (0. K))) by A3, A6, Def5;

set SA = Space_of_Solutions_of A;

A9: the carrier of (Space_of_Solutions_of A) = Solutions_of (A,((len A) |-> (0. K))) by A3, Def5;

A10: ColVec2Mx ((len A) |-> (0. K)) = 0. (K,(len A),1) by Th32;

len (ColVec2Mx ((len A) |-> (0. K))) = len ((len A) |-> (0. K)) by MATRIX_0:def 2;

then A11: dom (ColVec2Mx ((len A) |-> (0. K))) = dom A by A5, FINSEQ_3:29;

A12: dom A = Seg (len A) by FINSEQ_1:def 3;

then A13: Seg (len A) <> {} by A1, A2;

then A14: width (ColVec2Mx ((len A) |-> (0. K))) = 1 by Th26;

then A15: card (Seg (width (ColVec2Mx ((len A) |-> (0. K))))) = 1 by FINSEQ_1:57;

now :: thesis: for k, l being Nat st [k,l] in Indices (Segm ((ColVec2Mx ((len A) |-> (0. K))),N,(Seg (width (ColVec2Mx ((len A) |-> (0. K))))))) holds

(Segm ((ColVec2Mx ((len A) |-> (0. K))),N,(Seg (width (ColVec2Mx ((len A) |-> (0. K))))))) * (k,l) = (0. (K,(card N),1)) * (k,l)

then A20: Segm ((ColVec2Mx ((len A) |-> (0. K))),N,(Seg (width (ColVec2Mx ((len A) |-> (0. K)))))) =
0. (K,(card N),1)
by A15, MATRIX_0:27
(Segm ((ColVec2Mx ((len A) |-> (0. K))),N,(Seg (width (ColVec2Mx ((len A) |-> (0. K))))))) * (k,l) = (0. (K,(card N),1)) * (k,l)

A16:
rng (Sgm (Seg 1)) = Seg 1
by FINSEQ_1:def 13;

A17: Indices (Segm ((ColVec2Mx ((len A) |-> (0. K))),N,(Seg (width (ColVec2Mx ((len A) |-> (0. K))))))) = Indices (0. (K,(card N),1)) by A15, MATRIX_0:26;

let k, l be Nat; :: thesis: ( [k,l] in Indices (Segm ((ColVec2Mx ((len A) |-> (0. K))),N,(Seg (width (ColVec2Mx ((len A) |-> (0. K))))))) implies (Segm ((ColVec2Mx ((len A) |-> (0. K))),N,(Seg (width (ColVec2Mx ((len A) |-> (0. K))))))) * (k,l) = (0. (K,(card N),1)) * (k,l) )

assume A18: [k,l] in Indices (Segm ((ColVec2Mx ((len A) |-> (0. K))),N,(Seg (width (ColVec2Mx ((len A) |-> (0. K))))))) ; :: thesis: (Segm ((ColVec2Mx ((len A) |-> (0. K))),N,(Seg (width (ColVec2Mx ((len A) |-> (0. K))))))) * (k,l) = (0. (K,(card N),1)) * (k,l)

reconsider kk = k, ll = l as Element of NAT by ORDINAL1:def 12;

( [:N,(Seg (width (ColVec2Mx ((len A) |-> (0. K))))):] c= Indices (ColVec2Mx ((len A) |-> (0. K))) & rng (Sgm N) = N ) by A1, A12, A11, FINSEQ_1:def 13, ZFMISC_1:95;

then A19: [((Sgm N) . kk),((Sgm (Seg (width (ColVec2Mx ((len A) |-> (0. K)))))) . ll)] in Indices (ColVec2Mx ((len A) |-> (0. K))) by A14, A18, A16, MATRIX13:17;

thus (Segm ((ColVec2Mx ((len A) |-> (0. K))),N,(Seg (width (ColVec2Mx ((len A) |-> (0. K))))))) * (k,l) = (ColVec2Mx ((len A) |-> (0. K))) * (((Sgm N) . kk),((Sgm (Seg (width (ColVec2Mx ((len A) |-> (0. K)))))) . ll)) by A18, MATRIX13:def 1

.= 0. K by A10, A19, MATRIX_3:1

.= (0. (K,(card N),1)) * (k,l) by A18, A17, MATRIX_3:1 ; :: thesis: verum

end;A17: Indices (Segm ((ColVec2Mx ((len A) |-> (0. K))),N,(Seg (width (ColVec2Mx ((len A) |-> (0. K))))))) = Indices (0. (K,(card N),1)) by A15, MATRIX_0:26;

let k, l be Nat; :: thesis: ( [k,l] in Indices (Segm ((ColVec2Mx ((len A) |-> (0. K))),N,(Seg (width (ColVec2Mx ((len A) |-> (0. K))))))) implies (Segm ((ColVec2Mx ((len A) |-> (0. K))),N,(Seg (width (ColVec2Mx ((len A) |-> (0. K))))))) * (k,l) = (0. (K,(card N),1)) * (k,l) )

assume A18: [k,l] in Indices (Segm ((ColVec2Mx ((len A) |-> (0. K))),N,(Seg (width (ColVec2Mx ((len A) |-> (0. K))))))) ; :: thesis: (Segm ((ColVec2Mx ((len A) |-> (0. K))),N,(Seg (width (ColVec2Mx ((len A) |-> (0. K))))))) * (k,l) = (0. (K,(card N),1)) * (k,l)

reconsider kk = k, ll = l as Element of NAT by ORDINAL1:def 12;

( [:N,(Seg (width (ColVec2Mx ((len A) |-> (0. K))))):] c= Indices (ColVec2Mx ((len A) |-> (0. K))) & rng (Sgm N) = N ) by A1, A12, A11, FINSEQ_1:def 13, ZFMISC_1:95;

then A19: [((Sgm N) . kk),((Sgm (Seg (width (ColVec2Mx ((len A) |-> (0. K)))))) . ll)] in Indices (ColVec2Mx ((len A) |-> (0. K))) by A14, A18, A16, MATRIX13:17;

thus (Segm ((ColVec2Mx ((len A) |-> (0. K))),N,(Seg (width (ColVec2Mx ((len A) |-> (0. K))))))) * (k,l) = (ColVec2Mx ((len A) |-> (0. K))) * (((Sgm N) . kk),((Sgm (Seg (width (ColVec2Mx ((len A) |-> (0. K)))))) . ll)) by A18, MATRIX13:def 1

.= 0. K by A10, A19, MATRIX_3:1

.= (0. (K,(card N),1)) * (k,l) by A18, A17, MATRIX_3:1 ; :: thesis: verum

.= ColVec2Mx ((card N) |-> (0. K)) by Th32 ;

now :: thesis: for i being Nat st i in (dom A) \ N holds

( Line (A,i) = (width A) |-> (0. K) & Line ((ColVec2Mx ((len A) |-> (0. K))),i) = (width (ColVec2Mx ((len A) |-> (0. K)))) |-> (0. K) )

then
Solutions_of (A,(ColVec2Mx ((len A) |-> (0. K)))) = Solutions_of ((Segm (A,N,(Seg (width A)))),(Segm ((ColVec2Mx ((len A) |-> (0. K))),N,(Seg (width (ColVec2Mx ((len A) |-> (0. K))))))))
by A1, A2, A11, Th45;( Line (A,i) = (width A) |-> (0. K) & Line ((ColVec2Mx ((len A) |-> (0. K))),i) = (width (ColVec2Mx ((len A) |-> (0. K)))) |-> (0. K) )

let i be Nat; :: thesis: ( i in (dom A) \ N implies ( Line (A,i) = (width A) |-> (0. K) & Line ((ColVec2Mx ((len A) |-> (0. K))),i) = (width (ColVec2Mx ((len A) |-> (0. K)))) |-> (0. K) ) )

assume A21: i in (dom A) \ N ; :: thesis: ( Line (A,i) = (width A) |-> (0. K) & Line ((ColVec2Mx ((len A) |-> (0. K))),i) = (width (ColVec2Mx ((len A) |-> (0. K)))) |-> (0. K) )

A22: i in dom A by A21, XBOOLE_0:def 5;

then Line ((ColVec2Mx ((len A) |-> (0. K))),i) = (ColVec2Mx ((len A) |-> (0. K))) . i by A5, A12, MATRIX_0:52

.= ((len A) |-> ((width (ColVec2Mx ((len A) |-> (0. K)))) |-> (0. K))) . i by A10, A13, Th26

.= (width (ColVec2Mx ((len A) |-> (0. K)))) |-> (0. K) by A12, A22, FINSEQ_2:57 ;

hence ( Line (A,i) = (width A) |-> (0. K) & Line ((ColVec2Mx ((len A) |-> (0. K))),i) = (width (ColVec2Mx ((len A) |-> (0. K)))) |-> (0. K) ) by A4, A21; :: thesis: verum

end;assume A21: i in (dom A) \ N ; :: thesis: ( Line (A,i) = (width A) |-> (0. K) & Line ((ColVec2Mx ((len A) |-> (0. K))),i) = (width (ColVec2Mx ((len A) |-> (0. K)))) |-> (0. K) )

A22: i in dom A by A21, XBOOLE_0:def 5;

then Line ((ColVec2Mx ((len A) |-> (0. K))),i) = (ColVec2Mx ((len A) |-> (0. K))) . i by A5, A12, MATRIX_0:52

.= ((len A) |-> ((width (ColVec2Mx ((len A) |-> (0. K)))) |-> (0. K))) . i by A10, A13, Th26

.= (width (ColVec2Mx ((len A) |-> (0. K)))) |-> (0. K) by A12, A22, FINSEQ_2:57 ;

hence ( Line (A,i) = (width A) |-> (0. K) & Line ((ColVec2Mx ((len A) |-> (0. K))),i) = (width (ColVec2Mx ((len A) |-> (0. K)))) |-> (0. K) ) by A4, A21; :: thesis: verum

hence Space_of_Solutions_of A = Space_of_Solutions_of (Segm (A,N,(Seg (width A)))) by A20, A7, A9, A8, VECTSP_4:29; :: thesis: verum