let I be non empty finite set ; for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is strongly_connected ) holds
for f being Collineation of (Segre_Product A) ex s being Permutation of I st
for i, j being Element of I holds
( s . i = j iff for B1 being Segre-Coset of A
for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = i holds
indx b2 = j )
let A be PLS-yielding ManySortedSet of I; ( ( for i being Element of I holds A . i is strongly_connected ) implies for f being Collineation of (Segre_Product A) ex s being Permutation of I st
for i, j being Element of I holds
( s . i = j iff for B1 being Segre-Coset of A
for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = i holds
indx b2 = j ) )
assume A1:
for i being Element of I holds A . i is strongly_connected
; for f being Collineation of (Segre_Product A) ex s being Permutation of I st
for i, j being Element of I holds
( s . i = j iff for B1 being Segre-Coset of A
for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = i holds
indx b2 = j )
let f be Collineation of (Segre_Product A); ex s being Permutation of I st
for i, j being Element of I holds
( s . i = j iff for B1 being Segre-Coset of A
for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = i holds
indx b2 = j )
defpred S1[ set , set ] means for B1 being Segre-Coset of A
for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = $1 holds
indx b2 = $2;
A2:
for x, y, x9 being Element of I st S1[x,y] & S1[x9,y] holds
x = x9
proof
reconsider ff =
f " as
Collineation of
(Segre_Product A) by PENCIL_2:13;
let x,
y,
x9 be
Element of
I;
( S1[x,y] & S1[x9,y] implies x = x9 )
assume that A3:
for
B1 being
Segre-Coset of
A for
b1,
b2 being non
trivial-yielding Segre-like ManySortedSubset of
Carrier A st
B1 = product b1 &
f .: B1 = product b2 &
indx b1 = x holds
indx b2 = y
and A4:
for
B1 being
Segre-Coset of
A for
b1,
b2 being non
trivial-yielding Segre-like ManySortedSubset of
Carrier A st
B1 = product b1 &
f .: B1 = product b2 &
indx b1 = x9 holds
indx b2 = y
;
x = x9
consider b1 being non
trivial-yielding Segre-like ManySortedSubset of
Carrier A such that A5:
indx b1 = x
and A6:
product b1 is
Segre-Coset of
A
by Th8;
reconsider B1 =
product b1 as
Segre-Coset of
A by A6;
reconsider fB1 =
f .: B1 as
Segre-Coset of
A by A1, PENCIL_2:24;
consider L1 being non
trivial-yielding Segre-like ManySortedSubset of
Carrier A such that A7:
fB1 = product L1
and
L1 . (indx L1) = [#] (A . (indx L1))
by PENCIL_2:def 2;
consider b2 being non
trivial-yielding Segre-like ManySortedSubset of
Carrier A such that A8:
indx b2 = x9
and A9:
product b2 is
Segre-Coset of
A
by Th8;
reconsider B2 =
product b2 as
Segre-Coset of
A by A9;
reconsider fB2 =
f .: B2 as
Segre-Coset of
A by A1, PENCIL_2:24;
consider L2 being non
trivial-yielding Segre-like ManySortedSubset of
Carrier A such that A10:
fB2 = product L2
and
L2 . (indx L2) = [#] (A . (indx L2))
by PENCIL_2:def 2;
A11:
indx L2 = y
by A4, A8, A10;
A12:
f is
bijective
by PENCIL_2:def 4;
A13:
ff = f "
by A12, TOPS_2:def 4;
then A14:
ff .: fB2 = f " fB2
by A12, FUNCT_1:85;
A15:
ff .: fB1 = f " fB1
by A12, A13, FUNCT_1:85;
dom f = the
carrier of
(Segre_Product A)
by FUNCT_2:def 1;
then A16:
B2 c= ff .: fB2
by A14, FUNCT_1:76;
ff .: fB2 c= B2
by A12, A14, FUNCT_1:82;
then A17:
B2 = ff .: fB2
by A16;
dom f = the
carrier of
(Segre_Product A)
by FUNCT_2:def 1;
then A18:
B1 c= ff .: fB1
by A15, FUNCT_1:76;
ff .: fB1 c= B1
by A12, A15, FUNCT_1:82;
then A19:
B1 = ff .: fB1
by A18;
indx L1 = y
by A3, A5, A7;
hence
x = x9
by A1, A5, A7, A8, A10, A11, A19, A17, Th24;
verum
end;
A20:
for y being Element of I ex x being Element of I st S1[x,y]
proof
set p0 = the
Point of
(Segre_Product A);
reconsider p0 = the
Point of
(Segre_Product A) as
Element of
Carrier A by Th6;
let x be
Element of
I;
ex x being Element of I st S1[x,x]
reconsider p =
{p0} as
ManySortedSubset of
Carrier A by PENCIL_1:11;
dom A = I
by PARTFUN1:def 2;
then
A . x in rng A
by FUNCT_1:3;
then
not
A . x is
trivial
by PENCIL_1:def 18;
then reconsider C =
[#] (A . x) as non
trivial set ;
reconsider b =
p +* (
x,
C) as non
trivial-yielding Segre-like ManySortedSubset of
Carrier A by PENCIL_1:9, PENCIL_1:10, PENCIL_2:7;
dom p = I
by PARTFUN1:def 2;
then A21:
b . x = C
by FUNCT_7:31;
then A22:
indx b = x
by PENCIL_1:def 21;
product b c= the
carrier of
(Segre_Product A)
then reconsider B =
product b as
Segre-Coset of
A by A21, A22, PENCIL_2:def 2;
reconsider fB =
f " B as
Segre-Coset of
A by A1, PENCIL_2:25;
consider b0 being non
trivial-yielding Segre-like ManySortedSubset of
Carrier A such that A31:
fB = product b0
and
b0 . (indx b0) = [#] (A . (indx b0))
by PENCIL_2:def 2;
take y =
indx b0;
S1[y,x]
let B1 be
Segre-Coset of
A;
for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = y holds
indx b2 = xlet b1,
b2 be non
trivial-yielding Segre-like ManySortedSubset of
Carrier A;
( B1 = product b1 & f .: B1 = product b2 & indx b1 = y implies indx b2 = x )
f is
bijective
by PENCIL_2:def 4;
then
rng f = the
carrier of
(Segre_Product A)
by FUNCT_2:def 3;
then A32:
f .: fB = product b
by FUNCT_1:77;
assume
(
B1 = product b1 &
f .: B1 = product b2 &
indx b1 = y )
;
indx b2 = x
hence
indx b2 = x
by A1, A22, A31, A32, Th24;
verum
end;
A33:
for x being Element of I ex y being Element of I st S1[x,y]
proof
set p0 = the
Point of
(Segre_Product A);
reconsider p0 = the
Point of
(Segre_Product A) as
Element of
Carrier A by Th6;
let x be
Element of
I;
ex y being Element of I st S1[x,y]
reconsider p =
{p0} as
ManySortedSubset of
Carrier A by PENCIL_1:11;
dom A = I
by PARTFUN1:def 2;
then
A . x in rng A
by FUNCT_1:3;
then
not
A . x is
trivial
by PENCIL_1:def 18;
then reconsider C =
[#] (A . x) as non
trivial set ;
reconsider b =
p +* (
x,
C) as non
trivial-yielding Segre-like ManySortedSubset of
Carrier A by PENCIL_1:9, PENCIL_1:10, PENCIL_2:7;
dom p = I
by PARTFUN1:def 2;
then A34:
b . x = C
by FUNCT_7:31;
then A35:
indx b = x
by PENCIL_1:def 21;
product b c= the
carrier of
(Segre_Product A)
then reconsider B =
product b as
Segre-Coset of
A by A34, A35, PENCIL_2:def 2;
reconsider fB =
f .: B as
Segre-Coset of
A by A1, PENCIL_2:24;
consider b0 being non
trivial-yielding Segre-like ManySortedSubset of
Carrier A such that A44:
fB = product b0
and
b0 . (indx b0) = [#] (A . (indx b0))
by PENCIL_2:def 2;
take
indx b0
;
S1[x, indx b0]
let B1 be
Segre-Coset of
A;
for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = x holds
indx b2 = indx b0let b1,
b2 be non
trivial-yielding Segre-like ManySortedSubset of
Carrier A;
( B1 = product b1 & f .: B1 = product b2 & indx b1 = x implies indx b2 = indx b0 )
assume
(
B1 = product b1 &
f .: B1 = product b2 &
indx b1 = x )
;
indx b2 = indx b0
hence
indx b2 = indx b0
by A1, A35, A44, Th24;
verum
end;
A45:
for x, y, y9 being Element of I st S1[x,y] & S1[x,y9] holds
y = y9
proof
let x,
y,
y9 be
Element of
I;
( S1[x,y] & S1[x,y9] implies y = y9 )
assume that A46:
for
B1 being
Segre-Coset of
A for
b1,
b2 being non
trivial-yielding Segre-like ManySortedSubset of
Carrier A st
B1 = product b1 &
f .: B1 = product b2 &
indx b1 = x holds
indx b2 = y
and A47:
for
B1 being
Segre-Coset of
A for
b1,
b2 being non
trivial-yielding Segre-like ManySortedSubset of
Carrier A st
B1 = product b1 &
f .: B1 = product b2 &
indx b1 = x holds
indx b2 = y9
;
y = y9
consider b1 being non
trivial-yielding Segre-like ManySortedSubset of
Carrier A such that A48:
indx b1 = x
and A49:
product b1 is
Segre-Coset of
A
by Th8;
reconsider B1 =
product b1 as
Segre-Coset of
A by A49;
reconsider fB1 =
f .: B1 as
Segre-Coset of
A by A1, PENCIL_2:24;
consider L1 being non
trivial-yielding Segre-like ManySortedSubset of
Carrier A such that A50:
fB1 = product L1
and
L1 . (indx L1) = [#] (A . (indx L1))
by PENCIL_2:def 2;
indx L1 = y
by A46, A48, A50;
hence
y = y9
by A47, A48, A50;
verum
end;
thus
ex f being Permutation of I st
for x, y being Element of I holds
( f . x = y iff S1[x,y] )
from TRANSGEO:sch 1(A33, A20, A2, A45); verum