let I be non empty set ; for A being PLS-yielding ManySortedSet of I
for p, q being Point of (Segre_Product A) st p <> q holds
( p,q are_collinear iff for p1, q1 being ManySortedSet of I st p1 = p & q1 = q holds
ex i being Element of I st
( ( for a, b being Point of (A . i) st a = p1 . i & b = q1 . i holds
( a <> b & a,b are_collinear ) ) & ( for j being Element of I st j <> i holds
p1 . j = q1 . j ) ) )
let A be PLS-yielding ManySortedSet of I; for p, q being Point of (Segre_Product A) st p <> q holds
( p,q are_collinear iff for p1, q1 being ManySortedSet of I st p1 = p & q1 = q holds
ex i being Element of I st
( ( for a, b being Point of (A . i) st a = p1 . i & b = q1 . i holds
( a <> b & a,b are_collinear ) ) & ( for j being Element of I st j <> i holds
p1 . j = q1 . j ) ) )
let p, q be Point of (Segre_Product A); ( p <> q implies ( p,q are_collinear iff for p1, q1 being ManySortedSet of I st p1 = p & q1 = q holds
ex i being Element of I st
( ( for a, b being Point of (A . i) st a = p1 . i & b = q1 . i holds
( a <> b & a,b are_collinear ) ) & ( for j being Element of I st j <> i holds
p1 . j = q1 . j ) ) ) )
assume A1:
p <> q
; ( p,q are_collinear iff for p1, q1 being ManySortedSet of I st p1 = p & q1 = q holds
ex i being Element of I st
( ( for a, b being Point of (A . i) st a = p1 . i & b = q1 . i holds
( a <> b & a,b are_collinear ) ) & ( for j being Element of I st j <> i holds
p1 . j = q1 . j ) ) )
thus
( p,q are_collinear implies for p1, q1 being ManySortedSet of I st p1 = p & q1 = q holds
ex i being Element of I st
( ( for a, b being Point of (A . i) st a = p1 . i & b = q1 . i holds
( a <> b & a,b are_collinear ) ) & ( for j being Element of I st j <> i holds
p1 . j = q1 . j ) ) )
( ( for p1, q1 being ManySortedSet of I st p1 = p & q1 = q holds
ex i being Element of I st
( ( for a, b being Point of (A . i) st a = p1 . i & b = q1 . i holds
( a <> b & a,b are_collinear ) ) & ( for j being Element of I st j <> i holds
p1 . j = q1 . j ) ) ) implies p,q are_collinear )proof
assume
p,
q are_collinear
;
for p1, q1 being ManySortedSet of I st p1 = p & q1 = q holds
ex i being Element of I st
( ( for a, b being Point of (A . i) st a = p1 . i & b = q1 . i holds
( a <> b & a,b are_collinear ) ) & ( for j being Element of I st j <> i holds
p1 . j = q1 . j ) )
then consider l being
Block of
(Segre_Product A) such that A2:
{p,q} c= l
by A1, PENCIL_1:def 1;
let p1,
q1 be
ManySortedSet of
I;
( p1 = p & q1 = q implies ex i being Element of I st
( ( for a, b being Point of (A . i) st a = p1 . i & b = q1 . i holds
( a <> b & a,b are_collinear ) ) & ( for j being Element of I st j <> i holds
p1 . j = q1 . j ) ) )
assume that A3:
p1 = p
and A4:
q1 = q
;
ex i being Element of I st
( ( for a, b being Point of (A . i) st a = p1 . i & b = q1 . i holds
( a <> b & a,b are_collinear ) ) & ( for j being Element of I st j <> i holds
p1 . j = q1 . j ) )
A5:
q1 in l
by A2, A4, ZFMISC_1:32;
consider L being non
trivial-yielding Segre-like ManySortedSubset of
Carrier A such that A6:
l = product L
and A7:
L . (indx L) is
Block of
(A . (indx L))
by PENCIL_1:24;
take i =
indx L;
( ( for a, b being Point of (A . i) st a = p1 . i & b = q1 . i holds
( a <> b & a,b are_collinear ) ) & ( for j being Element of I st j <> i holds
p1 . j = q1 . j ) )
A8:
p1 in l
by A2, A3, ZFMISC_1:32;
thus
for
a,
b being
Point of
(A . i) st
a = p1 . i &
b = q1 . i holds
(
a <> b &
a,
b are_collinear )
for j being Element of I st j <> i holds
p1 . j = q1 . jproof
reconsider LI =
L . (indx L) as
Block of
(A . (indx L)) by A7;
let a,
b be
Point of
(A . i);
( a = p1 . i & b = q1 . i implies ( a <> b & a,b are_collinear ) )
A9:
ex
p0 being
Function st
(
p0 = p1 &
dom p0 = dom L & ( for
o being
object st
o in dom L holds
p0 . o in L . o ) )
by A6, A8, CARD_3:def 5;
A10:
ex
q0 being
Function st
(
q0 = q1 &
dom q0 = dom L & ( for
o being
object st
o in dom L holds
q0 . o in L . o ) )
by A6, A5, CARD_3:def 5;
assume A11:
(
a = p1 . i &
b = q1 . i )
;
( a <> b & a,b are_collinear )
hence
a <> b
;
a,b are_collinear
A17:
dom L = I
by PARTFUN1:def 2;
then A18:
q1 . i in LI
by A10;
p1 . i in LI
by A9, A17;
then
{a,b} c= LI
by A11, A18, ZFMISC_1:32;
hence
a,
b are_collinear
by PENCIL_1:def 1;
verum
end;
let j be
Element of
I;
( j <> i implies p1 . j = q1 . j )
assume
j <> i
;
p1 . j = q1 . j
hence
p1 . j = q1 . j
by A6, A8, A5, PENCIL_1:23;
verum
end;
reconsider p1 = p, q1 = q as Element of Carrier A by Th6;
assume
for p1, q1 being ManySortedSet of I st p1 = p & q1 = q holds
ex i being Element of I st
( ( for a, b being Point of (A . i) st a = p1 . i & b = q1 . i holds
( a <> b & a,b are_collinear ) ) & ( for j being Element of I st j <> i holds
p1 . j = q1 . j ) )
; p,q are_collinear
then consider i being Element of I such that
A19:
for a, b being Point of (A . i) st a = p1 . i & b = q1 . i holds
( a <> b & a,b are_collinear )
and
A20:
for j being Element of I st j <> i holds
p1 . j = q1 . j
;
q1 . i is Element of (Carrier A) . i
by PBOOLE:def 14;
then
q1 . i is Element of [#] (A . i)
by Th7;
then reconsider b = q1 . i as Point of (A . i) ;
p1 . i is Element of (Carrier A) . i
by PBOOLE:def 14;
then
p1 . i is Element of [#] (A . i)
by Th7;
then reconsider a = p1 . i as Point of (A . i) ;
A21:
a,b are_collinear
by A19;
per cases
( a = b or ex l being Block of (A . i) st {a,b} c= l )
by A21, PENCIL_1:def 1;
suppose
ex
l being
Block of
(A . i) st
{a,b} c= l
;
p,q are_collinear then consider l being
Block of
(A . i) such that A22:
{a,b} c= l
;
reconsider L =
product ({p1} +* (i,l)) as
Block of
(Segre_Product A) by Th16;
A23:
dom ({p1} +* (i,l)) = I
by PARTFUN1:def 2;
then A24:
dom {p1} = dom ({p1} +* (i,l))
by PARTFUN1:def 2;
A25:
for
o being
object st
o in dom ({p1} +* (i,l)) holds
q1 . o in ({p1} +* (i,l)) . o
A29:
for
o being
object st
o in dom ({p1} +* (i,l)) holds
p1 . o in ({p1} +* (i,l)) . o
dom q1 = dom ({p1} +* (i,l))
by A23, PARTFUN1:def 2;
then A32:
q in L
by A25, CARD_3:def 5;
dom p1 = dom ({p1} +* (i,l))
by A23, PARTFUN1:def 2;
then
p in L
by A29, CARD_3:def 5;
then
{p,q} c= L
by A32, ZFMISC_1:32;
hence
p,
q are_collinear
by PENCIL_1:def 1;
verum end; end;