Metamath Proof Explorer

Theorem evpmsubg

Description: The alternating group is a subgroup of the symmetric group. (Contributed by Thierry Arnoux, 1-Nov-2023)

Ref Expression
Hypotheses evpmsubg.s ⊢ S = SymGrp ⁡ D
evpmsubg.a ⊢ A = pmEven ⁡ D
Assertion evpmsubg ⊢ D ∈ Fin → A ∈ SubGrp ⁡ S

Proof

Step Hyp Ref Expression
1 evpmsubg.s ⊢ S = SymGrp ⁡ D
2 evpmsubg.a ⊢ A = pmEven ⁡ D
3 2 evpmval ⊢ D ∈ Fin → A = pmSgn ⁡ D -1 1
4 eqid ⊢ pmSgn ⁡ D = pmSgn ⁡ D
5 eqid ⊢ mulGrp ℂ fld ↾ 𝑠 1 − 1 = mulGrp ℂ fld ↾ 𝑠 1 − 1
6 1 4 5 psgnghm2 ⊢ D ∈ Fin → pmSgn ⁡ D ∈ S GrpHom mulGrp ℂ fld ↾ 𝑠 1 − 1
7 5 cnmsgngrp ⊢ mulGrp ℂ fld ↾ 𝑠 1 − 1 ∈ Grp
8 5 cnmsgn0g ⊢ 1 = 0 mulGrp ℂ fld ↾ 𝑠 1 − 1
9 8 0subg ⊢ mulGrp ℂ fld ↾ 𝑠 1 − 1 ∈ Grp → 1 ∈ SubGrp ⁡ mulGrp ℂ fld ↾ 𝑠 1 − 1
10 7 9 ax-mp ⊢ 1 ∈ SubGrp ⁡ mulGrp ℂ fld ↾ 𝑠 1 − 1
11 ghmpreima ⊢ pmSgn ⁡ D ∈ S GrpHom mulGrp ℂ fld ↾ 𝑠 1 − 1 ∧ 1 ∈ SubGrp ⁡ mulGrp ℂ fld ↾ 𝑠 1 − 1 → pmSgn ⁡ D -1 1 ∈ SubGrp ⁡ S
12 6 10 11 sylancl ⊢ D ∈ Fin → pmSgn ⁡ D -1 1 ∈ SubGrp ⁡ S
13 3 12 eqeltrd ⊢ D ∈ Fin → A ∈ SubGrp ⁡ S