let k be Element of NAT ; :: thesis: for X being non empty set st k = 1 & k + 1 c= card X holds
for F being IncProjMap of G_ k,X, G_ k,X st F is automorphism holds
ex s being Permutation of X st IncProjMap(# the point-map of F,the line-map of F #) = incprojmap k,s
let X be non empty set ; :: thesis: ( k = 1 & k + 1 c= card X implies for F being IncProjMap of G_ k,X, G_ k,X st F is automorphism holds
ex s being Permutation of X st IncProjMap(# the point-map of F,the line-map of F #) = incprojmap k,s )
assume A1:
( k = 1 & k + 1 c= card X )
; :: thesis: for F being IncProjMap of G_ k,X, G_ k,X st F is automorphism holds
ex s being Permutation of X st IncProjMap(# the point-map of F,the line-map of F #) = incprojmap k,s
A2:
the Points of (G_ k,X) = { A where A is Subset of X : card A = 1 }
by A1, Def1;
A3:
the Lines of (G_ k,X) = { L where L is Subset of X : card L = 1 + 1 }
by A1, Def1;
let F be IncProjMap of G_ k,X, G_ k,X; :: thesis: ( F is automorphism implies ex s being Permutation of X st IncProjMap(# the point-map of F,the line-map of F #) = incprojmap k,s )
assume A4:
F is automorphism
; :: thesis: ex s being Permutation of X st IncProjMap(# the point-map of F,the line-map of F #) = incprojmap k,s
deffunc H1( set ) -> set = {$1};
consider c being Function such that
A5:
dom c = X
and
A6:
for x being set st x in X holds
c . x = H1(x)
from FUNCT_1:sch 3();
rng c c= the Points of (G_ k,X)
then reconsider c = c as Function of X,the Points of (G_ k,X) by A5, FUNCT_2:4;
deffunc H2( Element of X) -> set = union (F . (c . $1));
consider f being Function such that
A8:
dom f = X
and
A9:
for x being Element of X holds f . x = H2(x)
from FUNCT_1:sch 4();
rng f c= X
proof
let b be
set ;
:: according to TARSKI:def 3 :: thesis: ( not b in rng f or b in X )
assume
b in rng f
;
:: thesis: b in X
then consider a being
set such that A10:
(
a in X &
b = f . a )
by A8, FUNCT_1:def 5;
reconsider a =
a as
Element of
X by A10;
A11:
b = union (F . (c . a))
by A9, A10;
consider A being
POINT of
(G_ k,X) such that A12:
A = F . (c . a)
;
A in the
Points of
(G_ k,X)
;
then consider A1 being
Subset of
X such that A13:
(
A1 = A &
card A1 = 1 )
by A2;
consider x being
set such that A14:
A = {x}
by A13, CARD_2:60;
x in X
by A13, A14, ZFMISC_1:37;
hence
b in X
by A11, A12, A14, ZFMISC_1:31;
:: thesis: verum
end;
then reconsider f = f as Function of X,X by A8, FUNCT_2:4;
A15:
( the point-map of F is bijective & dom the point-map of F = the Points of (G_ k,X) & dom the line-map of F = the Lines of (G_ k,X) & 0 < k & F is incidence_preserving )
by A1, A4, Def9, FUNCT_2:67;
then
( the point-map of F is one-to-one & the point-map of F is onto )
;
then A17:
( rng the point-map of F = the Points of (G_ k,X) & card 2 = 2 & card 1 = 1 )
by CARD_1:def 5, FUNCT_2:def 3;
f is bijective
proof
thus
f is
one-to-one
:: according to FUNCT_2:def 4 :: thesis: f is onto proof
let x1,
x2 be
set ;
:: according to FUNCT_1:def 8 :: thesis: ( not x1 in dom f or not x2 in dom f or not f . x1 = f . x2 or x1 = x2 )
assume A18:
(
x1 in dom f &
x2 in dom f &
f . x1 = f . x2 )
;
:: thesis: x1 = x2
reconsider x1 =
x1,
x2 =
x2 as
Element of
X by A18;
A19:
(
f . x1 = union (F . (c . x1)) &
f . x2 = union (F . (c . x2)) )
by A9;
consider A1 being
POINT of
(G_ k,X) such that A20:
A1 = F . (c . x1)
;
consider A2 being
POINT of
(G_ k,X) such that A21:
A2 = F . (c . x2)
;
A1 in the
Points of
(G_ k,X)
;
then consider A11 being
Subset of
X such that A22:
(
A11 = A1 &
card A11 = 1 )
by A2;
consider y1 being
set such that A23:
A1 = {y1}
by A22, CARD_2:60;
A2 in the
Points of
(G_ k,X)
;
then consider A12 being
Subset of
X such that A24:
(
A12 = A2 &
card A12 = 1 )
by A2;
consider y2 being
set such that A25:
A2 = {y2}
by A24, CARD_2:60;
(
f . x1 = y1 &
f . x2 = y2 )
by A19, A20, A21, A23, A25, ZFMISC_1:31;
then
(
c . x1 = c . x2 &
c . x1 = {x1} &
c . x2 = {x2} )
by A6, A15, A18, A20, A21, A23, A25, FUNCT_1:def 8;
hence
x1 = x2
by ZFMISC_1:6;
:: thesis: verum
end;
thus
f is
onto
:: thesis: verum
end;
then reconsider f = f as Permutation of X ;
IncProjMap(# the point-map of F,the line-map of F #) = incprojmap k,f
proof
A29:
the
point-map of
F = the
point-map of
(incprojmap k,f)
proof
A30:
dom the
point-map of
(incprojmap k,f) = the
Points of
(G_ k,X)
by FUNCT_2:67;
for
x being
set st
x in dom the
point-map of
F holds
the
point-map of
F . x = the
point-map of
(incprojmap k,f) . x
proof
let x be
set ;
:: thesis: ( x in dom the point-map of F implies the point-map of F . x = the point-map of (incprojmap k,f) . x )
assume A31:
x in dom the
point-map of
F
;
:: thesis: the point-map of F . x = the point-map of (incprojmap k,f) . x
then consider A being
POINT of
(G_ k,X) such that A32:
x = A
;
consider A1 being
Subset of
X such that A33:
(
x = A1 &
card A1 = 1 )
by A2, A15, A31;
consider x1 being
set such that A34:
x = {x1}
by A33, CARD_2:60;
A35:
(
(incprojmap k,f) . A = f .: A &
x1 in X )
by A1, A33, A34, Def14, ZFMISC_1:37;
reconsider x1 =
x1 as
Element of
X by A33, A34, ZFMISC_1:37;
A36:
F . (c . x1) = F . A
by A6, A32, A34;
Im f,
x1 = {(f . x1)}
by A8, FUNCT_1:117;
then A37:
(
f .: {x1} = {(f . x1)} &
f . x1 = union (F . A) )
by A9, A36;
F . A in the
Points of
(G_ k,X)
;
then consider B being
Subset of
X such that A38:
(
B = F . A &
card B = 1 )
by A2;
consider x2 being
set such that A39:
B = {x2}
by A38, CARD_2:60;
thus
the
point-map of
F . x = the
point-map of
(incprojmap k,f) . x
by A32, A34, A35, A37, A38, A39, ZFMISC_1:31;
:: thesis: verum
end;
hence
the
point-map of
F = the
point-map of
(incprojmap k,f)
by A15, A30, FUNCT_1:9;
:: thesis: verum
end;
the
line-map of
F = the
line-map of
(incprojmap k,f)
proof
A40:
dom the
line-map of
(incprojmap k,f) = the
Lines of
(G_ k,X)
by FUNCT_2:67;
for
x being
set st
x in dom the
line-map of
F holds
the
line-map of
F . x = the
line-map of
(incprojmap k,f) . x
proof
let x be
set ;
:: thesis: ( x in dom the line-map of F implies the line-map of F . x = the line-map of (incprojmap k,f) . x )
assume A41:
x in dom the
line-map of
F
;
:: thesis: the line-map of F . x = the line-map of (incprojmap k,f) . x
then consider A being
LINE of
(G_ k,X) such that A42:
x = A
;
consider A11 being
Subset of
X such that A43:
(
x = A11 &
card A11 = 2 )
by A3, A15, A41;
A11 is
finite
by A43;
then consider x1,
x2 being
set such that A44:
(
x1 <> x2 &
x = {x1,x2} )
by A43, CARD_2:79;
A45:
(
(incprojmap k,f) . A = f .: A &
x1 in X &
x2 in X )
by A1, A43, A44, Def14, ZFMISC_1:38;
reconsider x1 =
x1,
x2 =
x2 as
Element of
X by A43, A44, ZFMISC_1:38;
A46:
(
c . x1 = {x1} &
c . x2 = {x2} &
card {x1} = 1 &
card {x2} = 1 &
{x1} c= X &
{x2} c= X )
by A6, CARD_1:50;
then consider A1 being
POINT of
(G_ k,X) such that A47:
A1 = {x1}
;
consider A2 being
POINT of
(G_ k,X) such that A48:
A2 = {x2}
by A46;
(
A1 c= A &
A2 c= A &
F . (c . x1) = F . A1 &
F . (c . x2) = F . A2 )
by A6, A42, A44, A47, A48, ZFMISC_1:42;
then A49:
(
f .: (A1 \/ A2) = (f .: A1) \/ (f .: A2) &
A1 on A &
A2 on A &
A1 <> A2 &
A1 \/ A2 = A &
f . x1 = union (F . A1) &
f . x2 = union (F . A2) )
by A1, A9, A42, A44, A47, A48, Th10, ENUMSET1:41, RELAT_1:153, ZFMISC_1:24;
A50:
(
Im f,
x1 = {(f . x1)} &
Im f,
x2 = {(f . x2)} )
by A8, FUNCT_1:117;
then A51:
(
f .: A1 = {(f . x1)} &
f .: A2 = {(f . x2)} &
F . A1 on F . A &
F . A2 on F . A &
(incprojmap k,f) . A1 = f .: A1 &
(incprojmap k,f) . A2 = f .: A2 &
F . A1 <> F . A2 )
by A1, A15, A47, A48, A49, Def8, Def14, FUNCT_1:def 8;
then A52:
(
F . A1 c= F . A &
F . A2 c= F . A )
by A1, Th10;
A53:
(
F . A1 in the
Points of
(G_ k,X) &
F . A2 in the
Points of
(G_ k,X) )
;
then consider B1 being
Subset of
X such that A54:
(
B1 = F . A1 &
card B1 = 1 )
by A2;
consider B2 being
Subset of
X such that A55:
(
B2 = F . A2 &
card B2 = 1 )
by A2, A53;
F . A in the
Lines of
(G_ k,X)
;
then consider B3 being
Subset of
X such that A56:
(
B3 = F . A &
card B3 = 2 )
by A3;
A57:
(
F . A1 is
finite &
F . A2 is
finite &
F . A is
finite )
by A54, A55, A56;
consider y1 being
set such that A58:
F . A1 = {y1}
by A54, CARD_2:60;
consider y2 being
set such that A59:
F . A2 = {y2}
by A55, CARD_2:60;
not
y2 in F . A1
then
(
card ((F . A1) \/ (F . A2)) = 1
+ 1 &
(F . A1) \/ (F . A2) is
finite &
f .: A1 = F . A1 &
f .: A2 = F . A2 )
by A47, A48, A49, A50, A54, A58, A59, CARD_2:54, ZFMISC_1:31;
hence
the
line-map of
F . x = the
line-map of
(incprojmap k,f) . x
by A42, A45, A49, A52, A56, A57, CARD_FIN:1, XBOOLE_1:8;
:: thesis: verum
end;
hence
the
line-map of
F = the
line-map of
(incprojmap k,f)
by A15, A40, FUNCT_1:9;
:: thesis: verum
end;
hence
IncProjMap(# the
point-map of
F,the
line-map of
F #)
= incprojmap k,
f
by A29;
:: thesis: verum
end;
hence
ex s being Permutation of X st IncProjMap(# the point-map of F,the line-map of F #) = incprojmap k,s
; :: thesis: verum