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

Metamath Proof Explorer

Theorem symgextfv

Description: The function value of the extension of a permutation, fixing the additional element, for elements in 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 symgextfv 
|- ( ( K e. N /\ Z e. S ) -> ( X e. ( N \ { K } ) -> ( E ` X ) = ( Z ` X ) ) )

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 eldifi 
 |-  ( X e. ( N \ { K } ) -> X e. N )
4 fvexd 
 |-  ( ( K e. N /\ Z e. S ) -> ( Z ` X ) e. _V )
5 ifexg 
 |-  ( ( K e. N /\ ( Z ` X ) e. _V ) -> if ( X = K , K , ( Z ` X ) ) e. _V )
6 4 5 syldan 
 |-  ( ( K e. N /\ Z e. S ) -> if ( X = K , K , ( Z ` X ) ) e. _V )
7 eqeq1 
 |-  ( x = X -> ( x = K <-> X = K ) )
8 fveq2 
 |-  ( x = X -> ( Z ` x ) = ( Z ` X ) )
9 7 8 ifbieq2d 
 |-  ( x = X -> if ( x = K , K , ( Z ` x ) ) = if ( X = K , K , ( Z ` X ) ) )
10 9 2 fvmptg 
 |-  ( ( X e. N /\ if ( X = K , K , ( Z ` X ) ) e. _V ) -> ( E ` X ) = if ( X = K , K , ( Z ` X ) ) )
11 3 6 10 syl2anr 
 |-  ( ( ( K e. N /\ Z e. S ) /\ X e. ( N \ { K } ) ) -> ( E ` X ) = if ( X = K , K , ( Z ` X ) ) )
12 eldifsnneq 
 |-  ( X e. ( N \ { K } ) -> -. X = K )
13 12 adantl 
 |-  ( ( ( K e. N /\ Z e. S ) /\ X e. ( N \ { K } ) ) -> -. X = K )
14 13 iffalsed 
 |-  ( ( ( K e. N /\ Z e. S ) /\ X e. ( N \ { K } ) ) -> if ( X = K , K , ( Z ` X ) ) = ( Z ` X ) )
15 11 14 eqtrd 
 |-  ( ( ( K e. N /\ Z e. S ) /\ X e. ( N \ { K } ) ) -> ( E ` X ) = ( Z ` X ) )
16 15 ex 
 |-  ( ( K e. N /\ Z e. S ) -> ( X e. ( N \ { K } ) -> ( E ` X ) = ( Z ` X ) ) )