let k be Nat; for X being non empty set st 0 < k & k + 1 c= card X holds
for s being Permutation of X holds incprojmap (k,s) is automorphism
let X be non empty set ; ( 0 < k & k + 1 c= card X implies for s being Permutation of X holds incprojmap (k,s) is automorphism )
assume A1:
( 0 < k & k + 1 c= card X )
; for s being Permutation of X holds incprojmap (k,s) is automorphism
let s be Permutation of X; incprojmap (k,s) is automorphism
A2:
the Points of (G_ (k,X)) = { A where A is Subset of X : card A = k }
by A1, Def1;
A3:
the point-map of (incprojmap (k,s)) is one-to-one
proof
let x1,
x2 be
object ;
FUNCT_1:def 4 ( not x1 in dom the point-map of (incprojmap (k,s)) or not x2 in dom the point-map of (incprojmap (k,s)) or not the point-map of (incprojmap (k,s)) . x1 = the point-map of (incprojmap (k,s)) . x2 or x1 = x2 )
assume that A4:
x1 in dom the
point-map of
(incprojmap (k,s))
and A5:
x2 in dom the
point-map of
(incprojmap (k,s))
and A6:
the
point-map of
(incprojmap (k,s)) . x1 = the
point-map of
(incprojmap (k,s)) . x2
;
x1 = x2
consider X1 being
POINT of
(G_ (k,X)) such that A7:
X1 = x1
by A4;
x1 in the
Points of
(G_ (k,X))
by A4;
then A8:
ex
X11 being
Subset of
X st
(
X11 = x1 &
card X11 = k )
by A2;
consider X2 being
POINT of
(G_ (k,X)) such that A9:
X2 = x2
by A5;
x2 in the
Points of
(G_ (k,X))
by A5;
then A10:
ex
X12 being
Subset of
X st
(
X12 = x2 &
card X12 = k )
by A2;
A11:
(incprojmap (k,s)) . X2 = s .: X2
by A1, Def14;
(incprojmap (k,s)) . X1 = s .: X1
by A1, Def14;
hence
x1 = x2
by A6, A7, A9, A8, A10, A11, Th6;
verum
end;
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 = the point-map of (incprojmap (k,s)) . 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 = the point-map of (incprojmap (k,s)) . x ) )
assume
y in the
Points of
(G_ (k,X))
;
ex x being object st
( x in the Points of (G_ (k,X)) & y = the point-map of (incprojmap (k,s)) . x )
then A12:
ex
B being
Subset of
X st
(
B = y &
card B = k )
by A2;
reconsider y =
y as
set by TARSKI:1;
A13:
s " y c= dom s
by RELAT_1:132;
then A14:
s " y c= X
by FUNCT_2:52;
rng s = X
by FUNCT_2:def 3;
then A15:
s .: (s " y) = y
by A12, FUNCT_1:77;
then
card (s " y) = k
by A12, A13, Th4;
then
s " y in the
Points of
(G_ (k,X))
by A2, A14;
then consider A being
POINT of
(G_ (k,X)) such that A16:
A = s " y
;
y = (incprojmap (k,s)) . A
by A1, A15, A16, Def14;
hence
ex
x being
object st
(
x in the
Points of
(G_ (k,X)) &
y = the
point-map of
(incprojmap (k,s)) . x )
;
verum
end;
then
rng the point-map of (incprojmap (k,s)) = the Points of (G_ (k,X))
by FUNCT_2:10;
then A17:
the point-map of (incprojmap (k,s)) is onto
by FUNCT_2:def 3;
A18:
the Lines of (G_ (k,X)) = { L where L is Subset of X : card L = k + 1 }
by A1, Def1;
for y being object st y in the Lines of (G_ (k,X)) holds
ex x being object st
( x in the Lines of (G_ (k,X)) & y = the line-map of (incprojmap (k,s)) . x )
proof
let y be
object ;
( y in the Lines of (G_ (k,X)) implies ex x being object st
( x in the Lines of (G_ (k,X)) & y = the line-map of (incprojmap (k,s)) . x ) )
assume
y in the
Lines of
(G_ (k,X))
;
ex x being object st
( x in the Lines of (G_ (k,X)) & y = the line-map of (incprojmap (k,s)) . x )
then A19:
ex
B being
Subset of
X st
(
B = y &
card B = k + 1 )
by A18;
reconsider y =
y as
set by TARSKI:1;
A20:
s " y c= dom s
by RELAT_1:132;
then A21:
s " y c= X
by FUNCT_2:52;
rng s = X
by FUNCT_2:def 3;
then A22:
s .: (s " y) = y
by A19, FUNCT_1:77;
then
card (s " y) = k + 1
by A19, A20, Th4;
then
s " y in the
Lines of
(G_ (k,X))
by A18, A21;
then consider A being
LINE of
(G_ (k,X)) such that A23:
A = s " y
;
y = (incprojmap (k,s)) . A
by A1, A22, A23, Def14;
hence
ex
x being
object st
(
x in the
Lines of
(G_ (k,X)) &
y = the
line-map of
(incprojmap (k,s)) . x )
;
verum
end;
then
rng the line-map of (incprojmap (k,s)) = the Lines of (G_ (k,X))
by FUNCT_2:10;
then A24:
the line-map of (incprojmap (k,s)) is onto
by FUNCT_2:def 3;
A25:
dom s = X
by FUNCT_2:52;
A26:
incprojmap (k,s) 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 (incprojmap (k,s)) . A1 on (incprojmap (k,s)) . L1 )let L1 be
LINE of
(G_ (k,X));
( A1 on L1 iff (incprojmap (k,s)) . A1 on (incprojmap (k,s)) . L1 )
A27:
(
s .: A1 = (incprojmap (k,s)) . A1 &
s .: L1 = (incprojmap (k,s)) . L1 )
by A1, Def14;
A1 in the
Points of
(G_ (k,X))
;
then A28:
ex
a1 being
Subset of
X st
(
A1 = a1 &
card a1 = k )
by A2;
A29:
(
(incprojmap (k,s)) . A1 on (incprojmap (k,s)) . L1 implies
A1 on L1 )
(
A1 on L1 implies
(incprojmap (k,s)) . A1 on (incprojmap (k,s)) . L1 )
hence
(
A1 on L1 iff
(incprojmap (k,s)) . A1 on (incprojmap (k,s)) . L1 )
by A29;
verum
end;
the line-map of (incprojmap (k,s)) is one-to-one
proof
let x1,
x2 be
object ;
FUNCT_1:def 4 ( not x1 in dom the line-map of (incprojmap (k,s)) or not x2 in dom the line-map of (incprojmap (k,s)) or not the line-map of (incprojmap (k,s)) . x1 = the line-map of (incprojmap (k,s)) . x2 or x1 = x2 )
assume that A30:
x1 in dom the
line-map of
(incprojmap (k,s))
and A31:
x2 in dom the
line-map of
(incprojmap (k,s))
and A32:
the
line-map of
(incprojmap (k,s)) . x1 = the
line-map of
(incprojmap (k,s)) . x2
;
x1 = x2
consider X1 being
LINE of
(G_ (k,X)) such that A33:
X1 = x1
by A30;
x1 in the
Lines of
(G_ (k,X))
by A30;
then A34:
ex
X11 being
Subset of
X st
(
X11 = x1 &
card X11 = k + 1 )
by A18;
consider X2 being
LINE of
(G_ (k,X)) such that A35:
X2 = x2
by A31;
x2 in the
Lines of
(G_ (k,X))
by A31;
then A36:
ex
X12 being
Subset of
X st
(
X12 = x2 &
card X12 = k + 1 )
by A18;
A37:
(incprojmap (k,s)) . X2 = s .: X2
by A1, Def14;
(incprojmap (k,s)) . X1 = s .: X1
by A1, Def14;
hence
x1 = x2
by A32, A33, A35, A34, A36, A37, Th6;
verum
end;
hence
incprojmap (k,s) is automorphism
by A24, A3, A17, A26; verum