let I be non empty finite set ; :: thesis: for A being PLS-yielding ManySortedSet of st ( for i being Element of I holds A . i is strongly_connected ) holds
for f being Collineation of (Segre_Product A)
for B1, B2 being Segre-Coset of A
for b1, b2, b3, b4 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & B2 = product b2 & f .: B1 = product b3 & f .: B2 = product b4 & indx b1 = indx b2 holds
indx b3 = indx b4
let A be PLS-yielding ManySortedSet of ; :: thesis: ( ( for i being Element of I holds A . i is strongly_connected ) implies for f being Collineation of (Segre_Product A)
for B1, B2 being Segre-Coset of A
for b1, b2, b3, b4 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & B2 = product b2 & f .: B1 = product b3 & f .: B2 = product b4 & indx b1 = indx b2 holds
indx b3 = indx b4 )
assume A1:
for i being Element of I holds A . i is strongly_connected
; :: thesis: for f being Collineation of (Segre_Product A)
for B1, B2 being Segre-Coset of A
for b1, b2, b3, b4 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & B2 = product b2 & f .: B1 = product b3 & f .: B2 = product b4 & indx b1 = indx b2 holds
indx b3 = indx b4
let f be Collineation of (Segre_Product A); :: thesis: for B1, B2 being Segre-Coset of A
for b1, b2, b3, b4 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & B2 = product b2 & f .: B1 = product b3 & f .: B2 = product b4 & indx b1 = indx b2 holds
indx b3 = indx b4
let B1, B2 be Segre-Coset of A; :: thesis: for b1, b2, b3, b4 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & B2 = product b2 & f .: B1 = product b3 & f .: B2 = product b4 & indx b1 = indx b2 holds
indx b3 = indx b4
let b1, b2, b3, b4 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; :: thesis: ( B1 = product b1 & B2 = product b2 & f .: B1 = product b3 & f .: B2 = product b4 & indx b1 = indx b2 implies indx b3 = indx b4 )
assume A3:
( B1 = product b1 & B2 = product b2 & f .: B1 = product b3 & f .: B2 = product b4 )
; :: thesis: ( not indx b1 = indx b2 or indx b3 = indx b4 )
assume A4:
indx b1 = indx b2
; :: thesis: indx b3 = indx b4
per cases
( B1 misses B2 or B1 meets B2 )
;
suppose A5:
B1 misses B2
;
:: thesis: indx b3 = indx b4then consider D being
FinSequence of
bool the
carrier of
(Segre_Product A) such that A6:
(
D . 1
= B1 &
D . (len D) = B2 & ( for
i being
Nat st
i in dom D holds
D . i is
Segre-Coset of
A ) & ( for
i being
Nat st 1
<= i &
i < len D holds
for
Di,
Di1 being
Segre-Coset of
A st
Di = D . i &
Di1 = D . (i + 1) holds
(
Di misses Di1 &
Di '||' Di1 ) ) )
by A2, A3, A4, Th23;
deffunc H1(
Nat)
-> Element of
bool the
carrier of
(Segre_Product A) =
f .: (D . $1);
consider E being
FinSequence of
bool the
carrier of
(Segre_Product A) such that A7:
(
len E = len D & ( for
j being
Nat st
j in dom E holds
E . j = H1(
j) ) )
from FINSEQ_2:sch 1();
A8:
dom E = Seg (len D)
by A7, FINSEQ_1:def 3;
1
in dom D
by A3, A6, FUNCT_1:def 4;
then
1
in Seg (len D)
by FINSEQ_1:def 3;
then A9:
E . 1
= f .: B1
by A6, A7, A8;
len E in dom D
by A3, A6, A7, FUNCT_1:def 4;
then
len E in Seg (len D)
by FINSEQ_1:def 3;
then A10:
E . (len E) = f .: B2
by A6, A7, A8;
A11:
for
i being
Nat st
i in dom E holds
E . i is
Segre-Coset of
A
A13:
for
i being
Nat st 1
<= i &
i < len E holds
for
Ei,
Ei1 being
Segre-Coset of
A st
Ei = E . i &
Ei1 = E . (i + 1) holds
(
Ei misses Ei1 &
Ei '||' Ei1 )
proof
let i be
Nat;
:: thesis: ( 1 <= i & i < len E implies for Ei, Ei1 being Segre-Coset of A st Ei = E . i & Ei1 = E . (i + 1) holds
( Ei misses Ei1 & Ei '||' Ei1 ) )
assume A14:
( 1
<= i &
i < len E )
;
:: thesis: for Ei, Ei1 being Segre-Coset of A st Ei = E . i & Ei1 = E . (i + 1) holds
( Ei misses Ei1 & Ei '||' Ei1 )
let Ei,
Ei1 be
Segre-Coset of
A;
:: thesis: ( Ei = E . i & Ei1 = E . (i + 1) implies ( Ei misses Ei1 & Ei '||' Ei1 ) )
assume A15:
(
Ei = E . i &
Ei1 = E . (i + 1) )
;
:: thesis: ( Ei misses Ei1 & Ei '||' Ei1 )
i in Seg (len D)
by A7, A14, FINSEQ_1:3;
then A16:
Ei = f .: (D . i)
by A7, A15, A8;
( 1
<= i + 1 &
i + 1
<= len E )
by A14, NAT_1:13;
then
i + 1
in Seg (len D)
by A7, FINSEQ_1:3;
then A17:
Ei1 = f .: (D . (i + 1))
by A7, A15, A8;
i in dom D
by A7, A14, FINSEQ_3:27;
then reconsider Di =
D . i as
Segre-Coset of
A by A6;
( 1
<= i + 1 &
i + 1
<= len E )
by A14, NAT_1:13;
then
i + 1
in dom D
by A7, FINSEQ_3:27;
then reconsider Di1 =
D . (i + 1) as
Segre-Coset of
A by A6;
A18:
(
Di misses Di1 &
Di '||' Di1 )
by A6, A7, A14;
f is
bijective Function of the
carrier of
(Segre_Product A),the
carrier of
(Segre_Product A)
by PENCIL_2:def 4;
hence
Ei misses Ei1
by A16, A17, A18, FUNCT_1:125;
:: thesis: Ei '||' Ei1
thus
Ei '||' Ei1
by A16, A17, A18, Th20;
:: thesis: verum
end; reconsider fB1 =
f .: B1,
fB2 =
f .: B2 as
Segre-Coset of
A by A1, PENCIL_2:24;
f is
bijective Function of the
carrier of
(Segre_Product A),the
carrier of
(Segre_Product A)
by PENCIL_2:def 4;
then
fB1 misses fB2
by A5, FUNCT_1:125;
hence
indx b3 = indx b4
by A2, A3, A9, A10, A11, A13, Th23;
:: thesis: verum end;