let k be Element of NAT ; :: thesis: for X being non empty set st 1 < k & card X = k + 1 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: ( 1 < k & card X = k + 1 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:
( 1 < k & k + 1 = 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 = k }
by A1, Def1;
A3:
the Lines of (G_ k,X) = { L where L is Subset of X : card L = k + 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 ) -> Element of bool X = X \ {$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();
A8:
X is finite
by A1;
rng c c= the Points of (G_ k,X)
proof
let y be
set ;
:: according to TARSKI:def 3 :: thesis: ( not y in rng c or y in the Points of (G_ k,X) )
assume
y in rng c
;
:: thesis: y in the Points of (G_ k,X)
then consider x being
set such that A9:
(
x in dom c &
y = c . x )
by FUNCT_1:def 5;
A10:
(
y = X \ {x} &
{x} c= X &
card {x} = 1 )
by A5, A6, A9, CARD_1:50, ZFMISC_1:37;
then
(
card (X \ {x}) = (k + 1) - 1 &
X \ {x} c= X )
by A1, A8, CARD_2:63;
hence
y in the
Points of
(G_ k,X)
by A2, A10;
:: thesis: verum
end;
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 (X \ (F . (c . $1)));
consider f being Function such that
A11:
dom f = X
and
A12:
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 A13:
(
a in X &
b = f . a )
by A11, FUNCT_1:def 5;
reconsider a =
a as
Element of
X by A13;
A14:
b = union (X \ (F . (c . a)))
by A12, A13;
consider A being
POINT of
(G_ k,X) such that A15:
A = F . (c . a)
;
A in the
Points of
(G_ k,X)
;
then consider A1 being
Subset of
X such that A16:
(
A1 = A &
card A1 = k )
by A2;
card (X \ A) = (k + 1) - k
by A1, A8, A16, CARD_2:63;
then consider x being
set such that A17:
X \ A = {x}
by CARD_2:60;
x in X
by A17, ZFMISC_1:37;
hence
b in X
by A14, A15, A17, ZFMISC_1:31;
:: thesis: verum
end;
then reconsider f = f as Function of X,X by A11, FUNCT_2:4;
A18:
( 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 & k + 1 c= card X & the line-map of F is bijective )
by A1, A4, Def9, FUNCT_2:67;
then A19:
( the point-map of F is one-to-one & the point-map of F is onto & the line-map of F is onto )
;
then A20:
( rng the point-map of F = the Points of (G_ k,X) & card 2 = 2 & card 1 = 1 & rng the line-map of F = the Lines of (G_ k,X) )
by CARD_1:def 5, FUNCT_2:def 3;
A21:
f is one-to-one
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 A22:
(
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 A22;
A23:
(
f . x1 = union (X \ (F . (c . x1))) &
f . x2 = union (X \ (F . (c . x2))) )
by A12;
consider A1 being
POINT of
(G_ k,X) such that A24:
A1 = F . (c . x1)
;
consider A2 being
POINT of
(G_ k,X) such that A25:
A2 = F . (c . x2)
;
A1 in the
Points of
(G_ k,X)
;
then consider A11 being
Subset of
X such that A26:
(
A11 = A1 &
card A11 = k )
by A2;
A2 in the
Points of
(G_ k,X)
;
then consider A12 being
Subset of
X such that A27:
(
A12 = A2 &
card A12 = k )
by A2;
A28:
(
card (X \ A1) = (k + 1) - k &
card (X \ A2) = (k + 1) - k )
by A1, A8, A26, A27, CARD_2:63;
then consider y1 being
set such that A29:
X \ A1 = {y1}
by CARD_2:60;
consider y2 being
set such that A30:
X \ A2 = {y2}
by A28, CARD_2:60;
(
f . x1 = y1 &
f . x2 = y2 )
by A23, A24, A25, A29, A30, ZFMISC_1:31;
then
(
A1 = A2 &
c . x1 in dom the
point-map of
F &
c . x2 in dom the
point-map of
F )
by A18, A22, A26, A27, A29, A30, Th5;
then
(
c . x1 = c . x2 &
c . x1 = X \ {x1} &
c . x2 = X \ {x2} &
{x1} c= X &
{x2} c= X )
by A6, A19, A24, A25, FUNCT_1:def 8;
then
{x1} = {x2}
by Th5;
hence
x1 = x2
by ZFMISC_1:6;
:: thesis: verum
end;
for y being set st y in X holds
ex x being set st
( x in X & y = f . x )
proof
let y be
set ;
:: thesis: ( y in X implies ex x being set st
( x in X & y = f . x ) )
assume
y in X
;
:: thesis: ex x being set st
( x in X & y = f . x )
then A31:
(
{y} c= X &
card {y} = 1 )
by CARD_1:50, ZFMISC_1:37;
then
(
card (X \ {y}) = (k + 1) - 1 &
X \ {y} c= X )
by A1, A8, CARD_2:63;
then
X \ {y} in rng the
point-map of
F
by A2, A20;
then consider a being
set such that A32:
(
a in dom the
point-map of
F &
X \ {y} = the
point-map of
F . a )
by FUNCT_1:def 5;
a in the
Points of
(G_ k,X)
by A32;
then consider A1 being
Subset of
X such that A33:
(
A1 = a &
card A1 = k )
by A2;
card (X \ a) = (k + 1) - k
by A1, A8, A33, CARD_2:63;
then consider x being
set such that A34:
X \ a = {x}
by CARD_2:60;
reconsider x =
x as
Element of
X by A34, ZFMISC_1:37;
a /\ X = X \ {x}
by A34, XBOOLE_1:48;
then
(
c . x = X \ {x} &
X \ {x} = a )
by A6, A33, XBOOLE_1:28;
then
X /\ {y} = X \ (F . (c . x))
by A32, XBOOLE_1:48;
then
{y} = X \ (F . (c . x))
by A31, XBOOLE_1:28;
then
y = union (X \ (F . (c . x)))
by ZFMISC_1:31;
then
y = f . x
by A12;
hence
ex
x being
set st
(
x in X &
y = f . x )
;
:: thesis: verum
end;
then A35:
rng f = X
by FUNCT_2:16;
then
f is onto
by FUNCT_2:def 3;
then reconsider f = f as Permutation of X by A21;
IncProjMap(# the point-map of F,the line-map of F #) = incprojmap k,f
proof
A36:
the
point-map of
F = the
point-map of
(incprojmap k,f)
proof
A37:
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 A38:
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 A39:
x = A
;
consider A1 being
Subset of
X such that A40:
(
x = A1 &
card A1 = k )
by A2, A18, A38;
F . A in the
Points of
(G_ k,X)
;
then consider B being
Subset of
X such that A41:
(
B = F . A &
card B = k )
by A2;
A42:
(
X \ (X \ (F . A)) = (F . A) /\ X &
(F . A) /\ X = F . A &
F . A is
finite &
A is
finite )
by A39, A40, A41, XBOOLE_1:28, XBOOLE_1:48;
then A43:
(
X \ (X \ (F . A)) = F . A &
card (X \ (F . A)) = (k + 1) - k &
card (X \ A) = (k + 1) - k )
by A1, A8, A39, A40, A41, CARD_2:63;
then consider x1 being
set such that A44:
X \ A = {x1}
by CARD_2:60;
consider x2 being
set such that A45:
X \ (F . A) = {x2}
by A43, CARD_2:60;
A46:
(
F . A = X \ {(union (X \ (F . A)))} &
x1 in X )
by A42, A44, A45, ZFMISC_1:31, ZFMISC_1:37;
reconsider x1 =
x1 as
Element of
X by A44, ZFMISC_1:37;
A47:
(
X \ (X \ A) = X \ {x1} &
X \ (X \ A) = A /\ X &
A /\ X = A )
by A39, A40, A44, XBOOLE_1:28, XBOOLE_1:48;
then A48:
(
c . x1 = X \ {x1} &
A = X \ {x1} )
by A6;
(incprojmap k,f) . A = f .: A
by A1, Def14;
then A49:
(incprojmap k,f) . A = (f .: X) \ (f .: {x1})
by A47, FUNCT_1:123;
Im f,
x1 = {(f . x1)}
by A11, FUNCT_1:117;
then
(
f .: X = X &
f .: {x1} = {(f . x1)} )
by A35, FUNCT_2:45;
hence
the
point-map of
F . x = the
point-map of
(incprojmap k,f) . x
by A12, A39, A46, A48, A49;
:: thesis: verum
end;
hence
the
point-map of
F = the
point-map of
(incprojmap k,f)
by A18, A37, FUNCT_1:9;
:: thesis: verum
end;
the
line-map of
F = the
line-map of
(incprojmap k,f)
proof
A50:
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 A51:
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 A52:
x = A
;
consider A11 being
Subset of
X such that A53:
(
x = A11 &
card A11 = k + 1 )
by A3, A18, A51;
A54:
x = X
by A1, A8, A53, CARD_FIN:1;
F . A in the
Lines of
(G_ k,X)
;
then consider y being
Subset of
X such that A55:
(
y = F . A &
card y = k + 1 )
by A3;
(
F . A = X &
(incprojmap k,f) . A = f .: x )
by A1, A8, A52, A55, Def14, CARD_FIN:1;
hence
the
line-map of
F . x = the
line-map of
(incprojmap k,f) . x
by A35, A52, A54, FUNCT_2:45;
:: thesis: verum
end;
hence
the
line-map of
F = the
line-map of
(incprojmap k,f)
by A18, A50, FUNCT_1:9;
:: thesis: verum
end;
hence
IncProjMap(# the
point-map of
F,the
line-map of
F #)
= incprojmap k,
f
by A36;
:: 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