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 ) ) )