Metamath Proof Explorer

Theorem psgnevpmb

Description: A class is an even permutation if it is a permutation with sign 1. (Contributed by SO, 9-Jul-2018)

Ref Expression
Hypotheses evpmss.s ⊢ S = SymGrp ⁡ D
evpmss.p ⊢ P = Base S
psgnevpmb.n ⊢ N = pmSgn ⁡ D
Assertion psgnevpmb ⊢ D ∈ Fin → F ∈ pmEven ⁡ D ↔ F ∈ P ∧ N ⁡ F = 1

Proof

Step Hyp Ref Expression
1 evpmss.s ⊢ S = SymGrp ⁡ D
2 evpmss.p ⊢ P = Base S
3 psgnevpmb.n ⊢ N = pmSgn ⁡ D
4 elex ⊢ D ∈ Fin → D ∈ V
5 fveq2 ⊢ d = D → pmSgn ⁡ d = pmSgn ⁡ D
6 5 3 eqtr4di ⊢ d = D → pmSgn ⁡ d = N
7 6 cnveqd ⊢ d = D → pmSgn ⁡ d -1 = N -1
8 7 imaeq1d ⊢ d = D → pmSgn ⁡ d -1 1 = N -1 1
9 df-evpm ⊢ pmEven = d ∈ V ⟼ pmSgn ⁡ d -1 1
10 3 fvexi ⊢ N ∈ V
11 10 cnvex ⊢ N -1 ∈ V
12 11 imaex ⊢ N -1 1 ∈ V
13 8 9 12 fvmpt ⊢ D ∈ V → pmEven ⁡ D = N -1 1
14 4 13 syl ⊢ D ∈ Fin → pmEven ⁡ D = N -1 1
15 14 eleq2d ⊢ D ∈ Fin → F ∈ pmEven ⁡ D ↔ F ∈ N -1 1
16 eqid ⊢ mulGrp ℂ fld ↾ 𝑠 1 − 1 = mulGrp ℂ fld ↾ 𝑠 1 − 1
17 1 3 16 psgnghm2 ⊢ D ∈ Fin → N ∈ S GrpHom mulGrp ℂ fld ↾ 𝑠 1 − 1
18 eqid ⊢ Base mulGrp ℂ fld ↾ 𝑠 1 − 1 = Base mulGrp ℂ fld ↾ 𝑠 1 − 1
19 2 18 ghmf ⊢ N ∈ S GrpHom mulGrp ℂ fld ↾ 𝑠 1 − 1 → N : P ⟶ Base mulGrp ℂ fld ↾ 𝑠 1 − 1
20 17 19 syl ⊢ D ∈ Fin → N : P ⟶ Base mulGrp ℂ fld ↾ 𝑠 1 − 1
21 ffn ⊢ N : P ⟶ Base mulGrp ℂ fld ↾ 𝑠 1 − 1 → N Fn P
22 fniniseg ⊢ N Fn P → F ∈ N -1 1 ↔ F ∈ P ∧ N ⁡ F = 1
23 20 21 22 3syl ⊢ D ∈ Fin → F ∈ N -1 1 ↔ F ∈ P ∧ N ⁡ F = 1
24 15 23 bitrd ⊢ D ∈ Fin → F ∈ pmEven ⁡ D ↔ F ∈ P ∧ N ⁡ F = 1