let I be non empty set ; for A being PLS-yielding ManySortedSet of I
for S being Subset of (Segre_Product A) holds
( ( not S is trivial & S is strong & S is closed_under_lines ) iff ex B being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( S = product B & ( for C being Subset of (A . (indx B)) st C = B . (indx B) holds
( C is strong & C is closed_under_lines ) ) ) )
let A be PLS-yielding ManySortedSet of I; for S being Subset of (Segre_Product A) holds
( ( not S is trivial & S is strong & S is closed_under_lines ) iff ex B being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( S = product B & ( for C being Subset of (A . (indx B)) st C = B . (indx B) holds
( C is strong & C is closed_under_lines ) ) ) )
let S be Subset of (Segre_Product A); ( ( not S is trivial & S is strong & S is closed_under_lines ) iff ex B being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( S = product B & ( for C being Subset of (A . (indx B)) st C = B . (indx B) holds
( C is strong & C is closed_under_lines ) ) ) )
thus
( not S is trivial & S is strong & S is closed_under_lines implies ex B being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( S = product B & ( for C being Subset of (A . (indx B)) st C = B . (indx B) holds
( C is strong & C is closed_under_lines ) ) ) )
( ex B being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( S = product B & ( for C being Subset of (A . (indx B)) st C = B . (indx B) holds
( C is strong & C is closed_under_lines ) ) ) implies ( not S is trivial & S is strong & S is closed_under_lines ) )proof
assume A1:
( not
S is
trivial &
S is
strong &
S is
closed_under_lines )
;
ex B being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( S = product B & ( for C being Subset of (A . (indx B)) st C = B . (indx B) holds
( C is strong & C is closed_under_lines ) ) )
then
2
c= card S
by Th4;
then consider a,
b being
object such that A2:
a in S
and A3:
b in S
and A4:
a <> b
by Th2;
reconsider a =
a,
b =
b as
Point of
(Segre_Product A) by A2, A3;
a,
b are_collinear
by A1, A2, A3;
then consider C being
Block of
(Segre_Product A) such that A5:
{a,b} c= C
by A4;
consider CC being
Segre-like ManySortedSubset of
Carrier A such that A6:
C = product CC
and
ex
i being
Element of
I st
CC . i is
Block of
(A . i)
by Def22;
(
a in product CC &
b in product CC )
by A5, A6, ZFMISC_1:32;
then
2
c= card (product CC)
by A4, Th2;
then reconsider CC =
CC as non
trivial-yielding Segre-like ManySortedSubset of
Carrier A by Th13;
A7:
dom CC = I
by PARTFUN1:def 2;
reconsider a1 =
a,
b1 =
b as
ManySortedSet of
I by Th14;
A8:
dom a1 = I
by PARTFUN1:def 2;
A9:
dom b1 = I
by PARTFUN1:def 2;
A13:
for
f being
ManySortedSet of
I st
f in S holds
for
i being
Element of
I st
i <> indx CC holds
f . i in CC . i
proof
let f be
ManySortedSet of
I;
( f in S implies for i being Element of I st i <> indx CC holds
f . i in CC . i )
assume A14:
f in S
;
for i being Element of I st i <> indx CC holds
f . i in CC . i
then reconsider f1 =
f as
Point of
(Segre_Product A) ;
let i be
Element of
I;
( i <> indx CC implies f . i in CC . i )
assume A15:
i <> indx CC
;
f . i in CC . i
now f . i in CC . i
b1 in product CC
by A5, A6, ZFMISC_1:32;
then A16:
b1 . i in CC . i
by A7, CARD_3:9;
assume A17:
not
f . i in CC . i
;
contradiction
f1,
b are_collinear
by A1, A3, A14;
then consider lb being
Block of
(Segre_Product A) such that A18:
{f1,b} c= lb
by A17, A16;
consider Lb being non
trivial-yielding Segre-like ManySortedSubset of
Carrier A such that A19:
lb = product Lb
and
Lb . (indx Lb) is
Block of
(A . (indx Lb))
by Th24;
A20:
b1 in product Lb
by A18, A19, ZFMISC_1:32;
A21:
f in product Lb
by A18, A19, ZFMISC_1:32;
then
indx Lb = i
by A17, A16, A20, Th23;
then
Lb . (indx CC) is 1
-element
by A15, Th12;
then consider cb being
object such that A22:
Lb . (indx CC) = {cb}
by ZFMISC_1:131;
A23:
dom Lb = I
by PARTFUN1:def 2;
then
b1 . (indx CC) in {cb}
by A20, A22, CARD_3:9;
then A24:
b1 . (indx CC) = cb
by TARSKI:def 1;
a1 in product CC
by A5, A6, ZFMISC_1:32;
then A25:
a1 . i in CC . i
by A7, CARD_3:9;
f1,
a are_collinear
by A1, A2, A14;
then consider la being
Block of
(Segre_Product A) such that A26:
{f1,a} c= la
by A17, A25;
consider La being non
trivial-yielding Segre-like ManySortedSubset of
Carrier A such that A27:
la = product La
and
La . (indx La) is
Block of
(A . (indx La))
by Th24;
A28:
a1 in product La
by A26, A27, ZFMISC_1:32;
A29:
f in product La
by A26, A27, ZFMISC_1:32;
then
indx La = i
by A17, A25, A28, Th23;
then
La . (indx CC) is 1
-element
by A15, Th12;
then consider ca being
object such that A30:
La . (indx CC) = {ca}
by ZFMISC_1:131;
A31:
dom La = I
by PARTFUN1:def 2;
then
a1 . (indx CC) in {ca}
by A28, A30, CARD_3:9;
then A32:
ca <> cb
by A10, A24, TARSKI:def 1;
f . (indx CC) in {ca}
by A29, A30, A31, CARD_3:9;
then A33:
f . (indx CC) <> cb
by A32, TARSKI:def 1;
f . (indx CC) in {cb}
by A21, A22, A23, CARD_3:9;
hence
contradiction
by A33, TARSKI:def 1;
verum end;
hence
f . i in CC . i
;
verum
end;
(
a1 . (indx CC) in pi (
S,
(indx CC)) &
b1 . (indx CC) in pi (
S,
(indx CC)) )
by A2, A3, CARD_3:def 6;
then
2
c= card (pi (S,(indx CC)))
by A10, Th2;
then reconsider p =
pi (
S,
(indx CC)) as non
trivial set by Th4;
CC +* (
(indx CC),
p)
c= Carrier A
then reconsider B =
CC +* (
(indx CC),
p) as non
trivial-yielding Segre-like ManySortedSubset of
Carrier A by Th27, PBOOLE:def 18;
take
B
;
( S = product B & ( for C being Subset of (A . (indx B)) st C = B . (indx B) holds
( C is strong & C is closed_under_lines ) ) )
A40:
dom B = I
by PARTFUN1:def 2;
A41:
B . (indx CC) = p
by A7, FUNCT_7:31;
thus A42:
S = product B
for C being Subset of (A . (indx B)) st C = B . (indx B) holds
( C is strong & C is closed_under_lines )
let SS be
Subset of
(A . (indx B));
( SS = B . (indx B) implies ( SS is strong & SS is closed_under_lines ) )
assume A54:
SS = B . (indx B)
;
( SS is strong & SS is closed_under_lines )
thus
SS is
strong
SS is closed_under_lines proof
let q,
r be
Point of
(A . (indx B));
PENCIL_1:def 3 ( q in SS & r in SS implies q,r are_collinear )
assume that A55:
q in SS
and A56:
r in SS
;
q,r are_collinear
thus
q,
r are_collinear
verumproof
per cases
( q = r or q <> r )
;
suppose A57:
q <> r
;
q,r are_collinear reconsider R =
a1 +* (
(indx B),
r) as
Point of
(Segre_Product A) by Th25;
reconsider Q =
a1 +* (
(indx B),
q) as
Point of
(Segre_Product A) by Th25;
reconsider Q1 =
Q,
R1 =
R as
ManySortedSet of
I ;
A61:
for
i being
object st
i in dom B holds
Q1 . i in B . i
A64:
for
i being
object st
i in dom B holds
R1 . i in B . i
dom R1 =
I
by PARTFUN1:def 2
.=
dom B
by PARTFUN1:def 2
;
then A67:
R in product B
by A64, CARD_3:9;
dom Q1 =
I
by PARTFUN1:def 2
.=
dom B
by PARTFUN1:def 2
;
then
Q in product B
by A61, CARD_3:9;
then
Q,
R are_collinear
by A1, A42, A67;
then consider L being
Block of
(Segre_Product A) such that A68:
{Q,R} c= L
by A58;
dom a1 = I
by PARTFUN1:def 2;
then A69:
R1 . (indx B) = r
by FUNCT_7:31;
consider L1 being non
trivial-yielding Segre-like ManySortedSubset of
Carrier A such that A70:
L = product L1
and A71:
L1 . (indx L1) is
Block of
(A . (indx L1))
by Th24;
A72:
dom L1 = I
by PARTFUN1:def 2;
Q1 in product L1
by A68, A70, ZFMISC_1:32;
then A73:
Q1 . (indx B) in L1 . (indx B)
by A72, CARD_3:9;
A74:
dom L1 = I
by PARTFUN1:def 2;
R1 in product L1
by A68, A70, ZFMISC_1:32;
then A75:
R1 . (indx B) in L1 . (indx B)
by A74, CARD_3:9;
then
2
c= card (L1 . (indx B))
by A73, A75, Th2;
then A78:
not
L1 . (indx B) is
trivial
by Th4;
then reconsider LI =
L1 . (indx L1) as
Block of
(A . (indx B)) by A71, Def21;
dom a1 = I
by PARTFUN1:def 2;
then A79:
Q1 . (indx B) = q
by FUNCT_7:31;
indx B = indx L1
by A78, Def21;
then
{q,r} c= LI
by A73, A75, A79, A69, ZFMISC_1:32;
hence
q,
r are_collinear
;
verum end;
end;
end;
thus
SS is
closed_under_lines
verumproof
let L be
Block of
(A . (indx B));
PENCIL_1:def 2 ( 2 c= card (L /\ SS) implies L c= SS )
A80:
dom B = I
by PARTFUN1:def 2;
2
c= card L
by Def6;
then reconsider L1 =
L as non
trivial set by Th4;
L in the
topology of
(A . (indx B))
;
then A81:
L c= the
carrier of
(A . (indx B))
;
B +* (
(indx B),
L1)
c= Carrier A
then reconsider L2 =
B +* (
(indx B),
L1) as non
trivial-yielding Segre-like ManySortedSubset of
Carrier A by Th27, PBOOLE:def 18;
A86:
L2 . (indx B) = L1
by A40, FUNCT_7:31;
then
indx B = indx L2
by Def21;
then
L2 . (indx L2) is
Block of
(A . (indx L2))
by A80, FUNCT_7:31;
then reconsider L3 =
product L2 as
Block of
(Segre_Product A) by Th24;
assume
2
c= card (L /\ SS)
;
L c= SS
then consider x,
y being
object such that A87:
x in L /\ SS
and A88:
y in L /\ SS
and A89:
x <> y
by Th2;
set y1 =
a1 +* (
(indx B),
y);
A90:
dom (a1 +* ((indx B),y)) = I
by PARTFUN1:def 2;
then A93:
a1 +* (
(indx B),
y)
in S
by A40, A42, A90, CARD_3:9;
A94:
dom L2 = I
by PARTFUN1:def 2;
then
a1 +* (
(indx B),
y)
in L3
by A94, A90, CARD_3:9;
then A99:
a1 +* (
(indx B),
y)
in L3 /\ S
by A93, XBOOLE_0:def 4;
set x1 =
a1 +* (
(indx B),
x);
A100:
dom (a1 +* ((indx B),x)) = I
by PARTFUN1:def 2;
then A103:
a1 +* (
(indx B),
x)
in S
by A40, A42, A100, CARD_3:9;
A104:
(
(a1 +* ((indx B),x)) . (indx B) = x &
(a1 +* ((indx B),y)) . (indx B) = y )
by A8, FUNCT_7:31;
then
a1 +* (
(indx B),
x)
in L3
by A94, A100, CARD_3:9;
then
a1 +* (
(indx B),
x)
in L3 /\ S
by A103, XBOOLE_0:def 4;
then
2
c= card (L3 /\ S)
by A89, A104, A99, Th2;
then A109:
L3 c= S
by A1;
thus
L c= SS
verumproof
let e be
object ;
TARSKI:def 3 ( not e in L or e in SS )
consider f being
object such that A110:
f in L3
by XBOOLE_0:def 1;
A111:
ex
F being
Function st
(
F = f &
dom F = I & ( for
o being
object st
o in I holds
F . o in L2 . o ) )
by A94, A110, CARD_3:def 5;
then reconsider f =
f as
ManySortedSet of
I by PARTFUN1:def 2, RELAT_1:def 18;
assume A112:
e in L
;
e in SS
dom (f +* ((indx B),e)) = dom L2
by A94, PARTFUN1:def 2;
then
f +* (
(indx B),
e)
in L3
by A113, CARD_3:9;
then
(f +* ((indx B),e)) . (indx B) in B . (indx B)
by A40, A42, A109, CARD_3:9;
hence
e in SS
by A54, A111, FUNCT_7:31;
verum
end;
end;
end;
given B being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that A116:
S = product B
and
A117:
for C being Subset of (A . (indx B)) st C = B . (indx B) holds
( C is strong & C is closed_under_lines )
; ( not S is trivial & S is strong & S is closed_under_lines )
thus
not S is trivial
by A116; ( S is strong & S is closed_under_lines )
A118:
dom B = I
by PARTFUN1:def 2;
A119:
dom (Carrier A) = I
by PARTFUN1:def 2;
thus
S is strong
S is closed_under_lines proof
let x,
y be
Point of
(Segre_Product A);
PENCIL_1:def 3 ( x in S & y in S implies x,y are_collinear )
assume that A120:
x in S
and A121:
y in S
;
x,y are_collinear
per cases
( x = y or x <> y )
;
suppose A122:
x <> y
;
x,y are_collinear consider y1 being
Function such that A123:
y1 = y
and A124:
dom y1 = dom (Carrier A)
and A125:
for
a being
object st
a in dom (Carrier A) holds
y1 . a in (Carrier A) . a
by CARD_3:def 5;
A126:
dom (Carrier A) = I
by PARTFUN1:def 2;
then reconsider y1 =
y1 as
ManySortedSet of
I by A124, PARTFUN1:def 2, RELAT_1:def 18;
consider x1 being
Function such that A127:
x1 = x
and A128:
dom x1 = dom (Carrier A)
and A129:
for
a being
object st
a in dom (Carrier A) holds
x1 . a in (Carrier A) . a
by CARD_3:def 5;
reconsider x1 =
x1 as
ManySortedSet of
I by A128, A126, PARTFUN1:def 2, RELAT_1:def 18;
B c= Carrier A
by PBOOLE:def 18;
then
B . (indx B) c= (Carrier A) . (indx B)
;
then reconsider C =
B . (indx B) as
Subset of
(A . (indx B)) by YELLOW_6:2;
A132:
C is
strong
by A117;
y1 . (indx B) in (Carrier A) . (indx B)
by A119, A125;
then reconsider y1i =
y1 . (indx B) as
Point of
(A . (indx B)) by YELLOW_6:2;
A133:
y1i in C
by A116, A118, A121, A123, CARD_3:9;
x1 . (indx B) in (Carrier A) . (indx B)
by A119, A129;
then reconsider x1i =
x1 . (indx B) as
Point of
(A . (indx B)) by YELLOW_6:2;
x1i in C
by A116, A118, A120, A127, CARD_3:9;
then
x1i,
y1i are_collinear
by A133, A132;
then consider l being
Block of
(A . (indx B)) such that A134:
{x1i,y1i} c= l
by A130;
A135:
dom {x1} = I
by PARTFUN1:def 2;
A136:
for
a being
object st
a in dom ({x1} +* ((indx B),l)) holds
y1 . a in ({x1} +* ((indx B),l)) . a
{x1} +* (
(indx B),
l)
c= Carrier A
then A144:
{x1} +* (
(indx B),
l) is
ManySortedSubset of
Carrier A
by PBOOLE:def 18;
for
i being
Element of
I st
i <> indx B holds
({x1} +* ((indx B),l)) . i is 1
-element
then A145:
{x1} +* (
(indx B),
l) is
Segre-like
;
A146:
for
a being
object st
a in dom ({x1} +* ((indx B),l)) holds
x1 . a in ({x1} +* ((indx B),l)) . a
({x1} +* ((indx B),l)) . (indx B) is
Block of
(A . (indx B))
by A135, FUNCT_7:31;
then reconsider L =
product ({x1} +* ((indx B),l)) as
Block of
(Segre_Product A) by A145, A144, Def22;
dom y1 =
I
by PARTFUN1:def 2
.=
dom ({x1} +* ((indx B),l))
by PARTFUN1:def 2
;
then A150:
y1 in L
by A136, CARD_3:9;
dom x1 =
I
by PARTFUN1:def 2
.=
dom ({x1} +* ((indx B),l))
by PARTFUN1:def 2
;
then
x1 in L
by A146, CARD_3:9;
then
{x,y} c= L
by A127, A123, A150, ZFMISC_1:32;
hence
x,
y are_collinear
;
verum end;
end;
thus
S is closed_under_lines
verumproof
let l be
Block of
(Segre_Product A);
PENCIL_1:def 2 ( 2 c= card (l /\ S) implies l c= S )
consider L being
Segre-like ManySortedSubset of
Carrier A such that A151:
l = product L
and A152:
ex
i being
Element of
I st
L . i is
Block of
(A . i)
by Def22;
assume A153:
2
c= card (l /\ S)
;
l c= S
then consider a,
b being
object such that A154:
a in l /\ S
and A155:
b in l /\ S
and A156:
a <> b
by Th2;
card (l /\ S) c= card l
by CARD_1:11, XBOOLE_1:17;
then
2
c= card l
by A153;
then reconsider L =
L as non
trivial-yielding Segre-like ManySortedSubset of
Carrier A by A151, Th13;
reconsider a1 =
a,
b1 =
b as
ManySortedSet of
I by A154, A155, Th14;
A157:
dom L =
I
by PARTFUN1:def 2
.=
dom B
by PARTFUN1:def 2
;
A158:
indx B = indx L
by A116, A153, A151, Th26;
for
a being
object st
a in dom L holds
L . a c= B . a
proof
let a be
object ;
( a in dom L implies L . a c= B . a )
assume
a in dom L
;
L . a c= B . a
per cases
( a <> indx B or a = indx B )
;
suppose A159:
a = indx B
;
L . a c= B . a
B c= Carrier A
by PBOOLE:def 18;
then
B . (indx B) c= (Carrier A) . (indx B)
;
then reconsider C =
B . (indx B) as
Subset of
(A . (indx B)) by YELLOW_6:2;
consider j being
Element of
I such that A160:
L . j is
Block of
(A . j)
by A152;
2
c= card (L . j)
by A160, Def6;
then
not
L . j is
trivial
by Th4;
then
j = indx L
by Def21;
then reconsider Li =
L . (indx B) as
Block of
(A . (indx B)) by A158, A160;
A161:
C is
closed_under_lines
by A117;
a1 in product L
by A154, A151, XBOOLE_0:def 4;
then A162:
a1 . (indx B) in L . (indx B)
by A118, A157, CARD_3:9;
b1 in product L
by A155, A151, XBOOLE_0:def 4;
then A163:
b1 . (indx B) in L . (indx B)
by A118, A157, CARD_3:9;
A164:
b1 in product B
by A116, A155, XBOOLE_0:def 4;
then
b1 . (indx B) in B . (indx B)
by A118, CARD_3:9;
then A165:
b1 . (indx B) in Li /\ C
by A163, XBOOLE_0:def 4;
A166:
a1 in product B
by A116, A154, XBOOLE_0:def 4;
a1 . (indx B) in B . (indx B)
by A118, A166, CARD_3:9;
then
a1 . (indx B) in Li /\ C
by A162, XBOOLE_0:def 4;
then
2
c= card (Li /\ C)
by A167, A165, Th2;
hence
L . a c= B . a
by A159, A161;
verum end;
end;
hence
l c= S
by A116, A151, A157, CARD_3:27;
verum
end;