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

Metamath Proof Explorer

Theorem symgextres

Description: The restriction of the extension of a permutation, fixing the additional element, to the original domain. (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 symgextres 
|- ( ( K e. N /\ Z e. S ) -> ( E |` ( N \ { K } ) ) = Z )

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 1 2 symgextfv 
 |-  ( ( K e. N /\ Z e. S ) -> ( i e. ( N \ { K } ) -> ( E ` i ) = ( Z ` i ) ) )
4 3 ralrimiv 
 |-  ( ( K e. N /\ Z e. S ) -> A. i e. ( N \ { K } ) ( E ` i ) = ( Z ` i ) )
5 1 2 symgextf 
 |-  ( ( K e. N /\ Z e. S ) -> E : N --> N )
6 5 ffnd 
 |-  ( ( K e. N /\ Z e. S ) -> E Fn N )
7 eqid 
 |-  ( SymGrp ` ( N \ { K } ) ) = ( SymGrp ` ( N \ { K } ) )
8 7 1 symgbasf 
 |-  ( Z e. S -> Z : ( N \ { K } ) --> ( N \ { K } ) )
9 8 ffnd 
 |-  ( Z e. S -> Z Fn ( N \ { K } ) )
10 9 adantl 
 |-  ( ( K e. N /\ Z e. S ) -> Z Fn ( N \ { K } ) )
11 difssd 
 |-  ( ( K e. N /\ Z e. S ) -> ( N \ { K } ) C_ N )
12 fvreseq1 
 |-  ( ( ( E Fn N /\ Z Fn ( N \ { K } ) ) /\ ( N \ { K } ) C_ N ) -> ( ( E |` ( N \ { K } ) ) = Z <-> A. i e. ( N \ { K } ) ( E ` i ) = ( Z ` i ) ) )
13 6 10 11 12 syl21anc 
 |-  ( ( K e. N /\ Z e. S ) -> ( ( E |` ( N \ { K } ) ) = Z <-> A. i e. ( N \ { K } ) ( E ` i ) = ( Z ` i ) ) )
14 4 13 mpbird 
 |-  ( ( K e. N /\ Z e. S ) -> ( E |` ( N \ { K } ) ) = Z )