let k be Nat; for X being non empty set st 0 < k & k + 3 c= card X holds
for F being IncProjMap over G_ ((k + 1),X), G_ ((k + 1),X) st F is automorphism holds
for H being IncProjMap over G_ (k,X), G_ (k,X) st the line-map of H = the point-map of F 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 ; ( 0 < k & k + 3 c= card X implies for F being IncProjMap over G_ ((k + 1),X), G_ ((k + 1),X) st F is automorphism holds
for H being IncProjMap over G_ (k,X), G_ (k,X) st the line-map of H = the point-map of F 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 that
A1:
0 < k
and
A2:
k + 3 c= card X
; for F being IncProjMap over G_ ((k + 1),X), G_ ((k + 1),X) st F is automorphism holds
for H being IncProjMap over G_ (k,X), G_ (k,X) st the line-map of H = the point-map of F 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)
k + 1 <= k + 3
by XREAL_1:7;
then
Segm (k + 1) c= Segm (k + 3)
by NAT_1:39;
then A3:
k + 1 c= card X
by A2;
then A4:
the Lines of (G_ (k,X)) = { L where L is Subset of X : card L = k + 1 }
by A1, Def1;
k + 2 <= k + 3
by XREAL_1:7;
then
Segm (k + 2) c= Segm (k + 3)
by NAT_1:39;
then A5:
(k + 1) + 1 c= card X
by A2;
then A6:
the Points of (G_ ((k + 1),X)) = { A where A is Subset of X : card A = k + 1 }
by Def1;
k + 0 <= k + 1
by XREAL_1:7;
then A7:
Segm k c= Segm (k + 1)
by NAT_1:39;
k + 1 <= k + 2
by XREAL_1:7;
then A8:
Segm (k + 1) c= Segm (k + 2)
by NAT_1:39;
let F be IncProjMap over G_ ((k + 1),X), G_ ((k + 1),X); ( F is automorphism implies for H being IncProjMap over G_ (k,X), G_ (k,X) st the line-map of H = the point-map of F 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 A9:
F is automorphism
; for H being IncProjMap over G_ (k,X), G_ (k,X) st the line-map of H = the point-map of F 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)
A10:
F is incidence_preserving
by A9;
let H be IncProjMap over G_ (k,X), G_ (k,X); ( the line-map of H = the point-map of F 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 A11:
the line-map of H = the point-map of F
; 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)
A12:
dom the point-map of F = the Points of (G_ ((k + 1),X))
by FUNCT_2:52;
let f be Permutation of X; ( 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 A13:
IncProjMap(# the point-map of H, the line-map of H #) = incprojmap (k,f)
; IncProjMap(# the point-map of F, the line-map of F #) = incprojmap ((k + 1),f)
A14:
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 + 1),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 + 1),f)) . x )
assume
x in dom the
point-map of
F
;
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 A15:
x = A
;
consider A1 being
LINE of
(G_ (k,X)) such that A16:
x = A1
by A4, A6, A15;
(incprojmap (k,f)) . A1 = f .: A1
by A1, A3, Def14;
then
F . A = (incprojmap ((k + 1),f)) . A
by A11, A13, A5, A15, A16, Def14;
hence
the
point-map of
F . x = the
point-map of
(incprojmap ((k + 1),f)) . x
by A15;
verum
end;
A17:
the Lines of (G_ ((k + 1),X)) = { L where L is Subset of X : card L = (k + 1) + 1 }
by A5, Def1;
A18:
the point-map of F is bijective
by A9;
A19:
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 + 1),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 + 1),f)) . x )
assume
x in dom the
line-map of
F
;
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 A20:
x = A
;
reconsider x =
x as
set by TARSKI:1;
x in the
Lines of
(G_ ((k + 1),X))
by A20;
then A21:
ex
A11 being
Subset of
X st
(
x = A11 &
card A11 = (k + 1) + 1 )
by A17;
then consider B1 being
set such that A22:
B1 c= x
and A23:
card B1 = k + 1
by A8, CARD_FIL:36;
A24:
x is
finite
by A21;
then A25:
card (x \ B1) = (k + 2) - (k + 1)
by A21, A22, A23, CARD_2:44;
B1 c= X
by A21, A22, XBOOLE_1:1;
then
B1 in the
Points of
(G_ ((k + 1),X))
by A6, A23;
then consider b1 being
POINT of
(G_ ((k + 1),X)) such that A26:
b1 = B1
;
consider C1 being
set such that A27:
C1 c= B1
and A28:
card C1 = k
by A7, A23, CARD_FIL:36;
B1 is
finite
by A23;
then A29:
card (C1 \/ (x \ B1)) = k + 1
by A27, A28, A24, A25, CARD_2:40, XBOOLE_1:85;
C1 c= x
by A22, A27;
then A30:
C1 \/ (x \ B1) c= x
by XBOOLE_1:8;
then
C1 \/ (x \ B1) c= X
by A21, XBOOLE_1:1;
then
C1 \/ (x \ B1) in the
Points of
(G_ ((k + 1),X))
by A6, A29;
then consider b2 being
POINT of
(G_ ((k + 1),X)) such that A31:
b2 = C1 \/ (x \ B1)
;
b2 on A
by A5, A20, A30, A31, Th10;
then
F . b2 on F . A
by A10;
then A32:
F . b2 c= F . A
by A5, Th10;
B1 \/ (C1 \/ (x \ B1)) c= x
by A22, A30, XBOOLE_1:8;
then A33:
card (b1 \/ b2) c= k + 2
by A21, A26, A31, CARD_1:11;
B1 misses x \ B1
by XBOOLE_1:79;
then
card ((x \ B1) /\ B1) = 0
by CARD_1:27, XBOOLE_0:def 7;
then A34:
b1 <> b2
by A25, A26, A31, XBOOLE_1:11, XBOOLE_1:28;
then
(k + 1) + 1
c= card (b1 \/ b2)
by A23, A29, A26, A31, Th1;
then
card (b1 \/ b2) = k + 2
by A33, XBOOLE_0:def 10;
then A35:
b1 \/ b2 = x
by A21, A22, A24, A30, A26, A31, CARD_2:102, XBOOLE_1:8;
F . b2 in the
Points of
(G_ ((k + 1),X))
;
then A36:
ex
B12 being
Subset of
X st
(
F . b2 = B12 &
card B12 = k + 1 )
by A6;
F . b1 in the
Points of
(G_ ((k + 1),X))
;
then A37:
ex
B11 being
Subset of
X st
(
F . b1 = B11 &
card B11 = k + 1 )
by A6;
F . A in the
Lines of
(G_ ((k + 1),X))
;
then A38:
ex
L1 being
Subset of
X st
(
F . A = L1 &
card L1 = (k + 1) + 1 )
by A17;
then A39:
F . A is
finite
;
F . b1 <> F . b2
by A18, A12, A34, FUNCT_1:def 4;
then A40:
(k + 1) + 1
c= card ((F . b1) \/ (F . b2))
by A37, A36, Th1;
b1 on A
by A5, A20, A22, A26, Th10;
then
F . b1 on F . A
by A10;
then A41:
F . b1 c= F . A
by A5, Th10;
then
(F . b1) \/ (F . b2) c= F . A
by A32, XBOOLE_1:8;
then
card ((F . b1) \/ (F . b2)) c= k + 2
by A38, CARD_1:11;
then
card ((F . b1) \/ (F . b2)) = k + 2
by A40, XBOOLE_0:def 10;
then A42:
(F . b1) \/ (F . b2) = F . A
by A41, A32, A38, A39, CARD_2:102, XBOOLE_1:8;
A43:
(incprojmap ((k + 1),f)) . A = f .: x
by A5, A20, Def14;
A44:
(
(f .: b1) \/ (f .: b2) = f .: (b1 \/ b2) &
F . b2 = (incprojmap ((k + 1),f)) . b2 )
by A12, A14, RELAT_1:120;
(
F . b1 = (incprojmap ((k + 1),f)) . b1 &
(incprojmap ((k + 1),f)) . b1 = f .: b1 )
by A5, A12, A14, Def14;
hence
the
line-map of
F . x = the
line-map of
(incprojmap ((k + 1),f)) . x
by A5, A20, A35, A42, A43, A44, Def14;
verum
end;
A45:
( dom the line-map of F = the Lines of (G_ ((k + 1),X)) & dom the line-map of (incprojmap ((k + 1),f)) = the Lines of (G_ ((k + 1),X)) )
by FUNCT_2:52;
dom the point-map of (incprojmap ((k + 1),f)) = the Points of (G_ ((k + 1),X))
by FUNCT_2:52;
then
the point-map of F = the point-map of (incprojmap ((k + 1),f))
by A12, A14;
hence
IncProjMap(# the point-map of F, the line-map of F #) = incprojmap ((k + 1),f)
by A45, A19, FUNCT_1:def 11; verum