let k be Nat; for X being non empty set st 2 <= k & k + 2 c= card X 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 ; ( 2 <= k & k + 2 c= card X 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:
2 <= k
and
A2:
k + 2 c= 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)
defpred S1[ Nat] means ( 1 <= $1 & $1 <= k implies for F being IncProjMap over G_ ($1,X), G_ ($1,X) st F is automorphism holds
ex f being Permutation of X st IncProjMap(# the point-map of F, the line-map of F #) = incprojmap ($1,f) );
A3:
for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be
Nat;
( S1[i] implies S1[i + 1] )
assume A4:
S1[
i]
;
S1[i + 1]
( 1
<= i + 1 &
i + 1
<= k implies for
F being
IncProjMap over
G_ (
(i + 1),
X),
G_ (
(i + 1),
X) st
F is
automorphism holds
ex
f being
Permutation of
X st
IncProjMap(# the
point-map of
F, the
line-map of
F #)
= incprojmap (
(i + 1),
f) )
proof
assume that
1
<= i + 1
and A5:
i + 1
<= k
;
for F being IncProjMap over G_ ((i + 1),X), G_ ((i + 1),X) st F is automorphism holds
ex f being Permutation of X st IncProjMap(# the point-map of F, the line-map of F #) = incprojmap ((i + 1),f)
let F2 be
IncProjMap over
G_ (
(i + 1),
X),
G_ (
(i + 1),
X);
( F2 is automorphism implies ex f being Permutation of X st IncProjMap(# the point-map of F2, the line-map of F2 #) = incprojmap ((i + 1),f) )
assume A6:
F2 is
automorphism
;
ex f being Permutation of X st IncProjMap(# the point-map of F2, the line-map of F2 #) = incprojmap ((i + 1),f)
(i + 1) + 2
<= k + 2
by A5, XREAL_1:7;
then A7:
Segm (i + 3) c= Segm (k + 2)
by NAT_1:39;
then A8:
i + 3
c= card X
by A2;
A9:
(
i = 0 implies ex
f being
Permutation of
X st
IncProjMap(# the
point-map of
F2, the
line-map of
F2 #)
= incprojmap (
(i + 1),
f) )
(
0 < i implies ex
f being
Permutation of
X st
IncProjMap(# the
point-map of
F2, the
line-map of
F2 #)
= incprojmap (
(i + 1),
f) )
proof
assume A11:
0 < i
;
ex f being Permutation of X st IncProjMap(# the point-map of F2, the line-map of F2 #) = incprojmap ((i + 1),f)
then consider F1 being
IncProjMap over
G_ (
i,
X),
G_ (
i,
X)
such that A12:
F1 is
automorphism
and A13:
the
line-map of
F1 = the
point-map of
F2
and
for
A being
POINT of
(G_ (i,X)) for
B being
finite set st
B = A holds
F1 . A = meet (F2 .: (^^ (B,X,(i + 1))))
by A2, A6, A7, Th31, XBOOLE_1:1;
0 + 1
< i + 1
by A11, XREAL_1:8;
then consider f being
Permutation of
X such that A14:
IncProjMap(# the
point-map of
F1, the
line-map of
F1 #)
= incprojmap (
i,
f)
by A4, A5, A12, NAT_1:13;
IncProjMap(# the
point-map of
F2, the
line-map of
F2 #)
= incprojmap (
(i + 1),
f)
by A2, A6, A7, A11, A13, A14, Th32, XBOOLE_1:1;
hence
ex
f being
Permutation of
X st
IncProjMap(# the
point-map of
F2, the
line-map of
F2 #)
= incprojmap (
(i + 1),
f)
;
verum
end;
hence
ex
f being
Permutation of
X st
IncProjMap(# the
point-map of
F2, the
line-map of
F2 #)
= incprojmap (
(i + 1),
f)
by A9;
verum
end;
hence
S1[
i + 1]
;
verum
end;
A15:
S1[ 0 ]
;
for i being Nat holds S1[i]
from NAT_1:sch 2(A15, A3);
then A16:
S1[k]
;
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)
hence
ex s being Permutation of X st IncProjMap(# the point-map of F, the line-map of F #) = incprojmap (k,s)
by A1, A16, XXREAL_0:2; verum