let I be non empty set ; :: thesis: for A being PLS-yielding ManySortedSet of st ( for i being Element of I holds A . i is strongly_connected ) holds
for W being Subset of (Segre_Product A) st not W is trivial & W is strong & W is closed_under_lines holds
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 ) } is Segre-Coset of A
let A be PLS-yielding ManySortedSet of ; :: thesis: ( ( for i being Element of I holds A . i is strongly_connected ) implies for W being Subset of (Segre_Product A) st not W is trivial & W is strong & W is closed_under_lines holds
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 ) } is Segre-Coset of A )
assume A1:
for i being Element of I holds A . i is strongly_connected
; :: thesis: for W being Subset of (Segre_Product A) st not W is trivial & W is strong & W is closed_under_lines holds
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 ) } is Segre-Coset of A
let W be Subset of (Segre_Product A); :: thesis: ( not W is trivial & W is strong & W is closed_under_lines implies 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 ) } is Segre-Coset of A )
assume A2:
( not W is trivial & W is strong & W is closed_under_lines )
; :: thesis: 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 ) } is Segre-Coset of A
set 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 ) } ;
consider K being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A3:
( W = product K & ( for S being Subset of (A . (indx K)) st S = K . (indx K) holds
( S is strong & S is closed_under_lines ) ) )
by A2, PENCIL_1:29;
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 ) } c= the carrier of (Segre_Product A)
then reconsider C = 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 ) } as Subset of (Segre_Product A) ;
set O = [#] (A . (indx K));
dom A = I
by PARTFUN1:def 4;
then
A . (indx K) in rng A
by FUNCT_1:12;
then
not A . (indx K) is trivial
by PENCIL_1:def 17;
then A6:
not the carrier of (A . (indx K)) is trivial
;
then reconsider L = K +* (indx K),([#] (A . (indx K))) as non trivial-yielding Segre-like ManySortedSubset of Carrier A by Th7, PENCIL_1:27;
A7:
C = product L
proof
thus
C c= product L
:: according to XBOOLE_0:def 10 :: thesis: product L c= Cproof
let c be
set ;
:: according to TARSKI:def 3 :: thesis: ( not c in C or c in product L )
assume
c in C
;
:: thesis: c in product L
then consider y being
set such that A8:
(
c in y &
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 TARSKI:def 4;
consider Y being
Subset of
(Segre_Product A) such that A9:
(
y = Y & not
Y is
trivial &
Y is
strong &
Y is
closed_under_lines &
W,
Y are_joinable )
by A8;
consider M being non
trivial-yielding Segre-like ManySortedSubset of
Carrier A such that A10:
(
Y = product M & ( for
S being
Subset of
(A . (indx M)) st
S = M . (indx M) holds
(
S is
strong &
S is
closed_under_lines ) ) )
by A9, PENCIL_1:29;
reconsider c1 =
c as
ManySortedSet of
by A8, A9, PENCIL_1:14;
A11:
dom c1 =
I
by PARTFUN1:def 4
.=
dom L
by PARTFUN1:def 4
;
A12:
dom M =
I
by PARTFUN1:def 4
.=
dom L
by PARTFUN1:def 4
;
A13:
dom K =
I
by PARTFUN1:def 4
.=
dom L
by PARTFUN1:def 4
;
for
a being
set st
a in dom L holds
c1 . a in L . a
proof
let a be
set ;
:: thesis: ( a in dom L implies c1 . a in L . a )
assume A14:
a in dom L
;
:: thesis: c1 . a in L . a
then reconsider a1 =
a as
Element of
I by PARTFUN1:def 4;
per cases
( a = indx K or a <> indx K )
;
suppose A17:
a <> indx K
;
:: thesis: c1 . a in L . a
c1 . a in M . a
by A8, A9, A10, A12, A14, CARD_3:18;
then
c1 . a in K . a
by A2, A3, A9, A10, A17, Th11;
hence
c1 . a in L . a
by A17, FUNCT_7:34;
:: thesis: verum end;
end;
hence
c in product L
by A11, CARD_3:18;
:: thesis: verum
end;
thus
product L c= C
:: thesis: verumproof
let y be
set ;
:: according to TARSKI:def 3 :: thesis: ( not y in product L or y in C )
assume
y in product L
;
:: thesis: y in C
then consider z being
Function such that A18:
(
z = y &
dom z = dom L & ( for
a being
set st
a in dom L holds
z . a in L . a ) )
by CARD_3:def 5;
A19:
(
dom L = I &
dom K = I )
by PARTFUN1:def 4;
then reconsider z =
z as
ManySortedSet of
by A18, PARTFUN1:def 4, RELAT_1:def 18;
z . (indx K) in L . (indx K)
by A18, A19;
then reconsider zi =
z . (indx K) as
Point of
(A . (indx K)) by A19, FUNCT_7:33;
K c= Carrier A
by PBOOLE:def 23;
then
K . (indx K) c= (Carrier A) . (indx K)
by PBOOLE:def 5;
then reconsider S =
K . (indx K) as
Subset of
(A . (indx K)) by YELLOW_6:9;
A20:
( not
S is
trivial &
S is
strong &
S is
closed_under_lines )
by A3, PENCIL_1:def 21;
A . (indx K) is
strongly_connected
by A1;
then consider f being
FinSequence of
bool the
carrier of
(A . (indx K)) such that A21:
(
S = f . 1 &
zi in f . (len f) & ( for
Z being
Subset of
(A . (indx K)) st
Z in rng f holds
(
Z is
closed_under_lines &
Z is
strong ) ) & ( for
i being
Nat st 1
<= i &
i < len f holds
2
c= card ((f . i) /\ (f . (i + 1))) ) )
by A20, PENCIL_1:def 11;
A22:
len f in dom f
by A21, FUNCT_1:def 4;
then A23:
1
in dom f
by FINSEQ_5:6, RELAT_1:60;
deffunc H1(
set )
-> set =
product (L +* (indx K),(f . $1));
consider g being
FinSequence such that A24:
(
len g = len f & ( for
k being
Nat st
k in dom g holds
g . k = H1(
k) ) )
from FINSEQ_1:sch 2();
A25:
dom g = Seg (len f)
by A24, FINSEQ_1:def 3;
rng g c= bool the
carrier of
(Segre_Product A)
then reconsider g =
g as
FinSequence of
bool the
carrier of
(Segre_Product A) by FINSEQ_1:def 4;
len f in dom g
by A22, A24, FINSEQ_3:31;
then A34:
g . (len f) in rng g
by FUNCT_1:12;
then reconsider Yb =
g . (len f) as
Subset of
(Segre_Product A) ;
A35:
len f in Seg (len f)
by A22, FINSEQ_1:def 3;
then A36:
Yb = product (L +* (indx K),(f . (len f)))
by A24, A25;
A37:
dom z = dom (L +* (indx K),(f . (len f)))
by A18, FUNCT_7:32;
then A40:
y in Yb
by A18, A36, A37, CARD_3:18;
A41:
(
dom (L +* (indx K),(f . 1)) = I &
dom (Carrier A) = I )
by PARTFUN1:def 4;
then A43:
L +* (indx K),
(f . 1) = K
by A19, A41, FUNCT_1:9;
1
in Seg (len f)
by A23, FINSEQ_1:def 3;
then A44:
W = g . 1
by A3, A24, A43, A25;
A45:
not
f . (len f) is
trivial
then reconsider ff =
f . (len f) as non
trivial set ;
L . (indx K) = [#] (A . (indx K))
by A19, FUNCT_7:33;
then
indx K = indx L
by A6, PENCIL_1:def 21;
then reconsider EL =
L +* (indx K),
ff as non
trivial-yielding Segre-like ManySortedSet of
by PENCIL_1:27;
A49:
Yb = product EL
by A24, A35, A25;
A50:
for
V being
Subset of
(Segre_Product A) st
V in rng g holds
(
V is
closed_under_lines &
V is
strong )
proof
let V be
Subset of
(Segre_Product A);
:: thesis: ( V in rng g implies ( V is closed_under_lines & V is strong ) )
assume
V in rng g
;
:: thesis: ( V is closed_under_lines & V is strong )
then consider n1 being
set such that A51:
(
n1 in dom g &
V = g . n1 )
by FUNCT_1:def 5;
reconsider n =
n1 as
Element of
NAT by A51;
A52:
n in Seg (len f)
by A24, A51, FINSEQ_1:def 3;
then A53:
g . n = product (L +* (indx K),(f . n))
by A24, A25;
A54:
n in dom f
by A52, FINSEQ_1:def 3;
not
f . n is
trivial
then reconsider fn =
f . n as non
trivial set ;
L . (indx K) = [#] (A . (indx K))
by A19, FUNCT_7:33;
then A57:
indx K = indx L
by A6, PENCIL_1:def 21;
L +* (indx K),
(f . n) c= Carrier A
then reconsider LI =
L +* (indx K),
fn as non
trivial-yielding Segre-like ManySortedSubset of
Carrier A by A57, PBOOLE:def 23, PENCIL_1:27;
reconsider LI =
LI as non
trivial-yielding Segre-like ManySortedSubset of
Carrier A ;
A61:
LI . (indx K) = fn
by A19, FUNCT_7:33;
then A62:
indx LI = indx K
by PENCIL_1:def 21;
hence
(
V is
closed_under_lines &
V is
strong )
by A51, A53, PENCIL_1:29;
:: thesis: verum
end;
then A63:
( not
Yb is
trivial &
Yb is
strong &
Yb is
closed_under_lines )
by A34, A49;
for
i being
Element of
NAT st 1
<= i &
i < len g holds
2
c= card ((g . i) /\ (g . (i + 1)))
proof
let i be
Element of
NAT ;
:: thesis: ( 1 <= i & i < len g implies 2 c= card ((g . i) /\ (g . (i + 1))) )
assume A64:
( 1
<= i &
i < len g )
;
:: thesis: 2 c= card ((g . i) /\ (g . (i + 1)))
then
i in Seg (len f)
by A24, FINSEQ_1:3;
then A65:
g . i = product (L +* (indx K),(f . i))
by A24, A25;
( 1
<= i + 1 &
i + 1
<= len g )
by A64, NAT_1:13;
then
i + 1
in Seg (len f)
by A24, FINSEQ_1:3;
then A66:
g . (i + 1) = product (L +* (indx K),(f . (i + 1)))
by A24, A25;
2
c= card ((f . i) /\ (f . (i + 1)))
by A21, A24, A64;
then consider a,
b being
set such that A67:
(
a in (f . i) /\ (f . (i + 1)) &
b in (f . i) /\ (f . (i + 1)) &
a <> b )
by PENCIL_1:2;
consider l1 being
set such that A68:
l1 in product L
by XBOOLE_0:def 1;
consider l being
Function such that A69:
(
l = l1 &
dom l = dom L & ( for
o being
set st
o in dom L holds
l . o in L . o ) )
by A68, CARD_3:def 5;
reconsider l =
l as
ManySortedSet of
by A19, A69, PARTFUN1:def 4, RELAT_1:def 18;
set l1 =
l +* (indx K),
a;
set l2 =
l +* (indx K),
b;
(l +* (indx K),a) . (indx K) = a
by A19, A69, FUNCT_7:33;
then A70:
l +* (indx K),
a <> l +* (indx K),
b
by A19, A67, A69, FUNCT_7:33;
A71:
dom (l +* (indx K),a) =
I
by PARTFUN1:def 4
.=
dom (L +* (indx K),(f . i))
by PARTFUN1:def 4
;
then A77:
l +* (indx K),
a in product (L +* (indx K),(f . i))
by A71, CARD_3:18;
A78:
dom (l +* (indx K),a) =
I
by PARTFUN1:def 4
.=
dom (L +* (indx K),(f . (i + 1)))
by PARTFUN1:def 4
;
then
l +* (indx K),
a in product (L +* (indx K),(f . (i + 1)))
by A78, CARD_3:18;
then A84:
l +* (indx K),
a in (g . i) /\ (g . (i + 1))
by A65, A66, A77, XBOOLE_0:def 4;
A85:
dom (l +* (indx K),b) =
I
by PARTFUN1:def 4
.=
dom (L +* (indx K),(f . i))
by PARTFUN1:def 4
;
then A91:
l +* (indx K),
b in product (L +* (indx K),(f . i))
by A85, CARD_3:18;
A92:
dom (l +* (indx K),b) =
I
by PARTFUN1:def 4
.=
dom (L +* (indx K),(f . (i + 1)))
by PARTFUN1:def 4
;
then
l +* (indx K),
b in product (L +* (indx K),(f . (i + 1)))
by A92, CARD_3:18;
then
l +* (indx K),
b in (g . i) /\ (g . (i + 1))
by A65, A66, A91, XBOOLE_0:def 4;
hence
2
c= card ((g . i) /\ (g . (i + 1)))
by A70, A84, PENCIL_1:2;
:: thesis: verum
end;
then
W,
Yb are_joinable
by A24, A44, A50, Def3;
then
Yb 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 A63;
hence
y in C
by A40, TARSKI:def 4;
:: thesis: verum
end;
end;
dom K = I
by PARTFUN1:def 4;
then
L . (indx K) = [#] (A . (indx K))
by FUNCT_7:33;
then A98:
indx K = indx L
by A6, PENCIL_1:def 21;
dom K = I
by PARTFUN1:def 4;
then
L . (indx L) = [#] (A . (indx L))
by A98, FUNCT_7:33;
hence
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 ) } is Segre-Coset of A
by A7, Def2; :: thesis: verum