let k be Element of NAT ; :: thesis: for X being non empty set st 2 <= k & k + 2 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: ( 2 <= k & k + 2 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:
( 2 <= k & k + 2 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
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 A2:
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
defpred S1[ Element of NAT ] means ( 1 <= $1 & $1 <= k implies for F being IncProjMap of 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:
S1[ 0 ]
;
A4:
for i being Element of NAT st S1[i] holds
S1[i + 1]
proof
let i be
Element of
NAT ;
:: thesis: ( S1[i] implies S1[i + 1] )
assume A5:
S1[
i]
;
:: thesis: S1[i + 1]
( 1
<= i + 1 &
i + 1
<= k implies for
F being
IncProjMap of
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 A6:
( 1
<= i + 1 &
i + 1
<= k )
;
:: thesis: for F being IncProjMap of 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 of
G_ (i + 1),
X,
G_ (i + 1),
X;
:: thesis: ( 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 A7:
F2 is
automorphism
;
:: thesis: ex f being Permutation of X st IncProjMap(# the point-map of F2,the line-map of F2 #) = incprojmap (i + 1),f
0 c= i
by NAT_1:40;
then
(
0 in succ i &
(i + 1) + 2
<= k + 2 )
by A6, ORDINAL1:34, XREAL_1:9;
then
( (
0 = i or
0 in i ) &
card i = i &
i + 3
c= k + 2 )
by CARD_1:def 5, NAT_1:40, ORDINAL1:13;
then A8:
( (
0 = i or
0 < i ) &
i + 3
c= card X )
by A1, XBOOLE_1:1;
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
;
:: thesis: 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 of
G_ i,
X,
G_ i,
X such that A12:
(
F1 is
automorphism & the
line-map of
F1 = the
point-map of
F2 & ( 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 A7, A8, Th31;
(
0 + 1
< i + 1 &
i + 0 <= i + 1 )
by A11, XREAL_1:10;
then consider f being
Permutation of
X such that A13:
IncProjMap(# the
point-map of
F1,the
line-map of
F1 #)
= incprojmap i,
f
by A5, A6, A12, NAT_1:13;
IncProjMap(# the
point-map of
F2,the
line-map of
F2 #)
= incprojmap (i + 1),
f
by A7, A8, A11, A12, A13, Th32;
hence
ex
f being
Permutation of
X st
IncProjMap(# the
point-map of
F2,the
line-map of
F2 #)
= incprojmap (i + 1),
f
;
:: thesis: 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;
:: thesis: verum
end;
hence
S1[
i + 1]
;
:: thesis: verum
end;
for i being Element of NAT holds S1[i]
from NAT_1:sch 1(A3, A4);
then
( S1[k] & 1 <= k )
by A1, XXREAL_0:2;
hence
ex s being Permutation of X st IncProjMap(# the point-map of F,the line-map of F #) = incprojmap k,s
by A2; :: thesis: verum