let k be 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

let s be Permutation of X; :: thesis: 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

ex x being object st

( x in the Points of (G_ (k,X)) & y = the point-map of (incprojmap (k,s)) . x )

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 )

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

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

let s be Permutation of X; :: thesis: 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

for y being object st y in the Points of (G_ (k,X)) holds
let x1, x2 be object ; :: according to FUNCT_1:def 4 :: 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 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 ; :: thesis: 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; :: thesis: verum

end;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 ; :: thesis: 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; :: thesis: verum

ex x being object st

( x in the Points of (G_ (k,X)) & y = the point-map of (incprojmap (k,s)) . x )

proof

then
rng the point-map of (incprojmap (k,s)) = the Points of (G_ (k,X))
by FUNCT_2:10;
let y be object ; :: thesis: ( 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)) ; :: thesis: 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 ) ; :: thesis: verum

end;( 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)) ; :: thesis: 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 ) ; :: thesis: verum

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

then
rng the line-map of (incprojmap (k,s)) = the Lines of (G_ (k,X))
by FUNCT_2:10;
let y be object ; :: thesis: ( 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)) ; :: thesis: 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 ) ; :: thesis: verum

end;( 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)) ; :: thesis: 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 ) ; :: thesis: verum

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

the line-map of (incprojmap (k,s)) is one-to-one
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 )

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 )

end;( 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 )

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 )

proof

( A1 on L1 implies (incprojmap (k,s)) . A1 on (incprojmap (k,s)) . L1 )
assume
(incprojmap (k,s)) . A1 on (incprojmap (k,s)) . L1
; :: thesis: A1 on L1

then s .: A1 c= s .: L1 by A1, A27, Th10;

then A1 c= L1 by A25, A28, FUNCT_1:87;

hence A1 on L1 by A1, Th10; :: thesis: verum

end;then s .: A1 c= s .: L1 by A1, A27, Th10;

then A1 c= L1 by A25, A28, FUNCT_1:87;

hence A1 on L1 by A1, Th10; :: thesis: verum

proof

hence
( A1 on L1 iff (incprojmap (k,s)) . A1 on (incprojmap (k,s)) . L1 )
by A29; :: thesis: verum
assume
A1 on L1
; :: thesis: (incprojmap (k,s)) . A1 on (incprojmap (k,s)) . L1

then A1 c= L1 by A1, Th10;

then s .: A1 c= s .: L1 by RELAT_1:123;

hence (incprojmap (k,s)) . A1 on (incprojmap (k,s)) . L1 by A1, A27, Th10; :: thesis: verum

end;then A1 c= L1 by A1, Th10;

then s .: A1 c= s .: L1 by RELAT_1:123;

hence (incprojmap (k,s)) . A1 on (incprojmap (k,s)) . L1 by A1, A27, Th10; :: thesis: verum

proof

hence
incprojmap (k,s) is automorphism
by A24, A3, A17, A26; :: thesis: verum
let x1, x2 be object ; :: according to FUNCT_1:def 4 :: 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 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 ; :: thesis: 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; :: thesis: verum

end;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 ; :: thesis: 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; :: thesis: verum