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

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 1 2 symgextfv ⊢ K ∈ N ∧ Z ∈ S → i ∈ N ∖ K → E ⁡ i = Z ⁡ i
4 3 ralrimiv ⊢ K ∈ N ∧ Z ∈ S → ∀ i ∈ N ∖ K E ⁡ i = Z ⁡ i
5 1 2 symgextf ⊢ K ∈ N ∧ Z ∈ S → E : N ⟶ N
6 5 ffnd ⊢ K ∈ N ∧ Z ∈ S → E Fn N
7 eqid ⊢ SymGrp ⁡ N ∖ K = SymGrp ⁡ N ∖ K
8 7 1 symgbasf ⊢ Z ∈ S → Z : N ∖ K ⟶ N ∖ K
9 8 ffnd ⊢ Z ∈ S → Z Fn N ∖ K
10 9 adantl ⊢ K ∈ N ∧ Z ∈ S → Z Fn N ∖ K
11 difssd ⊢ K ∈ N ∧ Z ∈ S → N ∖ K ⊆ N
12 fvreseq1 ⊢ E Fn N ∧ Z Fn N ∖ K ∧ N ∖ K ⊆ N → E ↾ N ∖ K = Z ↔ ∀ i ∈ N ∖ K E ⁡ i = Z ⁡ i
13 6 10 11 12 syl21anc ⊢ K ∈ N ∧ Z ∈ S → E ↾ N ∖ K = Z ↔ ∀ i ∈ N ∖ K E ⁡ i = Z ⁡ i
14 4 13 mpbird ⊢ K ∈ N ∧ Z ∈ S → E ↾ N ∖ K = Z