let I be non empty set ; for A being PLS-yielding ManySortedSet of I
for B1, B2 being Segre-Coset of A st B1 '||' B2 holds
for f being Collineation of (Segre_Product A)
for C1, C2 being Segre-Coset of A st C1 = f .: B1 & C2 = f .: B2 holds
C1 '||' C2
let A be PLS-yielding ManySortedSet of I; for B1, B2 being Segre-Coset of A st B1 '||' B2 holds
for f being Collineation of (Segre_Product A)
for C1, C2 being Segre-Coset of A st C1 = f .: B1 & C2 = f .: B2 holds
C1 '||' C2
let B1, B2 be Segre-Coset of A; ( B1 '||' B2 implies for f being Collineation of (Segre_Product A)
for C1, C2 being Segre-Coset of A st C1 = f .: B1 & C2 = f .: B2 holds
C1 '||' C2 )
assume A1:
B1 '||' B2
; for f being Collineation of (Segre_Product A)
for C1, C2 being Segre-Coset of A st C1 = f .: B1 & C2 = f .: B2 holds
C1 '||' C2
let f be Collineation of (Segre_Product A); for C1, C2 being Segre-Coset of A st C1 = f .: B1 & C2 = f .: B2 holds
C1 '||' C2
let C1, C2 be Segre-Coset of A; ( C1 = f .: B1 & C2 = f .: B2 implies C1 '||' C2 )
assume that
A2:
C1 = f .: B1
and
A3:
C2 = f .: B2
; C1 '||' C2
let x be Point of (Segre_Product A); PENCIL_3:def 2 ( x in C1 implies ex y being Point of (Segre_Product A) st
( y in C2 & x,y are_collinear ) )
assume
x in C1
; ex y being Point of (Segre_Product A) st
( y in C2 & x,y are_collinear )
then consider a being object such that
A4:
a in dom f
and
A5:
a in B1
and
A6:
x = f . a
by A2, FUNCT_1:def 6;
reconsider a = a as Point of (Segre_Product A) by A4;
consider b being Point of (Segre_Product A) such that
A7:
b in B2
and
A8:
a,b are_collinear
by A1, A5;
take y = f . b; ( y in C2 & x,y are_collinear )
A9:
dom f = the carrier of (Segre_Product A)
by FUNCT_2:def 1;
hence
y in C2
by A3, A7, FUNCT_1:def 6; x,y are_collinear
per cases
( a = b or a <> b )
;
suppose
a <> b
;
x,y are_collinear then consider l being
Block of
(Segre_Product A) such that A10:
{a,b} c= l
by A8, PENCIL_1:def 1;
reconsider k =
f .: l as
Block of
(Segre_Product A) ;
b in l
by A10, ZFMISC_1:32;
then A11:
y in k
by A9, FUNCT_1:def 6;
a in l
by A10, ZFMISC_1:32;
then
x in k
by A4, A6, FUNCT_1:def 6;
then
{x,y} c= k
by A11, ZFMISC_1:32;
hence
x,
y are_collinear
by PENCIL_1:def 1;
verum end;