let k be Nat; for X being non empty set st 0 < k & k + 1 c= card X holds
for F being IncProjMap over G_ (k,X), G_ (k,X) holds
( F is automorphism iff 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 ; ( 0 < k & k + 1 c= card X implies for F being IncProjMap over G_ (k,X), G_ (k,X) holds
( F is automorphism iff ex s being Permutation of X st IncProjMap(# the point-map of F, the line-map of F #) = incprojmap (k,s) ) )
assume that
A1:
0 < k
and
A2:
k + 1 c= card X
; for F being IncProjMap over G_ (k,X), G_ (k,X) holds
( F is automorphism iff ex s being Permutation of X st IncProjMap(# the point-map of F, the line-map of F #) = incprojmap (k,s) )
let F be IncProjMap over G_ (k,X), G_ (k,X); ( F is automorphism iff ex s being Permutation of X st IncProjMap(# the point-map of F, the line-map of F #) = incprojmap (k,s) )
A3:
( 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) )
proof
A4:
(
card k = k &
succ 1
= 1
+ 1 )
;
A5:
card (k + 1) = k + 1
;
k + 1
in succ (card X)
by A2, ORDINAL1:22;
then A6:
(
k + 1
= card X or
k + 1
in card X )
by ORDINAL1:8;
A7:
card 1
= 1
;
(
0 + 1
< k + 1 &
succ (Segm k) = Segm (k + 1) )
by A1, NAT_1:38, XREAL_1:8;
then
Segm 1
in succ (Segm k)
by A7, A5, NAT_1:41;
then
( 1
= k or
Segm 1
in Segm k )
by ORDINAL1:8;
then A8:
( 1
= k or ( 1
< k &
Segm 2
c= Segm k ) )
by A7, A4, NAT_1:41, ORDINAL1:21;
assume A9:
F is
automorphism
;
ex s being Permutation of X st IncProjMap(# the point-map of F, the line-map of F #) = incprojmap (k,s)
succ (Segm (k + 1)) = Segm ((k + 1) + 1)
by NAT_1:38;
then
( 1
= k or ( 1
< k &
card X = k + 1 ) or ( 2
<= k &
k + 2
c= card X ) )
by A6, A8, NAT_1:39, ORDINAL1:21;
hence
ex
s being
Permutation of
X st
IncProjMap(# the
point-map of
F, the
line-map of
F #)
= incprojmap (
k,
s)
by A2, A9, Th24, Th25, Th33;
verum
end;
( ex s being Permutation of X st IncProjMap(# the point-map of F, the line-map of F #) = incprojmap (k,s) implies F is automorphism )
hence
( F is automorphism iff ex s being Permutation of X st IncProjMap(# the point-map of F, the line-map of F #) = incprojmap (k,s) )
by A3; verum