let I be non empty set ; for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is strongly_connected ) holds
for B being Segre-Coset of A
for f being Collineation of (Segre_Product A) holds f .: B is Segre-Coset of A
let A be PLS-yielding ManySortedSet of I; ( ( for i being Element of I holds A . i is strongly_connected ) implies for B being Segre-Coset of A
for f being Collineation of (Segre_Product A) holds f .: B is Segre-Coset of A )
assume A1:
for i being Element of I holds A . i is strongly_connected
; for B being Segre-Coset of A
for f being Collineation of (Segre_Product A) holds f .: B is Segre-Coset of A
let B be Segre-Coset of A; for f being Collineation of (Segre_Product A) holds f .: B is Segre-Coset of A
consider W being Subset of (Segre_Product A) such that
A2:
( not W is trivial & W is strong & W is closed_under_lines )
and
A3:
B = union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) }
by A1, Th23;
let f be Collineation of (Segre_Product A); f .: B is Segre-Coset of A
reconsider g = f " as Collineation of (Segre_Product A) by Th13;
A4:
dom f = the carrier of (Segre_Product A)
by FUNCT_2:def 1;
A5:
dom g = the carrier of (Segre_Product A)
by FUNCT_2:def 1;
A6:
f is bijective
by Def4;
then A7:
rng f = the carrier of (Segre_Product A)
by FUNCT_2:def 3;
A8:
rng f = [#] (Segre_Product A)
by A6, FUNCT_2:def 3;
A9:
f .: B = union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & f .: W,Y are_joinable ) }
proof
A10:
W c= f " (f .: W)
by A4, FUNCT_1:76;
f " (f .: W) c= W
by A6, FUNCT_1:82;
then A11:
f " (f .: W) = W
by A10;
thus
f .: B c= union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & f .: W,Y are_joinable ) }
XBOOLE_0:def 10 union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & f .: W,Y are_joinable ) } c= f .: Bproof
let o be
object ;
TARSKI:def 3 ( not o in f .: B or o in union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & f .: W,Y are_joinable ) } )
assume
o in f .: B
;
o in union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & f .: W,Y are_joinable ) }
then consider u being
object such that A12:
u in dom f
and A13:
u in B
and A14:
o = f . u
by FUNCT_1:def 6;
consider y being
set such that A15:
u in y
and A16:
y in { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) }
by A3, A13, TARSKI:def 4;
consider Y being
Subset of
(Segre_Product A) such that A17:
y = Y
and A18:
( not
Y is
trivial &
Y is
strong &
Y is
closed_under_lines )
and A19:
W,
Y are_joinable
by A16;
A20:
f .: W,
f .: Y are_joinable
by A2, A18, A19, Th20;
( not
f .: Y is
trivial &
f .: Y is
strong &
f .: Y is
closed_under_lines )
by A18, Th14, Th16, Th18;
then A21:
f .: Y in { Z where Z is Subset of (Segre_Product A) : ( not Z is trivial & Z is strong & Z is closed_under_lines & f .: W,Z are_joinable ) }
by A20;
o in f .: Y
by A12, A14, A15, A17, FUNCT_1:def 6;
hence
o in union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & f .: W,Y are_joinable ) }
by A21, TARSKI:def 4;
verum
end;
let o be
object ;
TARSKI:def 3 ( not o in union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & f .: W,Y are_joinable ) } or o in f .: B )
assume
o in union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & f .: W,Y are_joinable ) }
;
o in f .: B
then consider u being
set such that A22:
o in u
and A23:
u in { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & f .: W,Y are_joinable ) }
by TARSKI:def 4;
consider Y being
Subset of
(Segre_Product A) such that A24:
u = Y
and A25:
( not
Y is
trivial &
Y is
strong &
Y is
closed_under_lines )
and A26:
f .: W,
Y are_joinable
by A23;
A27:
( not
g .: Y is
trivial &
g .: Y is
strong &
g .: Y is
closed_under_lines )
by A25, Th14, Th16, Th18;
( not
f .: W is
trivial &
f .: W is
strong &
f .: W is
closed_under_lines )
by A2, Th14, Th16, Th18;
then
g .: (f .: W),
g .: Y are_joinable
by A25, A26, Th20;
then
W,
g .: Y are_joinable
by A6, A8, A11, TOPS_2:55;
then A28:
g .: Y in { Z where Z is Subset of (Segre_Product A) : ( not Z is trivial & Z is strong & Z is closed_under_lines & W,Z are_joinable ) }
by A27;
g . o in g .: Y
by A5, A22, A24, FUNCT_1:def 6;
then A29:
g . o in B
by A3, A28, TARSKI:def 4;
o = f . ((f ") . o)
by A6, A7, A22, A24, FUNCT_1:35;
then
o = f . (g . o)
by A6, TOPS_2:def 4;
hence
o in f .: B
by A4, A29, FUNCT_1:def 6;
verum
end;
( not f .: W is trivial & f .: W is strong & f .: W is closed_under_lines )
by A2, Th14, Th16, Th18;
hence
f .: B is Segre-Coset of A
by A1, A9, Th23; verum