Metamath Proof Explorer

Theorem psgninv

Description: The sign of a permutation equals the sign of the inverse of the permutation. (Contributed by SO, 9-Jul-2018)

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

Proof

Step Hyp Ref Expression
1 psgninv.s ⊢ S = SymGrp ⁡ D
2 psgninv.n ⊢ N = pmSgn ⁡ D
3 psgninv.p ⊢ P = Base S
4 eqid ⊢ mulGrp ℂ fld ↾ 𝑠 1 − 1 = mulGrp ℂ fld ↾ 𝑠 1 − 1
5 1 2 4 psgnghm2 ⊢ D ∈ Fin → N ∈ S GrpHom mulGrp ℂ fld ↾ 𝑠 1 − 1
6 eqid ⊢ inv g ⁡ S = inv g ⁡ S
7 eqid ⊢ inv g ⁡ mulGrp ℂ fld ↾ 𝑠 1 − 1 = inv g ⁡ mulGrp ℂ fld ↾ 𝑠 1 − 1
8 3 6 7 ghminv ⊢ N ∈ S GrpHom mulGrp ℂ fld ↾ 𝑠 1 − 1 ∧ F ∈ P → N ⁡ inv g ⁡ S ⁡ F = inv g ⁡ mulGrp ℂ fld ↾ 𝑠 1 − 1 ⁡ N ⁡ F
9 5 8 sylan ⊢ D ∈ Fin ∧ F ∈ P → N ⁡ inv g ⁡ S ⁡ F = inv g ⁡ mulGrp ℂ fld ↾ 𝑠 1 − 1 ⁡ N ⁡ F
10 1 3 6 symginv ⊢ F ∈ P → inv g ⁡ S ⁡ F = F -1
11 10 adantl ⊢ D ∈ Fin ∧ F ∈ P → inv g ⁡ S ⁡ F = F -1
12 11 fveq2d ⊢ D ∈ Fin ∧ F ∈ P → N ⁡ inv g ⁡ S ⁡ F = N ⁡ F -1
13 eqid ⊢ mulGrp ℂ fld ↾ 𝑠 ℂ ∖ 0 = mulGrp ℂ fld ↾ 𝑠 ℂ ∖ 0
14 13 cnmsgnsubg ⊢ 1 − 1 ∈ SubGrp ⁡ mulGrp ℂ fld ↾ 𝑠 ℂ ∖ 0
15 4 cnmsgnbas ⊢ 1 − 1 = Base mulGrp ℂ fld ↾ 𝑠 1 − 1
16 3 15 ghmf ⊢ N ∈ S GrpHom mulGrp ℂ fld ↾ 𝑠 1 − 1 → N : P ⟶ 1 − 1
17 5 16 syl ⊢ D ∈ Fin → N : P ⟶ 1 − 1
18 17 ffvelcdmda ⊢ D ∈ Fin ∧ F ∈ P → N ⁡ F ∈ 1 − 1
19 cnex ⊢ ℂ ∈ V
20 19 difexi ⊢ ℂ ∖ 0 ∈ V
21 ax-1cn ⊢ 1 ∈ ℂ
22 ax-1ne0 ⊢ 1 ≠ 0
23 eldifsn ⊢ 1 ∈ ℂ ∖ 0 ↔ 1 ∈ ℂ ∧ 1 ≠ 0
24 21 22 23 mpbir2an ⊢ 1 ∈ ℂ ∖ 0
25 neg1cn ⊢ − 1 ∈ ℂ
26 neg1ne0 ⊢ − 1 ≠ 0
27 eldifsn ⊢ − 1 ∈ ℂ ∖ 0 ↔ − 1 ∈ ℂ ∧ − 1 ≠ 0
28 25 26 27 mpbir2an ⊢ − 1 ∈ ℂ ∖ 0
29 prssi ⊢ 1 ∈ ℂ ∖ 0 ∧ − 1 ∈ ℂ ∖ 0 → 1 − 1 ⊆ ℂ ∖ 0
30 24 28 29 mp2an ⊢ 1 − 1 ⊆ ℂ ∖ 0
31 ressabs ⊢ ℂ ∖ 0 ∈ V ∧ 1 − 1 ⊆ ℂ ∖ 0 → mulGrp ℂ fld ↾ 𝑠 ℂ ∖ 0 ↾ 𝑠 1 − 1 = mulGrp ℂ fld ↾ 𝑠 1 − 1
32 20 30 31 mp2an ⊢ mulGrp ℂ fld ↾ 𝑠 ℂ ∖ 0 ↾ 𝑠 1 − 1 = mulGrp ℂ fld ↾ 𝑠 1 − 1
33 32 eqcomi ⊢ mulGrp ℂ fld ↾ 𝑠 1 − 1 = mulGrp ℂ fld ↾ 𝑠 ℂ ∖ 0 ↾ 𝑠 1 − 1
34 cnfldbas ⊢ ℂ = Base ℂ fld
35 cnfld0 ⊢ 0 = 0 ℂ fld
36 cndrng ⊢ ℂ fld ∈ DivRing
37 34 35 36 drngui ⊢ ℂ ∖ 0 = Unit ⁡ ℂ fld
38 eqid ⊢ inv r ⁡ ℂ fld = inv r ⁡ ℂ fld
39 37 13 38 invrfval ⊢ inv r ⁡ ℂ fld = inv g ⁡ mulGrp ℂ fld ↾ 𝑠 ℂ ∖ 0
40 33 39 7 subginv ⊢ 1 − 1 ∈ SubGrp ⁡ mulGrp ℂ fld ↾ 𝑠 ℂ ∖ 0 ∧ N ⁡ F ∈ 1 − 1 → inv r ⁡ ℂ fld ⁡ N ⁡ F = inv g ⁡ mulGrp ℂ fld ↾ 𝑠 1 − 1 ⁡ N ⁡ F
41 14 18 40 sylancr ⊢ D ∈ Fin ∧ F ∈ P → inv r ⁡ ℂ fld ⁡ N ⁡ F = inv g ⁡ mulGrp ℂ fld ↾ 𝑠 1 − 1 ⁡ N ⁡ F
42 30 18 sselid ⊢ D ∈ Fin ∧ F ∈ P → N ⁡ F ∈ ℂ ∖ 0
43 eldifsn ⊢ N ⁡ F ∈ ℂ ∖ 0 ↔ N ⁡ F ∈ ℂ ∧ N ⁡ F ≠ 0
44 42 43 sylib ⊢ D ∈ Fin ∧ F ∈ P → N ⁡ F ∈ ℂ ∧ N ⁡ F ≠ 0
45 cnfldinv ⊢ N ⁡ F ∈ ℂ ∧ N ⁡ F ≠ 0 → inv r ⁡ ℂ fld ⁡ N ⁡ F = 1 N ⁡ F
46 44 45 syl ⊢ D ∈ Fin ∧ F ∈ P → inv r ⁡ ℂ fld ⁡ N ⁡ F = 1 N ⁡ F
47 41 46 eqtr3d ⊢ D ∈ Fin ∧ F ∈ P → inv g ⁡ mulGrp ℂ fld ↾ 𝑠 1 − 1 ⁡ N ⁡ F = 1 N ⁡ F
48 9 12 47 3eqtr3d ⊢ D ∈ Fin ∧ F ∈ P → N ⁡ F -1 = 1 N ⁡ F
49 fvex ⊢ N ⁡ F ∈ V
50 49 elpr ⊢ N ⁡ F ∈ 1 − 1 ↔ N ⁡ F = 1 ∨ N ⁡ F = − 1
51 1div1e1 ⊢ 1 1 = 1
52 oveq2 ⊢ N ⁡ F = 1 → 1 N ⁡ F = 1 1
53 id ⊢ N ⁡ F = 1 → N ⁡ F = 1
54 51 52 53 3eqtr4a ⊢ N ⁡ F = 1 → 1 N ⁡ F = N ⁡ F
55 divneg2 ⊢ 1 ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ≠ 0 → − 1 1 = 1 − 1
56 21 21 22 55 mp3an ⊢ − 1 1 = 1 − 1
57 51 negeqi ⊢ − 1 1 = − 1
58 56 57 eqtr3i ⊢ 1 − 1 = − 1
59 oveq2 ⊢ N ⁡ F = − 1 → 1 N ⁡ F = 1 − 1
60 id ⊢ N ⁡ F = − 1 → N ⁡ F = − 1
61 58 59 60 3eqtr4a ⊢ N ⁡ F = − 1 → 1 N ⁡ F = N ⁡ F
62 54 61 jaoi ⊢ N ⁡ F = 1 ∨ N ⁡ F = − 1 → 1 N ⁡ F = N ⁡ F
63 50 62 sylbi ⊢ N ⁡ F ∈ 1 − 1 → 1 N ⁡ F = N ⁡ F
64 18 63 syl ⊢ D ∈ Fin ∧ F ∈ P → 1 N ⁡ F = N ⁡ F
65 48 64 eqtrd ⊢ D ∈ Fin ∧ F ∈ P → N ⁡ F -1 = N ⁡ F