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

Metamath Proof Explorer

Theorem symgextsymg

Description: The extension of a permutation is an element of the extended symmetric group. (Contributed by AV, 9-Mar-2019)

Ref Expression
Hypotheses symgext.s ⊢ S = Base SymGrp ⁡ N ∖ K
symgext.e ⊢ E = x ∈ N ⟼ if x = K K Z ⁡ x
Assertion symgextsymg ⊢ N ∈ V ∧ K ∈ N ∧ Z ∈ S → E ∈ Base SymGrp ⁡ N

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 symgextf1o ⊢ K ∈ N ∧ Z ∈ S → E : N ⟶ 1-1 onto N
4 3 3adant1 ⊢ N ∈ V ∧ K ∈ N ∧ Z ∈ S → E : N ⟶ 1-1 onto N
5 eqid ⊢ SymGrp ⁡ N = SymGrp ⁡ N
6 eqid ⊢ Base SymGrp ⁡ N = Base SymGrp ⁡ N
7 5 6 elsymgbas ⊢ N ∈ V → E ∈ Base SymGrp ⁡ N ↔ E : N ⟶ 1-1 onto N
8 7 3ad2ant1 ⊢ N ∈ V ∧ K ∈ N ∧ Z ∈ S → E ∈ Base SymGrp ⁡ N ↔ E : N ⟶ 1-1 onto N
9 4 8 mpbird ⊢ N ∈ V ∧ K ∈ N ∧ Z ∈ S → E ∈ Base SymGrp ⁡ N