let k be Nat; for X being non empty set st 1 < k & card X = k + 1 holds
for F being IncProjMap over 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 ; ( 1 < k & card X = k + 1 implies for F being IncProjMap over 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 that
A1:
1 < k
and
A2:
k + 1 = card X
; for F being IncProjMap over 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)
deffunc H1( object ) -> Element of bool X = X \ {$1};
consider c being Function such that
A3:
dom c = X
and
A4:
for x being object st x in X holds
c . x = H1(x)
from FUNCT_1:sch 3();
A5:
X is finite
by A2;
A6:
the Points of (G_ (k,X)) = { A where A is Subset of X : card A = k }
by A1, A2, Def1;
A7:
rng c c= the Points of (G_ (k,X))
proof
let y be
object ;
TARSKI:def 3 ( not y in rng c or y in the Points of (G_ (k,X)) )
assume
y in rng c
;
y in the Points of (G_ (k,X))
then consider x being
object such that A8:
x in dom c
and A9:
y = c . x
by FUNCT_1:def 3;
A10:
card {x} = 1
by CARD_1:30;
{x} c= X
by A3, A8, ZFMISC_1:31;
then A11:
card (X \ {x}) = (k + 1) - 1
by A2, A5, A10, CARD_2:44;
y = X \ {x}
by A3, A4, A8, A9;
hence
y in the
Points of
(G_ (k,X))
by A6, A11;
verum
end;
let F be IncProjMap over G_ (k,X), G_ (k,X); ( 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
F is automorphism
; ex s being Permutation of X st IncProjMap(# the point-map of F, the line-map of F #) = incprojmap (k,s)
then A12:
the point-map of F is bijective
;
reconsider c = c as Function of X, the Points of (G_ (k,X)) by A3, A7, FUNCT_2:2;
deffunc H2( Element of X) -> set = union (X \ (F . (c . $1)));
consider f being Function such that
A13:
dom f = X
and
A14:
for x being Element of X holds f . x = H2(x)
from FUNCT_1:sch 4();
rng f c= X
proof
let b be
object ;
TARSKI:def 3 ( not b in rng f or b in X )
assume
b in rng f
;
b in X
then consider a being
object such that A15:
a in X
and A16:
b = f . a
by A13, FUNCT_1:def 3;
reconsider a =
a as
Element of
X by A15;
A17:
b = union (X \ (F . (c . a)))
by A14, A16;
consider A being
POINT of
(G_ (k,X)) such that A18:
A = F . (c . a)
;
A in the
Points of
(G_ (k,X))
;
then
ex
A1 being
Subset of
X st
(
A1 = A &
card A1 = k )
by A6;
then
card (X \ A) = (k + 1) - k
by A2, A5, CARD_2:44;
then consider x being
object such that A19:
X \ A = {x}
by CARD_2:42;
x in X
by A19, ZFMISC_1:31;
hence
b in X
by A17, A18, A19, ZFMISC_1:25;
verum
end;
then reconsider f = f as Function of X,X by A13, FUNCT_2:2;
A20:
dom the point-map of F = the Points of (G_ (k,X))
by FUNCT_2:52;
A21:
f is one-to-one
proof
let x1,
x2 be
object ;
FUNCT_1:def 4 ( not x1 in dom f or not x2 in dom f or not f . x1 = f . x2 or x1 = x2 )
assume that A22:
(
x1 in dom f &
x2 in dom f )
and A23:
f . x1 = f . x2
;
x1 = x2
reconsider x1 =
x1,
x2 =
x2 as
Element of
X by A22;
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)
;
A2 in the
Points of
(G_ (k,X))
;
then A26:
ex
A12 being
Subset of
X st
(
A12 = A2 &
card A12 = k )
by A6;
then
card (X \ A2) = (k + 1) - k
by A2, A5, CARD_2:44;
then consider y2 being
object such that A27:
X \ A2 = {y2}
by CARD_2:42;
A1 in the
Points of
(G_ (k,X))
;
then A28:
ex
A11 being
Subset of
X st
(
A11 = A1 &
card A11 = k )
by A6;
then
card (X \ A1) = (k + 1) - k
by A2, A5, CARD_2:44;
then consider y1 being
object such that A29:
X \ A1 = {y1}
by CARD_2:42;
f . x2 = union (X \ (F . (c . x2)))
by A14;
then A30:
f . x2 = y2
by A25, A27, ZFMISC_1:25;
f . x1 = union (X \ (F . (c . x1)))
by A14;
then
f . x1 = y1
by A24, A29, ZFMISC_1:25;
then
A1 = A2
by A23, A28, A26, A29, A27, A30, Th5;
then A31:
c . x1 = c . x2
by A12, A20, A24, A25, FUNCT_1:def 4;
(
c . x1 = X \ {x1} &
c . x2 = X \ {x2} )
by A4;
then
{x1} = {x2}
by A31, Th5;
hence
x1 = x2
by ZFMISC_1:3;
verum
end;
A32:
rng the point-map of F = the Points of (G_ (k,X))
by A12, FUNCT_2:def 3;
for y being object st y in X holds
ex x being object st
( x in X & y = f . x )
proof
let y be
object ;
( y in X implies ex x being object st
( x in X & y = f . x ) )
assume
y in X
;
ex x being object st
( x in X & y = f . x )
then A33:
{y} c= X
by ZFMISC_1:31;
card {y} = 1
by CARD_1:30;
then
card (X \ {y}) = (k + 1) - 1
by A2, A5, A33, CARD_2:44;
then
X \ {y} in rng the
point-map of
F
by A6, A32;
then consider a being
object such that A34:
a in dom the
point-map of
F
and A35:
X \ {y} = the
point-map of
F . a
by FUNCT_1:def 3;
reconsider a =
a as
set by TARSKI:1;
a in the
Points of
(G_ (k,X))
by A34;
then A36:
ex
A1 being
Subset of
X st
(
A1 = a &
card A1 = k )
by A6;
then
card (X \ a) = (k + 1) - k
by A2, A5, CARD_2:44;
then consider x being
object such that A37:
X \ a = {x}
by CARD_2:42;
reconsider x =
x as
Element of
X by A37, ZFMISC_1:31;
a /\ X = X \ {x}
by A37, XBOOLE_1:48;
then A38:
X \ {x} = a
by A36, XBOOLE_1:28;
c . x = X \ {x}
by A4;
then
X /\ {y} = X \ (F . (c . x))
by A35, A38, XBOOLE_1:48;
then
{y} = X \ (F . (c . x))
by A33, XBOOLE_1:28;
then
y = union (X \ (F . (c . x)))
by ZFMISC_1:25;
then
y = f . x
by A14;
hence
ex
x being
object st
(
x in X &
y = f . x )
;
verum
end;
then A39:
rng f = X
by FUNCT_2:10;
then
f is onto
by FUNCT_2:def 3;
then reconsider f = f as Permutation of X by A21;
A40:
dom the line-map of F = the Lines of (G_ (k,X))
by FUNCT_2:52;
A41:
for x being object 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
object ;
( x in dom the point-map of F implies the point-map of F . x = the point-map of (incprojmap (k,f)) . x )
assume A42:
x in dom the
point-map of
F
;
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 A43:
x = A
;
F . A in the
Points of
(G_ (k,X))
;
then A44:
ex
B being
Subset of
X st
(
B = F . A &
card B = k )
by A6;
then
card (X \ (F . A)) = (k + 1) - k
by A2, A5, CARD_2:44;
then A45:
ex
x2 being
object st
X \ (F . A) = {x2}
by CARD_2:42;
(
X \ (X \ (F . A)) = (F . A) /\ X &
(F . A) /\ X = F . A )
by A44, XBOOLE_1:28, XBOOLE_1:48;
then A46:
F . A = X \ {(union (X \ (F . A)))}
by A45, ZFMISC_1:25;
A47:
f .: X = X
by A39, RELSET_1:22;
A48:
ex
A1 being
Subset of
X st
(
x = A1 &
card A1 = k )
by A6, A20, A42;
then A49:
(
X \ (X \ A) = A /\ X &
A /\ X = A )
by A43, XBOOLE_1:28, XBOOLE_1:48;
card (X \ A) = (k + 1) - k
by A2, A5, A43, A48, CARD_2:44;
then consider x1 being
object such that A50:
X \ A = {x1}
by CARD_2:42;
reconsider x1 =
x1 as
Element of
X by A50, ZFMISC_1:31;
A51:
(
c . x1 = X \ {x1} &
Im (
f,
x1)
= {(f . x1)} )
by A4, A13, FUNCT_1:59;
(incprojmap (k,f)) . A = f .: A
by A1, A2, Def14;
then
(incprojmap (k,f)) . A = (f .: X) \ (f .: {x1})
by A50, A49, FUNCT_1:64;
hence
the
point-map of
F . x = the
point-map of
(incprojmap (k,f)) . x
by A14, A43, A50, A46, A49, A51, A47;
verum
end;
dom the point-map of (incprojmap (k,f)) = the Points of (G_ (k,X))
by FUNCT_2:52;
then A52:
the point-map of F = the point-map of (incprojmap (k,f))
by A20, A41;
A53:
the Lines of (G_ (k,X)) = { L where L is Subset of X : card L = k + 1 }
by A1, A2, Def1;
A54:
for x being object 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
object ;
( x in dom the line-map of F implies the line-map of F . x = the line-map of (incprojmap (k,f)) . x )
assume A55:
x in dom the
line-map of
F
;
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 A56:
x = A
;
F . A in the
Lines of
(G_ (k,X))
;
then
ex
y being
Subset of
X st
(
y = F . A &
card y = k + 1 )
by A53;
then A57:
F . A = X
by A2, A5, CARD_2:102;
ex
A11 being
Subset of
X st
(
x = A11 &
card A11 = k + 1 )
by A53, A40, A55;
then A58:
x = X
by A2, A5, CARD_2:102;
reconsider xx =
x as
set by TARSKI:1;
(incprojmap (k,f)) . A = f .: xx
by A1, A2, A56, Def14;
hence
the
line-map of
F . x = the
line-map of
(incprojmap (k,f)) . x
by A39, A56, A58, A57, RELSET_1:22;
verum
end;
dom the line-map of (incprojmap (k,f)) = the Lines of (G_ (k,X))
by FUNCT_2:52;
then
IncProjMap(# the point-map of F, the line-map of F #) = incprojmap (k,f)
by A40, A52, A54, FUNCT_1:def 11;
hence
ex s being Permutation of X st IncProjMap(# the point-map of F, the line-map of F #) = incprojmap (k,s)
; verum