let k be Nat; :: thesis: for X being non empty set st 0 < k & k + 1 c= card X holds
for F being IncProjMap over G_ (k,X), G_ (k,X) holds
( F is automorphism iff ex s being Permutation of X st IncProjMap(# the point-map of F, the line-map of F #) = incprojmap (k,s) )
let X be non empty set ; :: thesis: ( 0 < k & k + 1 c= card X implies for F being IncProjMap over G_ (k,X), G_ (k,X) holds
( F is automorphism iff ex s being Permutation of X st IncProjMap(# the point-map of F, the line-map of F #) = incprojmap (k,s) ) )
assume that
A1: 0 < k and
A2: k + 1 c= card X ; :: thesis: for F being IncProjMap over G_ (k,X), G_ (k,X) holds
( F is automorphism iff ex s being Permutation of X st IncProjMap(# the point-map of F, the line-map of F #) = incprojmap (k,s) )
let F be IncProjMap over G_ (k,X), G_ (k,X); :: thesis: ( F is automorphism iff ex s being Permutation of X st IncProjMap(# the point-map of F, the line-map of F #) = incprojmap (k,s) )
A3: ( F is automorphism implies ex s being Permutation of X st IncProjMap(# the point-map of F, the line-map of F #) = incprojmap (k,s) )
proof
A4: ( card k = k & succ 1 = 1 + 1 ) ;
A5: card (k + 1) = k + 1 ;
k + 1 in succ (card X) by A2, ORDINAL1:22;
then A6: ( k + 1 = card X or k + 1 in card X ) by ORDINAL1:8;
A7: card 1 = 1 ;
( 0 + 1 < k + 1 & succ (Segm k) = Segm (k + 1) ) by A1, NAT_1:38, XREAL_1:8;
then Segm 1 in succ (Segm k) by A7, A5, NAT_1:41;
then ( 1 = k or Segm 1 in Segm k ) by ORDINAL1:8;
then A8: ( 1 = k or ( 1 < k & Segm 2 c= Segm k ) ) by A7, A4, NAT_1:41, ORDINAL1:21;
assume A9: F is automorphism ; :: thesis: ex s being Permutation of X st IncProjMap(# the point-map of F, the line-map of F #) = incprojmap (k,s)
succ (Segm (k + 1)) = Segm ((k + 1) + 1) by NAT_1:38;
then ( 1 = k or ( 1 < k & card X = k + 1 ) or ( 2 <= k & k + 2 c= card X ) ) by A6, A8, NAT_1:39, ORDINAL1:21;
hence ex s being Permutation of X st IncProjMap(# the point-map of F, the line-map of F #) = incprojmap (k,s) by A2, A9, Th24, Th25, Th33; :: thesis: verum
end;
( ex s being Permutation of X st IncProjMap(# the point-map of F, the line-map of F #) = incprojmap (k,s) implies F is automorphism )
proof
assume ex s being Permutation of X st IncProjMap(# the point-map of F, the line-map of F #) = incprojmap (k,s) ; :: thesis: F is automorphism
then consider s being Permutation of X such that
A10: IncProjMap(# the point-map of F, the line-map of F #) = incprojmap (k,s) ;
A11: incprojmap (k,s) is automorphism by A1, A2, Th34;
then A12: incprojmap (k,s) is incidence_preserving ;
A13: F is incidence_preserving
proof
let A be POINT of (G_ (k,X)); :: according to COMBGRAS:def 8 :: thesis: for L1 being LINE of (G_ (k,X)) holds
( A on L1 iff F . A on F . L1 )
let L be LINE of (G_ (k,X)); :: thesis: ( A on L iff F . A on F . L )
( F . A = (incprojmap (k,s)) . A & F . L = (incprojmap (k,s)) . L ) by A10;
hence ( A on L iff F . A on F . L ) by A12; :: thesis: verum
end;
( the line-map of F is bijective & the point-map of F is bijective ) by A10, A11;
hence F is automorphism by A13; :: thesis: verum
end;
hence ( F is automorphism iff ex s being Permutation of X st IncProjMap(# the point-map of F, the line-map of F #) = incprojmap (k,s) ) by A3; :: thesis: verum