Metamath Proof Explorer


Theorem evpmval

Description: Value of the set of even permutations, the alternating group. (Contributed by Thierry Arnoux, 1-Nov-2023)

Ref Expression
Hypothesis evpmval.1 A = pmEven D
Assertion evpmval D V A = pmSgn D -1 1

Proof

Step Hyp Ref Expression
1 evpmval.1 A = pmEven D
2 elex D V D V
3 fveq2 d = D pmSgn d = pmSgn D
4 3 cnveqd d = D pmSgn d -1 = pmSgn D -1
5 4 imaeq1d d = D pmSgn d -1 1 = pmSgn D -1 1
6 df-evpm pmEven = d V pmSgn d -1 1
7 fvex pmSgn D V
8 7 cnvex pmSgn D -1 V
9 8 imaex pmSgn D -1 1 V
10 5 6 9 fvmpt D V pmEven D = pmSgn D -1 1
11 2 10 syl D V pmEven D = pmSgn D -1 1
12 1 11 syl5eq D V A = pmSgn D -1 1