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
ex H being IncProjMap over 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)))) ) )
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
ex H being IncProjMap over 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)))) ) ) )
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
ex H being IncProjMap over 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)))) ) )
let F be IncProjMap over G_ ((k + 1),X), G_ ((k + 1),X); ( F is automorphism implies ex H being IncProjMap over 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)))) ) ) )
assume A3:
F is automorphism
; ex H being IncProjMap over 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)))) ) )
0 + 2 < k + (1 + 1)
by A1, XREAL_1:6;
then
0 + 2 < (k + 1) + 1
;
then A4:
2 <= k + 1
by NAT_1:13;
defpred S1[ object , object ] means ex B being finite set st
( B = $1 & $2 = meet (F .: (^^ (B,X,(k + 1)))) );
(k + 1) + 0 <= (k + 1) + 2
by XREAL_1:6;
then
Segm (k + 1) c= Segm (k + 3)
by NAT_1:39;
then A5:
k + 1 c= card X
by A2;
then A6:
the Points of (G_ (k,X)) = { A where A is Subset of X : card A = k }
by A1, Def1;
A7:
for e being object st e in the Points of (G_ (k,X)) holds
ex u being object st S1[e,u]
proof
let e be
object ;
( e in the Points of (G_ (k,X)) implies ex u being object st S1[e,u] )
assume
e in the
Points of
(G_ (k,X))
;
ex u being object st S1[e,u]
then
ex
B being
Subset of
X st
(
B = e &
card B = k )
by A6;
then reconsider B =
e as
finite Subset of
X ;
take
meet (F .: (^^ (B,X,(k + 1))))
;
S1[e, meet (F .: (^^ (B,X,(k + 1))))]
thus
S1[
e,
meet (F .: (^^ (B,X,(k + 1))))]
;
verum
end;
consider Hp being Function such that
A8:
dom Hp = the Points of (G_ (k,X))
and
A9:
for e being object st e in the Points of (G_ (k,X)) holds
S1[e,Hp . e]
from CLASSES1:sch 1(A7);
A10:
the Lines of (G_ (k,X)) = { L where L is Subset of X : card L = k + 1 }
by A1, A5, Def1;
(k + 1) + 1 <= (k + 1) + 2
by XREAL_1:6;
then
Segm (k + 2) c= Segm (k + 3)
by NAT_1:39;
then A11:
(k + 1) + 1 c= card X
by A2;
then A12:
the Points of (G_ ((k + 1),X)) = { A where A is Subset of X : card A = k + 1 }
by Def1;
then reconsider Hl = the point-map of F as Function of the Lines of (G_ (k,X)), the Lines of (G_ (k,X)) by A10;
A13:
(k + 1) + 2 c= card X
by A2;
rng Hp c= the Points of (G_ (k,X))
proof
let y be
object ;
TARSKI:def 3 ( not y in rng Hp or y in the Points of (G_ (k,X)) )
assume
y in rng Hp
;
y in the Points of (G_ (k,X))
then consider x being
object such that A14:
x in dom Hp
and A15:
y = Hp . x
by FUNCT_1:def 3;
consider B being
finite set such that A16:
B = x
and A17:
y = meet (F .: (^^ (B,X,(k + 1))))
by A8, A9, A14, A15;
A18:
ex
x1 being
Subset of
X st
(
x = x1 &
card x1 = k )
by A6, A8, A14;
^^ (
B,
X,
(k + 1)) is
STAR
by A11, A16, A18, Th29;
then
F .: (^^ (B,X,(k + 1))) is
STAR
by A3, A4, A13, Th23;
then consider S being
Subset of
X such that A19:
card S = (k + 1) - 1
and A20:
F .: (^^ (B,X,(k + 1))) = { C where C is Subset of X : ( card C = k + 1 & S c= C ) }
;
S = meet (F .: (^^ (B,X,(k + 1))))
by A11, A19, A20, Th26;
hence
y in the
Points of
(G_ (k,X))
by A6, A17, A19;
verum
end;
then reconsider Hp = Hp as Function of the Points of (G_ (k,X)), the Points of (G_ (k,X)) by A8, FUNCT_2:2;
A21:
the point-map of F is bijective
by A3;
A22:
Hp is one-to-one
proof
let x1,
x2 be
object ;
FUNCT_1:def 4 ( not x1 in dom Hp or not x2 in dom Hp or not Hp . x1 = Hp . x2 or x1 = x2 )
assume that A23:
x1 in dom Hp
and A24:
x2 in dom Hp
and A25:
Hp . x1 = Hp . x2
;
x1 = x2
consider X2 being
finite set such that A26:
X2 = x2
and A27:
Hp . x2 = meet (F .: (^^ (X2,X,(k + 1))))
by A9, A24;
A28:
ex
x12 being
Subset of
X st
(
x2 = x12 &
card x12 = k )
by A6, A8, A24;
then A29:
card X2 = (k + 1) - 1
by A26;
then A30:
meet (^^ (X2,X,(k + 1))) = X2
by A11, A26, A28, Th30;
^^ (
X2,
X,
(k + 1)) is
STAR
by A11, A26, A28, Th29;
then A31:
F .: (^^ (X2,X,(k + 1))) is
STAR
by A3, A4, A13, Th23;
consider X1 being
finite set such that A32:
X1 = x1
and A33:
Hp . x1 = meet (F .: (^^ (X1,X,(k + 1))))
by A9, A23;
A34:
ex
x11 being
Subset of
X st
(
x1 = x11 &
card x11 = k )
by A6, A8, A23;
^^ (
X1,
X,
(k + 1)) is
STAR
by A11, A32, A34, Th29;
then A35:
F .: (^^ (X1,X,(k + 1))) is
STAR
by A3, A4, A13, Th23;
meet (^^ (X1,X,(k + 1))) = X1
by A11, A32, A34, A29, Th30;
hence
x1 = x2
by A11, A21, A25, A32, A33, A26, A27, A35, A31, A30, Th6, Th28;
verum
end;
take H = IncProjMap(# Hp,Hl #); ( 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)))) ) )
A36:
dom the point-map of F = the Points of (G_ ((k + 1),X))
by FUNCT_2:52;
A37:
H is incidence_preserving
proof
let A1 be
POINT of
(G_ (k,X));
COMBGRAS:def 8 for L1 being LINE of (G_ (k,X)) holds
( A1 on L1 iff H . A1 on H . L1 )let L1 be
LINE of
(G_ (k,X));
( A1 on L1 iff H . A1 on H . L1 )
A38:
S1[
A1,
Hp . A1]
by A9;
L1 in the
Lines of
(G_ (k,X))
;
then A39:
ex
l1 being
Subset of
X st
(
l1 = L1 &
card l1 = k + 1 )
by A10;
A1 in the
Points of
(G_ (k,X))
;
then consider a1 being
Subset of
X such that A40:
a1 = A1
and A41:
card a1 = k
by A6;
consider L11 being
POINT of
(G_ ((k + 1),X)) such that A42:
L11 = L1
by A10, A12;
reconsider a1 =
a1 as
finite Subset of
X by A41;
A43:
card a1 = (k + 1) - 1
by A41;
A44:
(
H . A1 on H . L1 implies
A1 on L1 )
proof
(
F " (F .: (^^ (a1,X,(k + 1)))) c= ^^ (
a1,
X,
(k + 1)) &
^^ (
a1,
X,
(k + 1))
c= F " (F .: (^^ (a1,X,(k + 1)))) )
by A21, A36, FUNCT_1:76, FUNCT_1:82;
then A45:
F " (F .: (^^ (a1,X,(k + 1)))) = ^^ (
a1,
X,
(k + 1))
by XBOOLE_0:def 10;
H . L1 in the
Lines of
(G_ (k,X))
;
then A46:
ex
hl1 being
Subset of
X st
(
hl1 = H . L1 &
card hl1 = k + 1 )
by A10;
^^ (
a1,
X,
(k + 1)) is
STAR
by A11, A43, Th29;
then
F .: (^^ (a1,X,(k + 1))) is
STAR
by A3, A4, A13, Th23;
then consider S being
Subset of
X such that A47:
card S = (k + 1) - 1
and A48:
F .: (^^ (a1,X,(k + 1))) = { A where A is Subset of X : ( card A = k + 1 & S c= A ) }
;
H . A1 in the
Points of
(G_ (k,X))
;
then consider ha1 being
Subset of
X such that A49:
ha1 = H . A1
and A50:
card ha1 = k
by A6;
reconsider ha1 =
ha1,
S =
S as
finite Subset of
X by A50, A47;
A51:
^^ (
ha1,
X,
(k + 1))
= ^^ (
ha1,
X)
by A11, A50, A47, Def13;
assume
H . A1 on H . L1
;
A1 on L1
then
H . A1 c= H . L1
by A1, A5, Th10;
then
F . L11 in ^^ (
ha1,
X,
(k + 1))
by A42, A49, A50, A46, A51;
then
L1 in F " (^^ (ha1,X,(k + 1)))
by A36, A42, FUNCT_1:def 7;
then A52:
meet (F " (^^ (ha1,X,(k + 1)))) c= L1
by SETFAM_1:3;
^^ (
S,
X,
(k + 1))
= ^^ (
S,
X)
by A11, A47, Def13;
then A53:
S = meet (F .: (^^ (a1,X,(k + 1))))
by A11, A47, A48, Th30;
meet (^^ (a1,X,(k + 1))) = a1
by A11, A41, A47, Th30;
hence
A1 on L1
by A1, A5, A40, A38, A49, A50, A48, A51, A53, A52, A45, Th10;
verum
end;
A54:
^^ (
a1,
X,
(k + 1))
= ^^ (
a1,
X)
by A11, A43, Def13;
(
A1 on L1 implies
H . A1 on H . L1 )
proof
assume
A1 on L1
;
H . A1 on H . L1
then
A1 c= L1
by A1, A5, Th10;
then
L1 in ^^ (
a1,
X,
(k + 1))
by A40, A41, A39, A54;
then
F . L11 in F .: (^^ (a1,X,(k + 1)))
by A36, A42, FUNCT_1:def 6;
then
meet (F .: (^^ (a1,X,(k + 1)))) c= F . L11
by SETFAM_1:3;
hence
H . A1 on H . L1
by A1, A5, A40, A42, A38, Th10;
verum
end;
hence
(
A1 on L1 iff
H . A1 on H . L1 )
by A44;
verum
end;
A55:
rng the point-map of F = the Points of (G_ ((k + 1),X))
by A21, FUNCT_2:def 3;
for y being object st y in the Points of (G_ (k,X)) holds
ex x being object st
( x in the Points of (G_ (k,X)) & y = Hp . x )
proof
let y be
object ;
( y in the Points of (G_ (k,X)) implies ex x being object st
( x in the Points of (G_ (k,X)) & y = Hp . x ) )
assume
y in the
Points of
(G_ (k,X))
;
ex x being object st
( x in the Points of (G_ (k,X)) & y = Hp . x )
then A56:
ex
Y1 being
Subset of
X st
(
y = Y1 &
card Y1 = k )
by A6;
then reconsider y =
y as
finite Subset of
X ;
A57:
card y = (k + 1) - 1
by A56;
then
^^ (
y,
X,
(k + 1)) is
STAR
by A11, Th29;
then
F " (^^ (y,X,(k + 1))) is
STAR
by A3, A4, A13, Th23;
then consider S being
Subset of
X such that A58:
card S = (k + 1) - 1
and A59:
F " (^^ (y,X,(k + 1))) = { A where A is Subset of X : ( card A = k + 1 & S c= A ) }
;
A60:
S in the
Points of
(G_ (k,X))
by A6, A58;
reconsider S =
S as
finite Subset of
X by A58;
A61:
S1[
S,
Hp . S]
by A9, A60;
^^ (
S,
X,
(k + 1))
= ^^ (
S,
X)
by A11, A58, Def13;
then
Hp . S = meet (^^ (y,X,(k + 1)))
by A55, A58, A59, A61, FUNCT_1:77;
then
y = Hp . S
by A11, A57, Th30;
hence
ex
x being
object st
(
x in the
Points of
(G_ (k,X)) &
y = Hp . x )
by A60;
verum
end;
then
rng Hp = the Points of (G_ (k,X))
by FUNCT_2:10;
then A62:
Hp is onto
by FUNCT_2:def 3;
A63:
for A being POINT of (G_ (k,X))
for B being finite set st B = A holds
Hp . A = meet (F .: (^^ (B,X,(k + 1))))
proof
let A be
POINT of
(G_ (k,X));
for B being finite set st B = A holds
Hp . A = meet (F .: (^^ (B,X,(k + 1))))
A64:
S1[
A,
Hp . A]
by A9;
let B be
finite set ;
( B = A implies Hp . A = meet (F .: (^^ (B,X,(k + 1)))) )
assume
A = B
;
Hp . A = meet (F .: (^^ (B,X,(k + 1))))
hence
Hp . A = meet (F .: (^^ (B,X,(k + 1))))
by A64;
verum
end;
the line-map of H is bijective
by A3, A10, A12;
hence
( 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)))) ) )
by A63, A22, A62, A37; verum