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