let m, n be Nat; for K being Field
for M being Matrix of m,n,K
for U being Subset of (n -VectSp_over K) st U c= lines M holds
ex P being finite without_zero Subset of NAT st
( P c= Seg m & lines (Segm (M,P,(Seg n))) = U & Segm (M,P,(Seg n)) is without_repeated_line )
let K be Field; for M being Matrix of m,n,K
for U being Subset of (n -VectSp_over K) st U c= lines M holds
ex P being finite without_zero Subset of NAT st
( P c= Seg m & lines (Segm (M,P,(Seg n))) = U & Segm (M,P,(Seg n)) is without_repeated_line )
let M be Matrix of m,n,K; for U being Subset of (n -VectSp_over K) st U c= lines M holds
ex P being finite without_zero Subset of NAT st
( P c= Seg m & lines (Segm (M,P,(Seg n))) = U & Segm (M,P,(Seg n)) is without_repeated_line )
defpred S1[ object , object ] means ex i being Nat st
( i in Seg m & Line (M,i) = $1 & $2 = i );
let U be Subset of (n -VectSp_over K); ( U c= lines M implies ex P being finite without_zero Subset of NAT st
( P c= Seg m & lines (Segm (M,P,(Seg n))) = U & Segm (M,P,(Seg n)) is without_repeated_line ) )
assume A1:
U c= lines M
; ex P being finite without_zero Subset of NAT st
( P c= Seg m & lines (Segm (M,P,(Seg n))) = U & Segm (M,P,(Seg n)) is without_repeated_line )
A2:
for x being object st x in U holds
ex y being object st
( y in Seg m & S1[x,y] )
consider f being Function of U,(Seg m) such that
A5:
for x being object st x in U holds
S1[x,f . x]
from FUNCT_2:sch 1(A2);
A6:
rng f c= Seg m
by RELAT_1:def 19;
then
not 0 in rng f
;
then reconsider P = rng f as finite without_zero Subset of NAT by A6, MEASURE6:def 2, XBOOLE_1:1;
set S = Segm (M,P,(Seg n));
A7:
rng (Sgm P) = P
by A6, FINSEQ_1:def 13;
A8:
lines (Segm (M,P,(Seg n))) c= U
proof
A9:
rng (Sgm P) = P
by A6, FINSEQ_1:def 13;
let x be
object ;
TARSKI:def 3 ( not x in lines (Segm (M,P,(Seg n))) or x in U )
A10:
dom (Segm (M,P,(Seg n))) =
Seg (len (Segm (M,P,(Seg n))))
by FINSEQ_1:def 3
.=
Seg (card P)
by MATRIX_0:def 2
;
assume A11:
x in lines (Segm (M,P,(Seg n)))
;
x in U
then consider y being
object such that A12:
y in dom (Segm (M,P,(Seg n)))
and A13:
(Segm (M,P,(Seg n))) . y = x
by FUNCT_1:def 3;
lines (Segm (M,P,(Seg n))) c= lines M
by A6, Th118;
then A14:
M <> {}
by A11;
len M = m
by MATRIX_0:def 2;
then A15:
width M = n
by A14, Th1;
reconsider y =
y as
Element of
NAT by A12;
dom (Sgm P) = Seg (card P)
by A6, FINSEQ_3:40;
then
(Sgm P) . y in rng (Sgm P)
by A12, A10, FUNCT_1:def 3;
then consider z being
object such that A16:
z in dom f
and A17:
f . z = (Sgm P) . y
by A9, FUNCT_1:def 3;
ex
i being
Nat st
(
i in Seg m &
Line (
M,
i)
= z &
f . z = i )
by A5, A16;
then z =
Line (
(Segm (M,P,(Seg n))),
y)
by A12, A10, A17, A15, Th48
.=
x
by A12, A13, A10, MATRIX_0:52
;
hence
x in U
by A16;
verum
end;
take
P
; ( P c= Seg m & lines (Segm (M,P,(Seg n))) = U & Segm (M,P,(Seg n)) is without_repeated_line )
thus
P c= Seg m
by RELAT_1:def 19; ( lines (Segm (M,P,(Seg n))) = U & Segm (M,P,(Seg n)) is without_repeated_line )
U c= lines (Segm (M,P,(Seg n)))
proof
let x be
object ;
TARSKI:def 3 ( not x in U or x in lines (Segm (M,P,(Seg n))) )
A18:
dom (Sgm P) = Seg (card P)
by A6, FINSEQ_3:40;
assume A19:
x in U
;
x in lines (Segm (M,P,(Seg n)))
then consider i being
Nat such that A20:
i in Seg m
and A21:
Line (
M,
i)
= x
and A22:
f . x = i
by A5;
dom f = U
by A20, FUNCT_2:def 1;
then
i in P
by A19, A22, FUNCT_1:def 3;
then
i in rng (Sgm P)
by A6, FINSEQ_1:def 13;
then consider y being
object such that A23:
y in dom (Sgm P)
and A24:
(Sgm P) . y = i
by FUNCT_1:def 3;
reconsider y =
y as
Element of
NAT by A23;
m <> 0
by A20;
then
width M = n
by Th1;
then
Line (
(Segm (M,P,(Seg n))),
y)
= x
by A21, A23, A24, A18, Th48;
hence
x in lines (Segm (M,P,(Seg n)))
by A23, A18, Th103;
verum
end;
hence
U = lines (Segm (M,P,(Seg n)))
by A8, XBOOLE_0:def 10; Segm (M,P,(Seg n)) is without_repeated_line
let x1, x2 be object ; FUNCT_1:def 4 ( not x1 in dom (Segm (M,P,(Seg n))) or not x2 in dom (Segm (M,P,(Seg n))) or not (Segm (M,P,(Seg n))) . x1 = (Segm (M,P,(Seg n))) . x2 or x1 = x2 )
assume that
A25:
x1 in dom (Segm (M,P,(Seg n)))
and
A26:
x2 in dom (Segm (M,P,(Seg n)))
and
A27:
(Segm (M,P,(Seg n))) . x1 = (Segm (M,P,(Seg n))) . x2
; x1 = x2
A28: dom (Segm (M,P,(Seg n))) =
Seg (len (Segm (M,P,(Seg n))))
by FINSEQ_1:def 3
.=
Seg (card P)
by MATRIX_0:def 2
;
then A29:
dom (Sgm P) = dom (Segm (M,P,(Seg n)))
by A6, FINSEQ_3:40;
reconsider i1 = x1, i2 = x2 as Element of NAT by A25, A26;
A30:
dom (Sgm P) = Seg (card P)
by A6, FINSEQ_3:40;
then
(Sgm P) . i1 in rng (Sgm P)
by A25, A28, FUNCT_1:def 3;
then consider y1 being object such that
A31:
y1 in dom f
and
A32:
f . y1 = (Sgm P) . i1
by A7, FUNCT_1:def 3;
A33:
ex j1 being Nat st
( j1 in Seg m & Line (M,j1) = y1 & f . y1 = j1 )
by A5, A31;
then
m <> 0
;
then A34:
width M = n
by Th1;
(Sgm P) . i2 in rng (Sgm P)
by A26, A28, A30, FUNCT_1:def 3;
then consider y2 being object such that
A35:
y2 in dom f
and
A36:
f . y2 = (Sgm P) . i2
by A7, FUNCT_1:def 3;
ex j2 being Nat st
( j2 in Seg m & Line (M,j2) = y2 & f . y2 = j2 )
by A5, A35;
then A37:
Line ((Segm (M,P,(Seg n))),i2) = y2
by A26, A28, A36, A34, Th48;
A38:
Sgm P is one-to-one
by A6, FINSEQ_3:92;
A39:
Line ((Segm (M,P,(Seg n))),i1) = (Segm (M,P,(Seg n))) . i1
by A25, A28, MATRIX_0:52;
Line ((Segm (M,P,(Seg n))),i1) = y1
by A25, A28, A32, A33, A34, Th48;
then
(Sgm P) . i1 = (Sgm P) . i2
by A26, A27, A28, A32, A36, A37, A39, MATRIX_0:52;
hence
x1 = x2
by A25, A26, A29, A38; verum