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 )