let S be non empty non void TopStruct ; for f being Collineation of S
for X, Y being Subset of S st not X is trivial & not Y is trivial & X,Y are_joinable holds
f .: X,f .: Y are_joinable
let f be Collineation of S; for X, Y being Subset of S st not X is trivial & not Y is trivial & X,Y are_joinable holds
f .: X,f .: Y are_joinable
let X, Y be Subset of S; ( not X is trivial & not Y is trivial & X,Y are_joinable implies f .: X,f .: Y are_joinable )
assume that
A1:
not X is trivial
and
A2:
not Y is trivial
and
A3:
X,Y are_joinable
; f .: X,f .: Y are_joinable
consider g being FinSequence of bool the carrier of S such that
A4:
X = g . 1
and
A5:
Y = g . (len g)
and
A6:
for W being Subset of S st W in rng g holds
( W is closed_under_lines & W is strong )
and
A7:
for i being Element of NAT st 1 <= i & i < len g holds
2 c= card ((g . i) /\ (g . (i + 1)))
by A3;
deffunc H1( set ) -> Element of bool the carrier of S = f .: (g . $1);
consider p being FinSequence such that
A8:
( len p = len g & ( for k being Nat st k in dom p holds
p . k = H1(k) ) )
from FINSEQ_1:sch 2();
A9:
dom g = Seg (len g)
by FINSEQ_1:def 3;
A10:
dom p = Seg (len p)
by FINSEQ_1:def 3;
rng p c= bool the carrier of S
then reconsider p = p as FinSequence of bool the carrier of S by FINSEQ_1:def 4;
take
p
; PENCIL_2:def 3 ( f .: X = p . 1 & f .: Y = p . (len p) & ( for W being Subset of S st W in rng p holds
( W is closed_under_lines & W is strong ) ) & ( for i being Element of NAT st 1 <= i & i < len p holds
2 c= card ((p . i) /\ (p . (i + 1))) ) )
1 in dom g
by A1, A4, FUNCT_1:def 2;
hence
f .: X = p . 1
by A4, A8, A10, A9; ( f .: Y = p . (len p) & ( for W being Subset of S st W in rng p holds
( W is closed_under_lines & W is strong ) ) & ( for i being Element of NAT st 1 <= i & i < len p holds
2 c= card ((p . i) /\ (p . (i + 1))) ) )
len g in dom g
by A2, A5, FUNCT_1:def 2;
hence
f .: Y = p . (len p)
by A5, A8, A10, A9; ( ( for W being Subset of S st W in rng p holds
( W is closed_under_lines & W is strong ) ) & ( for i being Element of NAT st 1 <= i & i < len p holds
2 c= card ((p . i) /\ (p . (i + 1))) ) )
thus
for W being Subset of S st W in rng p holds
( W is closed_under_lines & W is strong )
for i being Element of NAT st 1 <= i & i < len p holds
2 c= card ((p . i) /\ (p . (i + 1)))proof
let W be
Subset of
S;
( W in rng p implies ( W is closed_under_lines & W is strong ) )
assume
W in rng p
;
( W is closed_under_lines & W is strong )
then consider i being
object such that A13:
i in dom p
and A14:
W = p . i
by FUNCT_1:def 3;
reconsider i =
i as
Element of
NAT by A13;
g . i in rng g
by A8, A10, A9, A13, FUNCT_1:3;
then reconsider gi =
g . i as
Subset of
S ;
gi in rng g
by A8, A10, A9, A13, FUNCT_1:3;
then A15:
(
gi is
strong &
gi is
closed_under_lines )
by A6;
p . i = f .: gi
by A8, A13;
hence
(
W is
closed_under_lines &
W is
strong )
by A14, A15, Th16, Th18;
verum
end;
A16:
f is bijective
by Def4;
thus
for i being Element of NAT st 1 <= i & i < len p holds
2 c= card ((p . i) /\ (p . (i + 1)))
verumproof
let i be
Element of
NAT ;
( 1 <= i & i < len p implies 2 c= card ((p . i) /\ (p . (i + 1))) )
assume that A17:
1
<= i
and A18:
i < len p
;
2 c= card ((p . i) /\ (p . (i + 1)))
A19:
(g . i) /\ (g . (i + 1)) c= g . i
by XBOOLE_1:17;
i in dom g
by A8, A17, A18, FINSEQ_3:25;
then
g . i in rng g
by FUNCT_1:3;
then reconsider gg =
(g . i) /\ (g . (i + 1)) as
Subset of
S by A19, XBOOLE_1:1;
2
c= card ((g . i) /\ (g . (i + 1)))
by A7, A8, A17, A18;
then
not
gg is
trivial
by PENCIL_1:4;
then
not
f .: gg is
trivial
by Th14;
then A20:
not
(f .: (g . i)) /\ (f .: (g . (i + 1))) is
trivial
by A16, FUNCT_1:62;
A21:
i + 1
<= len p
by A18, NAT_1:13;
1
<= i + 1
by A17, NAT_1:13;
then
i + 1
in dom p
by A21, FINSEQ_3:25;
then A22:
p . (i + 1) = f .: (g . (i + 1))
by A8;
i in dom g
by A8, A17, A18, FINSEQ_3:25;
then
p . i = f .: (g . i)
by A8, A10, A9;
hence
2
c= card ((p . i) /\ (p . (i + 1)))
by A22, A20, PENCIL_1:4;
verum
end;