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 ∈ N ⟼ if x = K K Z ⁡ x
Assertion symgextfv ⊢ K ∈ N ∧ Z ∈ S → X ∈ N ∖ K → E ⁡ X = Z ⁡ X

Proof

Step Hyp Ref Expression
1 symgext.s ⊢ S = Base SymGrp ⁡ N ∖ K
2 symgext.e ⊢ E = x ∈ N ⟼ if x = K K Z ⁡ x
3 eldifi ⊢ X ∈ N ∖ K → X ∈ N
4 fvexd ⊢ K ∈ N ∧ Z ∈ S → Z ⁡ X ∈ V
5 ifexg ⊢ K ∈ N ∧ Z ⁡ X ∈ V → if X = K K Z ⁡ X ∈ V
6 4 5 syldan ⊢ K ∈ N ∧ Z ∈ S → if X = K K Z ⁡ X ∈ 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 ∈ N ∧ if X = K K Z ⁡ X ∈ V → E ⁡ X = if X = K K Z ⁡ X
11 3 6 10 syl2anr ⊢ K ∈ N ∧ Z ∈ S ∧ X ∈ N ∖ K → E ⁡ X = if X = K K Z ⁡ X
12 eldifsnneq ⊢ X ∈ N ∖ K → ¬ X = K
13 12 adantl ⊢ K ∈ N ∧ Z ∈ S ∧ X ∈ N ∖ K → ¬ X = K
14 13 iffalsed ⊢ K ∈ N ∧ Z ∈ S ∧ X ∈ N ∖ K → if X = K K Z ⁡ X = Z ⁡ X
15 11 14 eqtrd ⊢ K ∈ N ∧ Z ∈ S ∧ X ∈ N ∖ K → E ⁡ X = Z ⁡ X
16 15 ex ⊢ K ∈ N ∧ Z ∈ S → X ∈ N ∖ K → E ⁡ X = Z ⁡ X