let l, m, n 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_0:23;
set Z = 0. (K,m,l);
set SN = (Seg m) \ N;
A6:
card (Seg m) = m
by FINSEQ_1:57;
then A7:
( m -' n = m - n & card ((Seg m) \ N) = m - n )
by A1, A2, CARD_2:44, NAT_1:43, XREAL_1:233;
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:99
.=
[:{},(Seg l):]
by A8
.=
{}
by ZFMISC_1:90
;
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_0:23;
A11:
n <= card (Seg m)
by A1, A2, NAT_1:43;
then A12:
( len (0. (K,m,l)) = m & width (0. (K,m,l)) = l )
by A3, A6, MATRIX_0:23;
A13:
Indices (0. (K,m,l)) = [:(Seg m),(Seg l):]
by A3, A11, A6, MATRIX_0:23;
then A14:
[:N,(Seg l):] c= Indices (0. (K,m,l))
by A2, ZFMISC_1:95;
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:57, ZFMISC_1:95;
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_0:23;
then A19:
dom X = Seg m
by FINSEQ_1:def 3;
len A = n
by A3, MATRIX_0:23;
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_0:23;
A22:
width B = l
by A3, MATRIX_0:23;
A23:
width X = l
by A3, A11, A6, MATRIX_0:23;
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_0:51;
A24:
Indices B = [:(Seg n),(Seg l):]
by A3, MATRIX_0:23;
now for i, j being Nat st [i,j] in Indices AX holds
AX * (i,j) = B * (i,j)A25:
[:N,(Seg l):] c= Indices X
by A2, A21, ZFMISC_1:95;
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,j)reconsider I =
i,
J =
j as
Element of
NAT by ORDINAL1:def 12;
A27:
Indices AX = Indices B
by MATRIX_0:26;
then A28:
i in Seg n
by A24, A26, ZFMISC_1:87;
(
len (Line (A,i)) = m &
len (Col (X,j)) = m )
by A5, A18, CARD_1:def 7;
then
len (mlt ((Line (A,i)),(Col (X,j)))) = m
by MATRIX_3:6;
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:95;
A32:
rng (Sgm N) = N
by A2, FINSEQ_1:def 13;
dom (Sgm N) = Seg n
by A1, A2, FINSEQ_3:40;
then A33:
(Sgm N) . i in N
by A28, A32, FUNCT_1:def 3;
A34:
j in Seg l
by A22, A26, A27, ZFMISC_1:87;
then A35:
j =
(idseq l) . j
by FINSEQ_2:49
.=
(Sgm (Seg l)) . j
by FINSEQ_3:48
;
then
[((Sgm N) . I),((Sgm (Seg l)) . J)] in Indices X
by A2, A21, A34, A33, ZFMISC_1:87;
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:49
.=
(Sgm (Seg n)) . i
by FINSEQ_3:48
;
then
[((Sgm (Seg n)) . i),((Sgm N) . i)] in Indices A
by A2, A10, A28, A33, ZFMISC_1:87;
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:95;
A41:
now for kk being Nat st kk in Seg m & kk <> (Sgm N) . I holds
(mlt ((Line (A,i)),(Col (X,j)))) . kk = 0. Klet 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
object such that A45:
x in dom (Sgm N)
and A46:
(Sgm N) . x = kk
by A32, FUNCT_1:def 3;
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:87;
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_0:def 8;
(Line (A,i)) . ((Sgm N) . x) =
A * (
I,
((Sgm N) . x))
by A2, A5, A44, A46, MATRIX_0:def 7
.=
(Segm (A,(Seg n),N)) * (
I,
x)
by A4, A38, A47, MATRIX13:def 1
.=
0. K
by A4, A43, A46, A47, MATRIX_1:def 3
;
hence (mlt ((Line (A,i)),(Col (X,j)))) . kk =
(0. K) * (X * (kk,j))
by A2, A5, A18, A44, A46, A48, FVSUM_1:61
.=
0. K
;
verum end; suppose A49:
kk in (Seg m) \ N
;
(mlt ((Line (A,i)),(Col (X,j)))) . b1 = 0. Kthen consider x being
object such that A50:
x in dom (Sgm ((Seg m) \ N))
and A51:
(Sgm ((Seg m) \ N)) . x = kk
by A37, FUNCT_1:def 3;
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_0:def 7;
[((Sgm ((Seg m) \ N)) . x),((Sgm (Seg l)) . J)] in Indices X
by A15, A21, A34, A35, A49, A51, ZFMISC_1:87;
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_0:def 8
.=
(0. (K,(m -' n),l)) * (
x,
J)
by A17, A53, MATRIX13:def 1
.=
0. K
by A53, MATRIX_3:1
;
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:61
.=
0. K
;
verum end; end; A54:
(Col (X,j)) . ((Sgm N) . i) =
X * (
((Sgm N) . i),
j)
by A2, A19, A33, MATRIX_0:def 8
.=
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_0:def 7
.=
(Segm (A,(Seg n),N)) * (
I,
I)
by A4, A38, A39, MATRIX13:def 1
.=
1_ K
by A4, A39, MATRIX_1:def 3
;
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:61
.=
B * (
I,
J)
;
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:12;
verum end;
then
AX = B
by MATRIX_0:27;
hence
X in Solutions_of (A,B)
by A5, A22, A18, A23; verum