let m be Nat; :: thesis: 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; :: thesis: 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; :: thesis: ( 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
; :: thesis: 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
;
:: thesis: 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 reconsider ONE =
1. K,
m as
Matrix of
m -' (dim W),
m,
K by NAT_D:40;
A3:
m -' (dim W) = m
by A2, NAT_D:40;
take
ONE
;
:: thesis: 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 N =
Seg m;
:: thesis: ( 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 )A4:
(
len (1. K,m) = m &
width (1. K,m) = m &
card N = m )
by FINSEQ_1:78, MATRIX_1:25;
A5:
dim (Space_of_Solutions_of ONE) = 0
by Lm8;
Space_of_Solutions_of ONE =
(Omega). (Space_of_Solutions_of ONE)
.=
(0). (Space_of_Solutions_of ONE)
by A5, VECTSP_9:33
.=
(0). W
by A4, VECTSP_4:48
.=
(Omega). W
by A2, VECTSP_9:33
.=
W
;
hence
(
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 )
by A4, A3, MATRIX13:46;
:: thesis: verum end; suppose A6:
dim W > 0
;
:: thesis: 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 )consider A being
Matrix of
dim W,
m,
K,
N being
finite without_zero Subset of
NAT such that A7:
(
N c= Seg m &
dim W = card N )
and A8:
Segm A,
(Seg (dim W)),
N = 1. K,
(dim W)
and A9:
(
the_rank_of A = dim W &
lines A is
Basis of
W )
by Th70;
set ZERO =
0. K,
(m -' (dim W)),
m;
A10:
(
m -' (dim W) = m - (dim W) &
m - (dim W) > (dim W) - (dim W) )
by A1, XREAL_1:11, XREAL_1:235;
then A11:
(
len (0. K,(m -' (dim W)),m) = m -' (dim W) &
width (0. K,(m -' (dim W)),m) = m &
Indices (0. K,(m -' (dim W)),m) = [:(Seg (m -' (dim W))),(Seg m):] &
card (Seg (m -' (dim W))) = m -' (dim W) )
by FINSEQ_1:78, MATRIX_1:24;
set SA =
Segm A,
(Seg (dim W)),
((Seg m) \ N);
A12:
(
card ((Seg m) \ N) = (card (Seg m)) - (card N) &
card (Seg (m -' (dim W))) = m -' (dim W) &
card (Seg (dim W)) = dim W &
card (Seg m) = m )
by A7, CARD_2:63, FINSEQ_1:78;
then reconsider CC =
1. K,
(m -' (dim W)) as
Matrix of
card (Seg (m -' (dim W))),
card ((Seg m) \ N),
K by A1, A7, XREAL_1:235;
(
len (Segm A,(Seg (dim W)),((Seg m) \ N)) = dim W &
width (Segm A,(Seg (dim W)),((Seg m) \ N)) = m - (card N) )
by A6, A12, MATRIX_1:24;
then
(
len ((Segm A,(Seg (dim W)),((Seg m) \ N)) @ ) = m - (dim W) &
width ((Segm A,(Seg (dim W)),((Seg m) \ N)) @ ) = dim W )
by A7, A10, MATRIX_2:12;
then
(
len (- ((Segm A,(Seg (dim W)),((Seg m) \ N)) @ )) = m -' (dim W) &
width (- ((Segm A,(Seg (dim W)),((Seg m) \ N)) @ )) = dim W )
by A10, 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 A7, A12, MATRIX_2:7;
A13:
(Seg m) \ N c= Seg m
by XBOOLE_1:36;
then A14:
(
[:(Seg (m -' (dim W))),N:] c= Indices (0. K,(m -' (dim W)),m) &
(Seg m) \ ((Seg m) \ N) = (Seg m) /\ N &
[:(Seg (m -' (dim W))),((Seg m) \ N):] c= Indices (0. K,(m -' (dim W)),m) &
(Seg m) /\ N = N )
by A11, A7, XBOOLE_1:28, XBOOLE_1:48, ZFMISC_1:118;
A15:
N misses (Seg m) \ N
by XBOOLE_1:79;
[:(Seg (m -' (dim W))),N:] /\ [:(Seg (m -' (dim W))),((Seg m) \ N):] =
[:(Seg (m -' (dim W))),(N /\ ((Seg m) \ N)):]
by ZFMISC_1:122
.=
[:(Seg (m -' (dim W))),{} :]
by A15, XBOOLE_0:def 7
.=
{}
by ZFMISC_1:113
;
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 A16:
(
Segm M,
(Seg (m -' (dim W))),
N = BB &
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 Th9, A11, A14;
m -' (m -' (dim W)) = m - (m -' (dim W))
by NAT_D:35, XREAL_1:235;
then consider MV being
Matrix of
dim W,
m,
K such that A17:
Segm MV,
(Seg (dim W)),
N = 1. K,
(dim W)
and A18:
Segm MV,
(Seg (dim W)),
((Seg m) \ N) = - ((Segm M,(Seg (m -' (dim W))),N) @ )
and A19:
Lin (lines MV) = Space_of_Solutions_of M
by A6, A7, A10, A12, A14, A16, A13, Th67;
A20:
now let i,
j be
Nat;
:: thesis: ( [i,j] in Indices A implies A * i,j = MV * i,j )assume A21:
[i,j] in Indices A
;
:: thesis: A * i,j = MV * i,jA22:
(
Indices A = [:(Seg (dim W)),(Seg m):] &
Indices A = Indices MV )
by A6, MATRIX_1:24, MATRIX_1:27;
then A23:
(
i in Seg (dim W) &
rng (Sgm (Seg (dim W))) = Seg (dim W) &
dom (Sgm (Seg (dim W))) = Seg (dim W) &
j in Seg m )
by A21, A12, FINSEQ_1:def 13, FINSEQ_3:45, ZFMISC_1:106;
then consider x being
set such that A24:
(
x in Seg (dim W) &
(Sgm (Seg (dim W))) . x = i )
by FUNCT_1:def 5;
reconsider x =
x as
Element of
NAT by A24;
now per cases
( j in N or not j in N )
;
suppose A25:
j in N
;
:: thesis: A * i,j = MV * i,jA26:
(
rng (Sgm N) = N &
dom (Sgm N) = Seg (dim W) )
by A7, FINSEQ_1:def 13, FINSEQ_3:45;
then consider y being
set such that A27:
(
y in Seg (dim W) &
(Sgm N) . y = j )
by A25, FUNCT_1:def 5;
reconsider y =
y as
Element of
NAT by A27;
(
[:(Seg (dim W)),N:] c= Indices A &
[i,j] in [:(Seg (dim W)),N:] )
by A7, A22, A23, A25, ZFMISC_1:106, ZFMISC_1:118;
then A28:
(
[x,y] in Indices (Segm A,(Seg (dim W)),N) &
[x,y] in Indices (Segm MV,(Seg (dim W)),N) )
by A22, A23, A24, A26, A27, MATRIX13:17;
hence A * i,
j =
(Segm MV,(Seg (dim W)),N) * x,
y
by A8, A24, A27, A17, MATRIX13:def 1
.=
MV * i,
j
by A24, A27, A28, MATRIX13:def 1
;
:: thesis: verum end; suppose
not
j in N
;
:: thesis: MV * i,j = A * i,jthen A29:
j in (Seg m) \ N
by A23, XBOOLE_0:def 5;
A30:
(
rng (Sgm ((Seg m) \ N)) = (Seg m) \ N &
dom (Sgm ((Seg m) \ N)) = Seg (m -' (dim W)) )
by A7, A12, A13, A10, FINSEQ_1:def 13, FINSEQ_3:45;
then consider y being
set such that A31:
(
y in Seg (m -' (dim W)) &
(Sgm ((Seg m) \ N)) . y = j )
by A29, FUNCT_1:def 5;
reconsider y =
y as
Element of
NAT by A31;
(
[:(Seg (dim W)),((Seg m) \ N):] c= Indices A &
[i,j] in [:(Seg (dim W)),((Seg m) \ N):] )
by A22, A23, A29, A13, ZFMISC_1:106, ZFMISC_1:118;
then A32:
(
[x,y] in Indices (Segm A,(Seg (dim W)),((Seg m) \ N)) &
[x,y] in Indices (Segm MV,(Seg (dim W)),((Seg m) \ N)) )
by A22, A23, A24, A30, A31, MATRIX13:17;
then A33:
[x,y] in Indices ((Segm M,(Seg (m -' (dim W))),N) @ )
by A18, Lm1;
then A34:
[y,x] in Indices (Segm M,(Seg (m -' (dim W))),N)
by MATRIX_1:def 7;
then A35:
[y,x] in Indices ((Segm A,(Seg (dim W)),((Seg m) \ N)) @ )
by Lm1, A16;
thus MV * i,
j =
(- ((Segm M,(Seg (m -' (dim W))),N) @ )) * x,
y
by A24, A31, A32, A18, MATRIX13:def 1
.=
- (((Segm M,(Seg (m -' (dim W))),N) @ ) * x,y)
by A33, MATRIX_3:def 2
.=
- ((- ((Segm A,(Seg (dim W)),((Seg m) \ N)) @ )) * y,x)
by A16, A34, MATRIX_1:def 7
.=
- (- (((Segm A,(Seg (dim W)),((Seg m) \ N)) @ ) * y,x))
by A35, MATRIX_3:def 2
.=
((Segm A,(Seg (dim W)),((Seg m) \ N)) @ ) * y,
x
by RLVECT_1:30
.=
(Segm A,(Seg (dim W)),((Seg m) \ N)) * x,
y
by A32, MATRIX_1:def 7
.=
A * i,
j
by A24, A31, A32, MATRIX13:def 1
;
:: thesis: verum end; hence
A * i,
j = MV * i,
j
;
:: thesis: verum end; take
M
;
:: thesis: 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 NN =
(Seg m) \ N;
:: thesis: ( card NN = m -' (dim W) & NN c= Seg m & Segm M,(Seg (m -' (dim W))),NN = 1. K,(m -' (dim W)) & W = Space_of_Solutions_of M )reconsider lA =
lines MV as
Subset of
W by A9, A20, MATRIX_1:28;
MV = A
by A20, MATRIX_1:28;
then
Lin lA = VectSpStr(# the
carrier of
W,the
addF of
W,the
U2 of
W,the
lmult of
W #)
by A9, VECTSP_7:def 3;
hence
(
card NN = m -' (dim W) &
NN c= Seg m &
Segm M,
(Seg (m -' (dim W))),
NN = 1. K,
(m -' (dim W)) &
W = Space_of_Solutions_of M )
by A16, A19, A7, A1, A12, VECTSP_9:21, XBOOLE_1:36, XREAL_1:235;
:: thesis: verum end;