let k be Element of NAT ; :: thesis: for X being non empty set st 0 < k & k + 3 c= card X holds
for F being IncProjMap of G_ (k + 1),X, G_ (k + 1),X st F is automorphism holds
for H being IncProjMap of G_ k,X, G_ k,X st H is automorphism & the line-map of H = the point-map of F & ( for A being POINT of (G_ k,X)
for B being finite set st B = A holds
H . A = meet (F .: (^^ B,X,(k + 1))) ) holds
for f being Permutation of X st IncProjMap(# the point-map of H,the line-map of H #) = incprojmap k,f holds
IncProjMap(# the point-map of F,the line-map of F #) = incprojmap (k + 1),f
let X be non empty set ; :: thesis: ( 0 < k & k + 3 c= card X implies for F being IncProjMap of G_ (k + 1),X, G_ (k + 1),X st F is automorphism holds
for H being IncProjMap of G_ k,X, G_ k,X st H is automorphism & the line-map of H = the point-map of F & ( for A being POINT of (G_ k,X)
for B being finite set st B = A holds
H . A = meet (F .: (^^ B,X,(k + 1))) ) holds
for f being Permutation of X st IncProjMap(# the point-map of H,the line-map of H #) = incprojmap k,f holds
IncProjMap(# the point-map of F,the line-map of F #) = incprojmap (k + 1),f )
assume A1:
( 0 < k & k + 3 c= card X )
; :: thesis: for F being IncProjMap of G_ (k + 1),X, G_ (k + 1),X st F is automorphism holds
for H being IncProjMap of G_ k,X, G_ k,X st H is automorphism & the line-map of H = the point-map of F & ( for A being POINT of (G_ k,X)
for B being finite set st B = A holds
H . A = meet (F .: (^^ B,X,(k + 1))) ) holds
for f being Permutation of X st IncProjMap(# the point-map of H,the line-map of H #) = incprojmap k,f holds
IncProjMap(# the point-map of F,the line-map of F #) = incprojmap (k + 1),f
let F be IncProjMap of G_ (k + 1),X, G_ (k + 1),X; :: thesis: ( F is automorphism implies for H being IncProjMap of G_ k,X, G_ k,X st H is automorphism & the line-map of H = the point-map of F & ( for A being POINT of (G_ k,X)
for B being finite set st B = A holds
H . A = meet (F .: (^^ B,X,(k + 1))) ) holds
for f being Permutation of X st IncProjMap(# the point-map of H,the line-map of H #) = incprojmap k,f holds
IncProjMap(# the point-map of F,the line-map of F #) = incprojmap (k + 1),f )
assume A2:
F is automorphism
; :: thesis: for H being IncProjMap of G_ k,X, G_ k,X st H is automorphism & the line-map of H = the point-map of F & ( for A being POINT of (G_ k,X)
for B being finite set st B = A holds
H . A = meet (F .: (^^ B,X,(k + 1))) ) holds
for f being Permutation of X st IncProjMap(# the point-map of H,the line-map of H #) = incprojmap k,f holds
IncProjMap(# the point-map of F,the line-map of F #) = incprojmap (k + 1),f
let H be IncProjMap of G_ k,X, G_ k,X; :: thesis: ( H is automorphism & the line-map of H = the point-map of F & ( for A being POINT of (G_ k,X)
for B being finite set st B = A holds
H . A = meet (F .: (^^ B,X,(k + 1))) ) implies for f being Permutation of X st IncProjMap(# the point-map of H,the line-map of H #) = incprojmap k,f holds
IncProjMap(# the point-map of F,the line-map of F #) = incprojmap (k + 1),f )
assume A3:
( H is automorphism & the line-map of H = the point-map of F & ( for A being POINT of (G_ k,X)
for B being finite set st B = A holds
H . A = meet (F .: (^^ B,X,(k + 1))) ) )
; :: thesis: for f being Permutation of X st IncProjMap(# the point-map of H,the line-map of H #) = incprojmap k,f holds
IncProjMap(# the point-map of F,the line-map of F #) = incprojmap (k + 1),f
let f be Permutation of X; :: thesis: ( IncProjMap(# the point-map of H,the line-map of H #) = incprojmap k,f implies IncProjMap(# the point-map of F,the line-map of F #) = incprojmap (k + 1),f )
assume A4:
IncProjMap(# the point-map of H,the line-map of H #) = incprojmap k,f
; :: thesis: IncProjMap(# the point-map of F,the line-map of F #) = incprojmap (k + 1),f
( k + 2 <= k + 3 & k + 1 <= k + 2 & k + 1 <= k + 3 & k + 0 <= k + 1 )
by XREAL_1:9;
then A5:
( k + 2 c= k + 3 & k + 1 c= k + 2 & k + 1 c= k + 3 & k c= k + 1 & card k = k & card (k + 1) = k + 1 & card (k + 2) = k + 2 )
by CARD_1:def 5, NAT_1:40;
then A6:
( k + 1 c= card X & (k + 1) + 1 c= card X & 0 < k + 1 )
by A1, XBOOLE_1:1;
then A7:
the Lines of (G_ k,X) = { L where L is Subset of X : card L = k + 1 }
by A1, Def1;
A8:
the Points of (G_ (k + 1),X) = { A where A is Subset of X : card A = k + 1 }
by A6, Def1;
A9:
the Lines of (G_ (k + 1),X) = { L where L is Subset of X : card L = (k + 1) + 1 }
by A6, Def1;
A10:
( the point-map of F is bijective & F is incidence_preserving & dom the point-map of F = the Points of (G_ (k + 1),X) & dom the line-map of F = the Lines of (G_ (k + 1),X) & dom the point-map of (incprojmap (k + 1),f) = the Points of (G_ (k + 1),X) & dom the line-map of (incprojmap (k + 1),f) = the Lines of (G_ (k + 1),X) )
by A2, Def9, FUNCT_2:67;
A12:
the point-map of F = the point-map of (incprojmap (k + 1),f)
proof
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 + 1),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 + 1),f) . x )
assume
x in dom the
point-map of
F
;
:: thesis: the point-map of F . x = the point-map of (incprojmap (k + 1),f) . x
then consider A being
POINT of
(G_ (k + 1),X) such that A13:
x = A
;
consider A1 being
LINE of
(G_ k,X) such that A14:
x = A1
by A7, A8, A13;
(incprojmap k,f) . A1 = f .: A1
by A1, A6, Def14;
then
F . A = (incprojmap (k + 1),f) . A
by A3, A4, A6, A13, A14, Def14;
hence
the
point-map of
F . x = the
point-map of
(incprojmap (k + 1),f) . x
by A13;
:: thesis: verum
end;
hence
the
point-map of
F = the
point-map of
(incprojmap (k + 1),f)
by A10, FUNCT_1:9;
:: thesis: verum
end;
the line-map of F = the line-map of (incprojmap (k + 1),f)
proof
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 + 1),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 + 1),f) . x )
assume
x in dom the
line-map of
F
;
:: thesis: the line-map of F . x = the line-map of (incprojmap (k + 1),f) . x
then consider A being
LINE of
(G_ (k + 1),X) such that A15:
x = A
;
x in the
Lines of
(G_ (k + 1),X)
by A15;
then consider A11 being
Subset of
X such that A16:
(
x = A11 &
card A11 = (k + 1) + 1 )
by A9;
consider B1 being
set such that A17:
(
B1 c= x &
card B1 = k + 1 )
by A5, A16, CARD_FIL:36;
consider C1 being
set such that A18:
(
C1 c= B1 &
card C1 = k )
by A5, A17, CARD_FIL:36;
A19:
(
B1 is
finite &
C1 is
finite &
x is
finite &
x \ B1 c= x &
C1 c= x )
by A16, A17, A18, XBOOLE_1:1;
then A20:
(
card (x \ B1) = (k + 2) - (k + 1) &
C1 misses x \ B1 &
x \ B1 is
finite &
C1 \/ (x \ B1) c= x )
by A16, A17, A18, CARD_2:63, XBOOLE_1:8, XBOOLE_1:85;
then A21:
(
card (C1 \/ (x \ B1)) = k + 1 &
C1 \/ (x \ B1) c= X &
B1 c= X &
B1 \/ (C1 \/ (x \ B1)) c= x )
by A16, A17, A18, A19, CARD_2:53, XBOOLE_1:1, XBOOLE_1:8;
then A22:
(
B1 in the
Points of
(G_ (k + 1),X) &
C1 \/ (x \ B1) in the
Points of
(G_ (k + 1),X) )
by A8, A17;
then consider b1 being
POINT of
(G_ (k + 1),X) such that A23:
b1 = B1
;
consider b2 being
POINT of
(G_ (k + 1),X) such that A24:
b2 = C1 \/ (x \ B1)
by A22;
B1 misses x \ B1
by XBOOLE_1:79;
then
card ((x \ B1) /\ B1) = 0
by CARD_1:47, XBOOLE_0:def 7;
then A25:
b1 <> b2
by A20, A23, A24, XBOOLE_1:11, XBOOLE_1:28;
then
(
card (b1 \/ b2) c= k + 2 &
(k + 1) + 1
c= card (b1 \/ b2) &
b2 is
finite &
b1 on A &
b2 on A )
by A6, A15, A16, A17, A20, A21, A23, A24, Th1, Th10, CARD_1:27;
then
(
card (b1 \/ b2) = k + 2 &
b1 \/ b2 is
finite &
b1 \/ b2 c= x &
F . b1 on F . A &
F . b2 on F . A )
by A10, A17, A20, A23, A24, Def8, XBOOLE_0:def 10, XBOOLE_1:8;
then A26:
(
b1 \/ b2 = x &
(f .: b1) \/ (f .: b2) = f .: (b1 \/ b2) &
F . b1 in the
Points of
(G_ (k + 1),X) &
F . b2 in the
Points of
(G_ (k + 1),X) &
F . A in the
Lines of
(G_ (k + 1),X) &
F . b1 c= F . A &
F . b2 c= F . A )
by A6, A16, A19, Th10, CARD_FIN:1, RELAT_1:153;
then consider B11 being
Subset of
X such that A27:
(
F . b1 = B11 &
card B11 = k + 1 )
by A8;
consider B12 being
Subset of
X such that A28:
(
F . b2 = B12 &
card B12 = k + 1 )
by A8, A26;
consider L1 being
Subset of
X such that A29:
(
F . A = L1 &
card L1 = (k + 1) + 1 )
by A9, A26;
A30:
(
F . b1 <> F . b2 &
(F . b1) \/ (F . b2) c= F . A &
F . A is
finite )
by A10, A25, A26, A29, FUNCT_1:def 8, XBOOLE_1:8;
then
(
(k + 1) + 1
c= card ((F . b1) \/ (F . b2)) &
card ((F . b1) \/ (F . b2)) c= k + 2 )
by A27, A28, A29, Th1, CARD_1:27;
then
(
card ((F . b1) \/ (F . b2)) = k + 2 &
(F . b1) \/ (F . b2) is
finite )
by XBOOLE_0:def 10;
then
(
(F . b1) \/ (F . b2) = F . A &
(incprojmap (k + 1),f) . A = f .: x &
F . b2 = (incprojmap (k + 1),f) . b2 &
F . b1 = (incprojmap (k + 1),f) . b1 &
(incprojmap (k + 1),f) . b1 = f .: b1 &
(incprojmap (k + 1),f) . b2 = f .: b2 )
by A6, A12, A15, A29, A30, Def14, CARD_FIN:1;
hence
the
line-map of
F . x = the
line-map of
(incprojmap (k + 1),f) . x
by A15, A26;
:: thesis: verum
end;
hence
the
line-map of
F = the
line-map of
(incprojmap (k + 1),f)
by A10, FUNCT_1:9;
:: thesis: verum
end;
hence
IncProjMap(# the point-map of F,the line-map of F #) = incprojmap (k + 1),f
by A12; :: thesis: verum