let m be Nat; for K being Field
for W being strict Subspace of m -VectSp_over K st dim W < m holds
ex A being Matrix of m -' (dim W),m,K ex N being finite without_zero Subset of NAT st
( card N = m -' (dim W) & N c= Seg m & Segm (A,(Seg (m -' (dim W))),N) = 1. (K,(m -' (dim W))) & W = Space_of_Solutions_of A )
let K be Field; for W being strict Subspace of m -VectSp_over K st dim W < m holds
ex A being Matrix of m -' (dim W),m,K ex N being finite without_zero Subset of NAT st
( card N = m -' (dim W) & N c= Seg m & Segm (A,(Seg (m -' (dim W))),N) = 1. (K,(m -' (dim W))) & W = Space_of_Solutions_of A )
let W be strict Subspace of m -VectSp_over K; ( dim W < m implies ex A being Matrix of m -' (dim W),m,K ex N being finite without_zero Subset of NAT st
( card N = m -' (dim W) & N c= Seg m & Segm (A,(Seg (m -' (dim W))),N) = 1. (K,(m -' (dim W))) & W = Space_of_Solutions_of A ) )
assume A1:
dim W < m
; ex A being Matrix of m -' (dim W),m,K ex N being finite without_zero Subset of NAT st
( card N = m -' (dim W) & N c= Seg m & Segm (A,(Seg (m -' (dim W))),N) = 1. (K,(m -' (dim W))) & W = Space_of_Solutions_of A )
per cases
( dim W = 0 or dim W > 0 )
;
suppose A2:
dim W = 0
;
ex A being Matrix of m -' (dim W),m,K ex N being finite without_zero Subset of NAT st
( card N = m -' (dim W) & N c= Seg m & Segm (A,(Seg (m -' (dim W))),N) = 1. (K,(m -' (dim W))) & W = Space_of_Solutions_of A )then
m -' (dim W) = m
by NAT_D:40;
then reconsider ONE =
1. (
K,
m) as
Matrix of
m -' (dim W),
m,
K ;
take
ONE
;
ex N being finite without_zero Subset of NAT st
( card N = m -' (dim W) & N c= Seg m & Segm (ONE,(Seg (m -' (dim W))),N) = 1. (K,(m -' (dim W))) & W = Space_of_Solutions_of ONE )take
Seg m
;
( card (Seg m) = m -' (dim W) & Seg m c= Seg m & Segm (ONE,(Seg (m -' (dim W))),(Seg m)) = 1. (K,(m -' (dim W))) & W = Space_of_Solutions_of ONE )A3:
len (1. (K,m)) = m
by MATRIX_0:24;
A4:
dim (Space_of_Solutions_of ONE) = 0
by Lm8;
A5:
m -' (dim W) = m
by A2, NAT_D:40;
A6:
width (1. (K,m)) = m
by MATRIX_0:24;
Space_of_Solutions_of ONE =
(Omega). (Space_of_Solutions_of ONE)
.=
(0). (Space_of_Solutions_of ONE)
by A4, VECTSP_9:29
.=
(0). W
by A6, VECTSP_4:37
.=
(Omega). W
by A2, VECTSP_9:29
.=
W
;
hence
(
card (Seg m) = m -' (dim W) &
Seg m c= Seg m &
Segm (
ONE,
(Seg (m -' (dim W))),
(Seg m))
= 1. (
K,
(m -' (dim W))) &
W = Space_of_Solutions_of ONE )
by A5, A3, A6, FINSEQ_1:57, MATRIX13:46;
verum end; suppose A7:
dim W > 0
;
ex A being Matrix of m -' (dim W),m,K ex N being finite without_zero Subset of NAT st
( card N = m -' (dim W) & N c= Seg m & Segm (A,(Seg (m -' (dim W))),N) = 1. (K,(m -' (dim W))) & W = Space_of_Solutions_of A )set ZERO =
0. (
K,
(m -' (dim W)),
m);
A8:
m - (dim W) > (dim W) - (dim W)
by A1, XREAL_1:9;
A9:
m -' (dim W) = m - (dim W)
by A1, XREAL_1:233;
then A10:
(
len (0. (K,(m -' (dim W)),m)) = m -' (dim W) &
width (0. (K,(m -' (dim W)),m)) = m )
by A8, MATRIX_0:23;
A11:
card (Seg m) = m
by FINSEQ_1:57;
consider A being
Matrix of
dim W,
m,
K,
N being
finite without_zero Subset of
NAT such that A12:
N c= Seg m
and A13:
dim W = card N
and A14:
Segm (
A,
(Seg (dim W)),
N)
= 1. (
K,
(dim W))
and
the_rank_of A = dim W
and A15:
lines A is
Basis of
W
by Th70;
set SA =
Segm (
A,
(Seg (dim W)),
((Seg m) \ N));
A16:
card ((Seg m) \ N) = (card (Seg m)) - (card N)
by A12, CARD_2:44;
then A17:
width (Segm (A,(Seg (dim W)),((Seg m) \ N))) = m - (card N)
by A7, A11, MATRIX_0:23;
A18:
card (Seg (dim W)) = dim W
by FINSEQ_1:57;
then
len (Segm (A,(Seg (dim W)),((Seg m) \ N))) = dim W
by A7, MATRIX_0:23;
then
width ((Segm (A,(Seg (dim W)),((Seg m) \ N))) @) = dim W
by A13, A8, A17, MATRIX_0:54;
then A19:
width (- ((Segm (A,(Seg (dim W)),((Seg m) \ N))) @)) = dim W
by MATRIX_3:def 2;
A20:
card (Seg (m -' (dim W))) = m -' (dim W)
by FINSEQ_1:57;
m -' (dim W) = m - (dim W)
by A1, XREAL_1:233;
then reconsider CC =
1. (
K,
(m -' (dim W))) as
Matrix of
card (Seg (m -' (dim W))),
card ((Seg m) \ N),
K by A13, A16, A11, A20;
A21:
(
(Seg m) \ ((Seg m) \ N) = (Seg m) /\ N &
m -' (m -' (dim W)) = m - (m -' (dim W)) )
by NAT_D:35, XBOOLE_1:48, XREAL_1:233;
A22:
Indices (0. (K,(m -' (dim W)),m)) = [:(Seg (m -' (dim W))),(Seg m):]
by A9, A8, MATRIX_0:23;
then A23:
[:(Seg (m -' (dim W))),N:] c= Indices (0. (K,(m -' (dim W)),m))
by A12, ZFMISC_1:95;
len ((Segm (A,(Seg (dim W)),((Seg m) \ N))) @) = m - (dim W)
by A13, A8, A17, MATRIX_0:54;
then
len (- ((Segm (A,(Seg (dim W)),((Seg m) \ N))) @)) = m -' (dim W)
by A9, MATRIX_3:def 2;
then reconsider BB =
- ((Segm (A,(Seg (dim W)),((Seg m) \ N))) @) as
Matrix of
card (Seg (m -' (dim W))),
card N,
K by A13, A20, A19, MATRIX_0:51;
A24:
N misses (Seg m) \ N
by XBOOLE_1:79;
A25:
(Seg m) \ N c= Seg m
by XBOOLE_1:36;
then A26:
[:(Seg (m -' (dim W))),((Seg m) \ N):] c= Indices (0. (K,(m -' (dim W)),m))
by A22, ZFMISC_1:95;
[:(Seg (m -' (dim W))),N:] /\ [:(Seg (m -' (dim W))),((Seg m) \ N):] =
[:(Seg (m -' (dim W))),(N /\ ((Seg m) \ N)):]
by ZFMISC_1:99
.=
[:(Seg (m -' (dim W))),{}:]
by A24
.=
{}
by ZFMISC_1:90
;
then
for
i,
j,
bi,
bj,
ci,
cj being
Nat st
[i,j] in [:(Seg (m -' (dim W))),N:] /\ [:(Seg (m -' (dim W))),((Seg m) \ N):] &
bi = ((Sgm (Seg (m -' (dim W)))) ") . i &
bj = ((Sgm N) ") . j &
ci = ((Sgm (Seg (m -' (dim W)))) ") . i &
cj = ((Sgm ((Seg m) \ N)) ") . j holds
BB * (
bi,
bj)
= CC * (
ci,
cj)
;
then consider M being
Matrix of
m -' (dim W),
m,
K such that A27:
Segm (
M,
(Seg (m -' (dim W))),
N)
= BB
and A28:
Segm (
M,
(Seg (m -' (dim W))),
((Seg m) \ N))
= CC
and
for
i,
j being
Nat st
[i,j] in (Indices M) \ ([:(Seg (m -' (dim W))),N:] \/ [:(Seg (m -' (dim W))),((Seg m) \ N):]) holds
M * (
i,
j)
= (0. (K,(m -' (dim W)),m)) * (
i,
j)
by A10, A23, A26, Th9;
(Seg m) /\ N = N
by A12, XBOOLE_1:28;
then consider MV being
Matrix of
dim W,
m,
K such that A29:
Segm (
MV,
(Seg (dim W)),
N)
= 1. (
K,
(dim W))
and A30:
Segm (
MV,
(Seg (dim W)),
((Seg m) \ N))
= - ((Segm (M,(Seg (m -' (dim W))),N)) @)
and A31:
Lin (lines MV) = Space_of_Solutions_of M
by A7, A13, A9, A8, A16, A11, A28, A21, Th67, XBOOLE_1:36;
A32:
now for i, j being Nat st [i,j] in Indices A holds
A * (i,j) = MV * (i,j)A33:
Indices A = [:(Seg (dim W)),(Seg m):]
by A7, MATRIX_0:23;
let i,
j be
Nat;
( [i,j] in Indices A implies A * (i,j) = MV * (i,j) )assume A34:
[i,j] in Indices A
;
A * (i,j) = MV * (i,j)A35:
i in Seg (dim W)
by A34, A33, ZFMISC_1:87;
A36:
Indices A = Indices MV
by MATRIX_0:26;
A37:
rng (Sgm (Seg (dim W))) = Seg (dim W)
by FINSEQ_1:def 13;
dom (Sgm (Seg (dim W))) = Seg (dim W)
by A18, FINSEQ_3:40;
then consider x being
object such that A38:
x in Seg (dim W)
and A39:
(Sgm (Seg (dim W))) . x = i
by A35, A37, FUNCT_1:def 3;
reconsider x =
x as
Element of
NAT by A38;
A40:
j in Seg m
by A34, A33, ZFMISC_1:87;
now A * (i,j) = MV * (i,j)per cases
( j in N or not j in N )
;
suppose A41:
j in N
;
A * (i,j) = MV * (i,j)then A42:
[i,j] in [:(Seg (dim W)),N:]
by A35, ZFMISC_1:87;
A43:
rng (Sgm N) = N
by A12, FINSEQ_1:def 13;
dom (Sgm N) = Seg (dim W)
by A12, A13, FINSEQ_3:40;
then consider y being
object such that A44:
y in Seg (dim W)
and A45:
(Sgm N) . y = j
by A41, A43, FUNCT_1:def 3;
reconsider y =
y as
Element of
NAT by A44;
A46:
[:(Seg (dim W)),N:] c= Indices A
by A12, A33, ZFMISC_1:95;
then A47:
[x,y] in Indices (Segm (MV,(Seg (dim W)),N))
by A36, A37, A39, A43, A45, A42, MATRIX13:17;
[x,y] in Indices (Segm (A,(Seg (dim W)),N))
by A37, A39, A43, A45, A46, A42, MATRIX13:17;
hence A * (
i,
j) =
(Segm (MV,(Seg (dim W)),N)) * (
x,
y)
by A14, A29, A39, A45, MATRIX13:def 1
.=
MV * (
i,
j)
by A39, A45, A47, MATRIX13:def 1
;
verum end; suppose
not
j in N
;
MV * (i,j) = A * (i,j)then A48:
j in (Seg m) \ N
by A40, XBOOLE_0:def 5;
then A49:
[i,j] in [:(Seg (dim W)),((Seg m) \ N):]
by A35, ZFMISC_1:87;
A50:
rng (Sgm ((Seg m) \ N)) = (Seg m) \ N
by A25, FINSEQ_1:def 13;
dom (Sgm ((Seg m) \ N)) = Seg (m -' (dim W))
by A13, A9, A16, A11, FINSEQ_3:40, XBOOLE_1:36;
then consider y being
object such that A51:
y in Seg (m -' (dim W))
and A52:
(Sgm ((Seg m) \ N)) . y = j
by A48, A50, FUNCT_1:def 3;
reconsider y =
y as
Element of
NAT by A51;
A53:
[:(Seg (dim W)),((Seg m) \ N):] c= Indices A
by A25, A33, ZFMISC_1:95;
then A54:
[x,y] in Indices (Segm (A,(Seg (dim W)),((Seg m) \ N)))
by A37, A39, A50, A52, A49, MATRIX13:17;
A55:
[x,y] in Indices (Segm (MV,(Seg (dim W)),((Seg m) \ N)))
by A36, A37, A39, A50, A52, A53, A49, MATRIX13:17;
then A56:
[x,y] in Indices ((Segm (M,(Seg (m -' (dim W))),N)) @)
by A30, Lm1;
then A57:
[y,x] in Indices (Segm (M,(Seg (m -' (dim W))),N))
by MATRIX_0:def 6;
then A58:
[y,x] in Indices ((Segm (A,(Seg (dim W)),((Seg m) \ N))) @)
by A27, Lm1;
thus MV * (
i,
j) =
(- ((Segm (M,(Seg (m -' (dim W))),N)) @)) * (
x,
y)
by A30, A39, A52, A55, MATRIX13:def 1
.=
- (((Segm (M,(Seg (m -' (dim W))),N)) @) * (x,y))
by A56, MATRIX_3:def 2
.=
- ((- ((Segm (A,(Seg (dim W)),((Seg m) \ N))) @)) * (y,x))
by A27, A57, MATRIX_0:def 6
.=
- (- (((Segm (A,(Seg (dim W)),((Seg m) \ N))) @) * (y,x)))
by A58, MATRIX_3:def 2
.=
((Segm (A,(Seg (dim W)),((Seg m) \ N))) @) * (
y,
x)
by RLVECT_1:17
.=
(Segm (A,(Seg (dim W)),((Seg m) \ N))) * (
x,
y)
by A54, MATRIX_0:def 6
.=
A * (
i,
j)
by A39, A52, A54, MATRIX13:def 1
;
verum end; hence
A * (
i,
j)
= MV * (
i,
j)
;
verum end; then reconsider lA =
lines MV as
Subset of
W by A15, MATRIX_0:27;
take
M
;
ex N being finite without_zero Subset of NAT st
( card N = m -' (dim W) & N c= Seg m & Segm (M,(Seg (m -' (dim W))),N) = 1. (K,(m -' (dim W))) & W = Space_of_Solutions_of M )take
(Seg m) \ N
;
( card ((Seg m) \ N) = m -' (dim W) & (Seg m) \ N c= Seg m & Segm (M,(Seg (m -' (dim W))),((Seg m) \ N)) = 1. (K,(m -' (dim W))) & W = Space_of_Solutions_of M )
MV = A
by A32, MATRIX_0:27;
then
Lin lA = ModuleStr(# the
carrier of
W, the
addF of
W, the
ZeroF of
W, the
lmult of
W #)
by A15, VECTSP_7:def 3;
hence
(
card ((Seg m) \ N) = m -' (dim W) &
(Seg m) \ N c= Seg m &
Segm (
M,
(Seg (m -' (dim W))),
((Seg m) \ N))
= 1. (
K,
(m -' (dim W))) &
W = Space_of_Solutions_of M )
by A1, A13, A16, A11, A28, A31, VECTSP_9:17, XBOOLE_1:36, XREAL_1:233;
verum end;