let K be Field; 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; 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; ( 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)
; 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 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)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;
( [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)))))))
;
(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
;
verum end;
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
.=
ColVec2Mx ((card N) |-> (0. K))
by Th32
;
now 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) )let i be
Nat;
( 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
;
( 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;
verum end;
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;
hence
Space_of_Solutions_of A = Space_of_Solutions_of (Segm (A,N,(Seg (width A))))
by A20, A7, A9, A8, VECTSP_4:29; verum