let n, m, l be Nat; for K being Field
for A being Matrix of n,m,K
for B being Matrix of n,l,K
for N being finite without_zero Subset of NAT st card N = n & N c= Seg m & n > 0 & Segm A,(Seg n),N = 1. K,n holds
ex X being Matrix of m,l,K st
( Segm X,((Seg m) \ N),(Seg l) = 0. K,(m -' n),l & Segm X,N,(Seg l) = B & X in Solutions_of A,B )
let K be Field; for A being Matrix of n,m,K
for B being Matrix of n,l,K
for N being finite without_zero Subset of NAT st card N = n & N c= Seg m & n > 0 & Segm A,(Seg n),N = 1. K,n holds
ex X being Matrix of m,l,K st
( Segm X,((Seg m) \ N),(Seg l) = 0. K,(m -' n),l & Segm X,N,(Seg l) = B & X in Solutions_of A,B )
let A be Matrix of n,m,K; for B being Matrix of n,l,K
for N being finite without_zero Subset of NAT st card N = n & N c= Seg m & n > 0 & Segm A,(Seg n),N = 1. K,n holds
ex X being Matrix of m,l,K st
( Segm X,((Seg m) \ N),(Seg l) = 0. K,(m -' n),l & Segm X,N,(Seg l) = B & X in Solutions_of A,B )
let B be Matrix of n,l,K; for N being finite without_zero Subset of NAT st card N = n & N c= Seg m & n > 0 & Segm A,(Seg n),N = 1. K,n holds
ex X being Matrix of m,l,K st
( Segm X,((Seg m) \ N),(Seg l) = 0. K,(m -' n),l & Segm X,N,(Seg l) = B & X in Solutions_of A,B )
let N be finite without_zero Subset of NAT ; ( card N = n & N c= Seg m & n > 0 & Segm A,(Seg n),N = 1. K,n implies ex X being Matrix of m,l,K st
( Segm X,((Seg m) \ N),(Seg l) = 0. K,(m -' n),l & Segm X,N,(Seg l) = B & X in Solutions_of A,B ) )
assume that
A1:
card N = n
and
A2:
N c= Seg m
and
A3:
n > 0
and
A4:
Segm A,(Seg n),N = 1. K,n
; ex X being Matrix of m,l,K st
( Segm X,((Seg m) \ N),(Seg l) = 0. K,(m -' n),l & Segm X,N,(Seg l) = B & X in Solutions_of A,B )
A5:
width A = m
by A3, MATRIX_1:24;
set Z = 0. K,m,l;
set SN = (Seg m) \ N;
A6:
card (Seg m) = m
by FINSEQ_1:78;
then A7:
( m -' n = m - n & card ((Seg m) \ N) = m - n )
by A1, A2, CARD_2:63, NAT_1:44, XREAL_1:235;
set ZERO = 0. K,(m -' n),l;
A8:
N misses (Seg m) \ N
by XBOOLE_1:79;
[:N,(Seg l):] /\ [:((Seg m) \ N),(Seg l):] =
[:(N /\ ((Seg m) \ N)),(Seg l):]
by ZFMISC_1:122
.=
[:{} ,(Seg l):]
by A8, XBOOLE_0:def 7
.=
{}
by ZFMISC_1:113
;
then A9:
for i, j, bi, bj, ci, cj being Nat st [i,j] in [:N,(Seg l):] /\ [:((Seg m) \ N),(Seg l):] & bi = ((Sgm N) " ) . i & bj = ((Sgm (Seg l)) " ) . j & ci = ((Sgm ((Seg m) \ N)) " ) . i & cj = ((Sgm (Seg l)) " ) . j holds
B * bi,bj = (0. K,(m -' n),l) * ci,cj
;
A10:
Indices A = [:(Seg n),(Seg m):]
by A3, MATRIX_1:24;
A11:
n <= card (Seg m)
by A1, A2, NAT_1:44;
then A12:
( len (0. K,m,l) = m & width (0. K,m,l) = l )
by A3, A6, MATRIX_1:24;
A13:
Indices (0. K,m,l) = [:(Seg m),(Seg l):]
by A3, A11, A6, MATRIX_1:24;
then A14:
[:N,(Seg l):] c= Indices (0. K,m,l)
by A2, ZFMISC_1:118;
A15:
(Seg m) \ N c= Seg m
by XBOOLE_1:36;
then
( card (Seg l) = l & [:((Seg m) \ N),(Seg l):] c= Indices (0. K,m,l) )
by A13, FINSEQ_1:78, ZFMISC_1:118;
then consider X being Matrix of m,l,K such that
A16:
Segm X,N,(Seg l) = B
and
A17:
Segm X,((Seg m) \ N),(Seg l) = 0. K,(m -' n),l
and
for i, j being Nat st [i,j] in (Indices X) \ ([:N,(Seg l):] \/ [:((Seg m) \ N),(Seg l):]) holds
X * i,j = (0. K,m,l) * i,j
by A1, A7, A12, A14, A9, Th9;
set AX = A * X;
A18:
len X = m
by A3, A11, A6, MATRIX_1:24;
then A19:
dom X = Seg m
by FINSEQ_1:def 3;
len A = n
by A3, MATRIX_1:24;
then A20:
len (A * X) = n
by A5, A18, MATRIX_3:def 4;
take
X
; ( Segm X,((Seg m) \ N),(Seg l) = 0. K,(m -' n),l & Segm X,N,(Seg l) = B & X in Solutions_of A,B )
thus
( Segm X,((Seg m) \ N),(Seg l) = 0. K,(m -' n),l & Segm X,N,(Seg l) = B )
by A16, A17; X in Solutions_of A,B
A21:
Indices X = [:(Seg m),(Seg l):]
by A3, A11, A6, MATRIX_1:24;
A22:
width B = l
by A3, MATRIX_1:24;
A23:
width X = l
by A3, A11, A6, MATRIX_1:24;
then
width (A * X) = l
by A5, A18, MATRIX_3:def 4;
then reconsider AX = A * X as Matrix of n,l,K by A20, MATRIX_2:7;
A24:
Indices B = [:(Seg n),(Seg l):]
by A3, MATRIX_1:24;
now A25:
[:N,(Seg l):] c= Indices X
by A2, A21, ZFMISC_1:118;
let i,
j be
Nat;
( [i,j] in Indices AX implies AX * i,j = B * i,j )assume A26:
[i,j] in Indices AX
;
AX * i,j = B * i,jreconsider I =
i,
J =
j as
Element of
NAT by ORDINAL1:def 13;
A27:
Indices AX = Indices B
by MATRIX_1:27;
then A28:
i in Seg n
by A24, A26, ZFMISC_1:106;
(
len (Line A,i) = m &
len (Col X,j) = m )
by A5, A18, FINSEQ_1:def 18;
then
len (mlt (Line A,i),(Col X,j)) = m
by MATRIX_3:8;
then A29:
dom (mlt (Line A,i),(Col X,j)) = Seg m
by FINSEQ_1:def 3;
A30:
rng (Sgm (Seg l)) = Seg l
by FINSEQ_1:def 13;
A31:
(
rng (Sgm (Seg n)) = Seg n &
[:(Seg n),N:] c= Indices A )
by A2, A10, FINSEQ_1:def 13, ZFMISC_1:118;
A32:
rng (Sgm N) = N
by A2, FINSEQ_1:def 13;
dom (Sgm N) = Seg n
by A1, A2, FINSEQ_3:45;
then A33:
(Sgm N) . i in N
by A28, A32, FUNCT_1:def 5;
A34:
j in Seg l
by A22, A26, A27, ZFMISC_1:106;
then A35:
j =
(idseq l) . j
by FINSEQ_2:57
.=
(Sgm (Seg l)) . j
by FINSEQ_3:54
;
then
[((Sgm N) . I),((Sgm (Seg l)) . J)] in Indices X
by A2, A21, A34, A33, ZFMISC_1:106;
then A36:
[I,J] in Indices B
by A16, A32, A30, A25, MATRIX13:17;
A37:
rng (Sgm ((Seg m) \ N)) = (Seg m) \ N
by A15, FINSEQ_1:def 13;
A38:
i =
(idseq n) . i
by A28, FINSEQ_2:57
.=
(Sgm (Seg n)) . i
by FINSEQ_3:54
;
then
[((Sgm (Seg n)) . i),((Sgm N) . i)] in Indices A
by A2, A10, A28, A33, ZFMISC_1:106;
then A39:
[I,I] in Indices (1. K,n)
by A4, A32, A31, MATRIX13:17;
A40:
[:((Seg m) \ N),(Seg l):] c= Indices X
by A15, A21, ZFMISC_1:118;
A41:
now let kk be
Nat;
( kk in Seg m & kk <> (Sgm N) . I implies (mlt (Line A,i),(Col X,j)) . b1 = 0. K )assume that A42:
kk in Seg m
and A43:
kk <> (Sgm N) . I
;
(mlt (Line A,i),(Col X,j)) . b1 = 0. Kper cases
( kk in N or kk in (Seg m) \ N )
by A42, XBOOLE_0:def 5;
suppose A44:
kk in N
;
(mlt (Line A,i),(Col X,j)) . b1 = 0. Kthen consider x being
set such that A45:
x in dom (Sgm N)
and A46:
(Sgm N) . x = kk
by A32, FUNCT_1:def 5;
reconsider x =
x as
Element of
NAT by A45;
[((Sgm (Seg n)) . i),((Sgm N) . x)] in Indices A
by A2, A10, A28, A38, A44, A46, ZFMISC_1:106;
then A47:
[I,x] in Indices (1. K,n)
by A4, A32, A31, MATRIX13:17;
A48:
(Col X,j) . kk = X * kk,
j
by A2, A19, A44, MATRIX_1:def 9;
(Line A,i) . ((Sgm N) . x) =
A * I,
((Sgm N) . x)
by A2, A5, A44, A46, MATRIX_1:def 8
.=
(Segm A,(Seg n),N) * I,
x
by A4, A38, A47, MATRIX13:def 1
.=
0. K
by A4, A43, A46, A47, MATRIX_1:def 12
;
hence (mlt (Line A,i),(Col X,j)) . kk =
(0. K) * (X * kk,j)
by A2, A5, A18, A44, A46, A48, FVSUM_1:74
.=
0. K
by VECTSP_1:36
;
verum end; suppose A49:
kk in (Seg m) \ N
;
(mlt (Line A,i),(Col X,j)) . b1 = 0. Kthen consider x being
set such that A50:
x in dom (Sgm ((Seg m) \ N))
and A51:
(Sgm ((Seg m) \ N)) . x = kk
by A37, FUNCT_1:def 5;
reconsider x =
x as
Element of
NAT by A50;
A52:
(Line A,i) . kk = A * I,
((Sgm ((Seg m) \ N)) . x)
by A5, A42, A51, MATRIX_1:def 8;
[((Sgm ((Seg m) \ N)) . x),((Sgm (Seg l)) . J)] in Indices X
by A15, A21, A34, A35, A49, A51, ZFMISC_1:106;
then A53:
[x,J] in Indices (0. K,(m -' n),l)
by A17, A30, A37, A40, MATRIX13:17;
(Col X,j) . kk =
X * ((Sgm ((Seg m) \ N)) . x),
((Sgm (Seg l)) . j)
by A15, A19, A35, A49, A51, MATRIX_1:def 9
.=
(0. K,(m -' n),l) * x,
J
by A17, A53, MATRIX13:def 1
.=
0. K
by A53, MATRIX_3:3
;
hence (mlt (Line A,i),(Col X,j)) . kk =
(A * I,((Sgm ((Seg m) \ N)) . x)) * (0. K)
by A5, A18, A42, A52, FVSUM_1:74
.=
0. K
by VECTSP_1:36
;
verum end; end; A54:
(Col X,j) . ((Sgm N) . i) =
X * ((Sgm N) . i),
j
by A2, A19, A33, MATRIX_1:def 9
.=
B * I,
J
by A16, A35, A36, MATRIX13:def 1
;
(Line A,i) . ((Sgm N) . i) =
A * I,
((Sgm N) . I)
by A2, A5, A33, MATRIX_1:def 8
.=
(Segm A,(Seg n),N) * I,
I
by A4, A38, A39, MATRIX13:def 1
.=
1_ K
by A4, A39, MATRIX_1:def 12
;
then A55:
(mlt (Line A,i),(Col X,j)) . ((Sgm N) . i) =
(1_ K) * (B * I,J)
by A2, A5, A18, A33, A54, FVSUM_1:74
.=
B * I,
J
by VECTSP_1:def 13
;
AX * i,
j =
(Line A,i) "*" (Col X,j)
by A5, A18, A26, MATRIX_3:def 4
.=
Sum (mlt (Line A,i),(Col X,j))
;
hence
AX * i,
j = B * i,
j
by A2, A33, A55, A29, A41, MATRIX_3:14;
verum end;
then
AX = B
by MATRIX_1:28;
hence
X in Solutions_of A,B
by A5, A22, A18, A23; verum