This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem symgextf

Description: The extension of a permutation, fixing the additional element, is a function. (Contributed by AV, 6-Jan-2019)

Ref Expression
Hypotheses symgext.s 
|- S = ( Base ` ( SymGrp ` ( N \ { K } ) ) )
symgext.e 
|- E = ( x e. N |-> if ( x = K , K , ( Z ` x ) ) )
Assertion symgextf 
|- ( ( K e. N /\ Z e. S ) -> E : N --> N )

Proof

Step Hyp Ref Expression
1 symgext.s 
 |-  S = ( Base ` ( SymGrp ` ( N \ { K } ) ) )
2 symgext.e 
 |-  E = ( x e. N |-> if ( x = K , K , ( Z ` x ) ) )
3 simplll 
 |-  ( ( ( ( K e. N /\ Z e. S ) /\ x e. N ) /\ x = K ) -> K e. N )
4 simpllr 
 |-  ( ( ( ( K e. N /\ Z e. S ) /\ x e. N ) /\ -. x = K ) -> Z e. S )
5 simpr 
 |-  ( ( ( K e. N /\ Z e. S ) /\ x e. N ) -> x e. N )
6 neqne 
 |-  ( -. x = K -> x =/= K )
7 5 6 anim12i 
 |-  ( ( ( ( K e. N /\ Z e. S ) /\ x e. N ) /\ -. x = K ) -> ( x e. N /\ x =/= K ) )
8 eldifsn 
 |-  ( x e. ( N \ { K } ) <-> ( x e. N /\ x =/= K ) )
9 7 8 sylibr 
 |-  ( ( ( ( K e. N /\ Z e. S ) /\ x e. N ) /\ -. x = K ) -> x e. ( N \ { K } ) )
10 eqid 
 |-  ( SymGrp ` ( N \ { K } ) ) = ( SymGrp ` ( N \ { K } ) )
11 10 1 symgfv 
 |-  ( ( Z e. S /\ x e. ( N \ { K } ) ) -> ( Z ` x ) e. ( N \ { K } ) )
12 4 9 11 syl2anc 
 |-  ( ( ( ( K e. N /\ Z e. S ) /\ x e. N ) /\ -. x = K ) -> ( Z ` x ) e. ( N \ { K } ) )
13 12 eldifad 
 |-  ( ( ( ( K e. N /\ Z e. S ) /\ x e. N ) /\ -. x = K ) -> ( Z ` x ) e. N )
14 3 13 ifclda 
 |-  ( ( ( K e. N /\ Z e. S ) /\ x e. N ) -> if ( x = K , K , ( Z ` x ) ) e. N )
15 14 2 fmptd 
 |-  ( ( K e. N /\ Z e. S ) -> E : N --> N )