# 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}=\mathrm{SymGrp}\left({D}\right)$
psgninv.n ${⊢}{N}=\mathrm{pmSgn}\left({D}\right)$
psgninv.p ${⊢}{P}={\mathrm{Base}}_{{S}}$
Assertion psgninv ${⊢}\left({D}\in \mathrm{Fin}\wedge {F}\in {P}\right)\to {N}\left({{F}}^{-1}\right)={N}\left({F}\right)$

### Proof

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