let k be Element of NAT ; :: thesis: 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 ; :: thesis: ( 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 )
; :: thesis: for s being Permutation of X holds 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 Lines of (G_ k,X) = { L where L is Subset of X : card L = k + 1 }
by A1, Def1;
let s be Permutation of X; :: thesis: incprojmap k,s is automorphism
A4:
dom s = X
by FUNCT_2:67;
A5:
the line-map of (incprojmap k,s) is bijective
proof
A6:
the
line-map of
(incprojmap k,s) is
one-to-one
proof
let x1,
x2 be
set ;
:: according to FUNCT_1:def 8 :: thesis: ( 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 A7:
(
x1 in dom the
line-map of
(incprojmap k,s) &
x2 in dom the
line-map of
(incprojmap k,s) & the
line-map of
(incprojmap k,s) . x1 = the
line-map of
(incprojmap k,s) . x2 )
;
:: thesis: x1 = x2
then A8:
(
x1 in the
Lines of
(G_ k,X) &
x2 in the
Lines of
(G_ k,X) )
;
consider X1 being
LINE of
(G_ k,X) such that A9:
X1 = x1
by A7;
consider X2 being
LINE of
(G_ k,X) such that A10:
X2 = x2
by A7;
consider X11 being
Subset of
X such that A11:
(
X11 = x1 &
card X11 = k + 1 )
by A3, A8;
consider X12 being
Subset of
X such that A12:
(
X12 = x2 &
card X12 = k + 1 )
by A3, A8;
(
(incprojmap k,s) . X1 = s .: x1 &
(incprojmap k,s) . X2 = s .: x2 )
by A1, A9, A10, Def14;
hence
x1 = x2
by A7, A9, A10, A11, A12, Th6;
:: thesis: verum
end;
the
line-map of
(incprojmap k,s) is
onto
proof
for
y being
set st
y in the
Lines of
(G_ k,X) holds
ex
x being
set st
(
x in the
Lines of
(G_ k,X) &
y = the
line-map of
(incprojmap k,s) . x )
proof
let y be
set ;
:: thesis: ( y in the Lines of (G_ k,X) implies ex x being set st
( x in the Lines of (G_ k,X) & y = the line-map of (incprojmap k,s) . x ) )
assume A13:
y in the
Lines of
(G_ k,X)
;
:: thesis: ex x being set st
( x in the Lines of (G_ k,X) & y = the line-map of (incprojmap k,s) . x )
consider B being
Subset of
X such that A14:
(
B = y &
card B = k + 1 )
by A3, A13;
rng s = X
by FUNCT_2:def 3;
then A15:
(
s " y c= dom s &
s .: (s " y) = y )
by A14, FUNCT_1:147, RELAT_1:167;
then
(
card (s " y) = k + 1 &
s " y c= X )
by A14, Th4, FUNCT_2:67;
then
s " y in the
Lines of
(G_ k,X)
by A3;
then consider A being
LINE of
(G_ k,X) such that A16:
A = s " y
;
y = (incprojmap k,s) . A
by A1, A15, A16, Def14;
hence
ex
x being
set st
(
x in the
Lines of
(G_ k,X) &
y = the
line-map of
(incprojmap k,s) . x )
;
:: thesis: verum
end;
then
rng the
line-map of
(incprojmap k,s) = the
Lines of
(G_ k,X)
by FUNCT_2:16;
hence
the
line-map of
(incprojmap k,s) is
onto
by FUNCT_2:def 3;
:: thesis: verum
end;
hence
the
line-map of
(incprojmap k,s) is
bijective
by A6;
:: thesis: verum
end;
A17:
the point-map of (incprojmap k,s) is bijective
proof
A18:
the
point-map of
(incprojmap k,s) is
one-to-one
proof
let x1,
x2 be
set ;
:: according to FUNCT_1:def 8 :: thesis: ( 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 A19:
(
x1 in dom the
point-map of
(incprojmap k,s) &
x2 in dom the
point-map of
(incprojmap k,s) & the
point-map of
(incprojmap k,s) . x1 = the
point-map of
(incprojmap k,s) . x2 )
;
:: thesis: x1 = x2
then A20:
(
x1 in the
Points of
(G_ k,X) &
x2 in the
Points of
(G_ k,X) )
;
consider X1 being
POINT of
(G_ k,X) such that A21:
X1 = x1
by A19;
consider X2 being
POINT of
(G_ k,X) such that A22:
X2 = x2
by A19;
consider X11 being
Subset of
X such that A23:
(
X11 = x1 &
card X11 = k )
by A2, A20;
consider X12 being
Subset of
X such that A24:
(
X12 = x2 &
card X12 = k )
by A2, A20;
(
(incprojmap k,s) . X1 = s .: x1 &
(incprojmap k,s) . X2 = s .: x2 )
by A1, A21, A22, Def14;
hence
x1 = x2
by A19, A21, A22, A23, A24, Th6;
:: thesis: verum
end;
the
point-map of
(incprojmap k,s) is
onto
proof
for
y being
set st
y in the
Points of
(G_ k,X) holds
ex
x being
set st
(
x in the
Points of
(G_ k,X) &
y = the
point-map of
(incprojmap k,s) . x )
proof
let y be
set ;
:: thesis: ( y in the Points of (G_ k,X) implies ex x being set st
( x in the Points of (G_ k,X) & y = the point-map of (incprojmap k,s) . x ) )
assume A25:
y in the
Points of
(G_ k,X)
;
:: thesis: ex x being set st
( x in the Points of (G_ k,X) & y = the point-map of (incprojmap k,s) . x )
consider B being
Subset of
X such that A26:
(
B = y &
card B = k )
by A2, A25;
rng s = X
by FUNCT_2:def 3;
then A27:
(
s " y c= dom s &
s .: (s " y) = y )
by A26, FUNCT_1:147, RELAT_1:167;
then
(
card (s " y) = k &
s " y c= X )
by A26, Th4, FUNCT_2:67;
then
s " y in the
Points of
(G_ k,X)
by A2;
then consider A being
POINT of
(G_ k,X) such that A28:
A = s " y
;
y = (incprojmap k,s) . A
by A1, A27, A28, Def14;
hence
ex
x being
set st
(
x in the
Points of
(G_ k,X) &
y = the
point-map of
(incprojmap k,s) . x )
;
:: thesis: verum
end;
then
rng the
point-map of
(incprojmap k,s) = the
Points of
(G_ k,X)
by FUNCT_2:16;
hence
the
point-map of
(incprojmap k,s) is
onto
by FUNCT_2:def 3;
:: thesis: verum
end;
hence
the
point-map of
(incprojmap k,s) is
bijective
by A18;
:: thesis: verum
end;
incprojmap k,s is incidence_preserving
proof
let A1 be
POINT of
(G_ k,X);
:: according to COMBGRAS:def 8 :: thesis: 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);
:: thesis: ( A1 on L1 iff (incprojmap k,s) . A1 on (incprojmap k,s) . L1 )
A1 in the
Points of
(G_ k,X)
;
then consider a1 being
Subset of
X such that A29:
(
A1 = a1 &
card a1 = k )
by A2;
A30:
(
s .: A1 = (incprojmap k,s) . A1 &
s .: L1 = (incprojmap k,s) . L1 )
by A1, Def14;
A31:
(
A1 on L1 implies
(incprojmap k,s) . A1 on (incprojmap k,s) . L1 )
(
(incprojmap k,s) . A1 on (incprojmap k,s) . L1 implies
A1 on L1 )
hence
(
A1 on L1 iff
(incprojmap k,s) . A1 on (incprojmap k,s) . L1 )
by A31;
:: thesis: verum
end;
hence
incprojmap k,s is automorphism
by A5, A17, Def9; :: thesis: verum