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}}}{\upharpoonright }_{𝑠}\left\{1,-1\right\}={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\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}}}{\upharpoonright }_{𝑠}\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}}}{\upharpoonright }_{𝑠}\left\{1,-1\right\}\right)={inv}_g\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left\{1,-1\right\}\right)$$
8	3 6 7	ghminv	$$⊢\left(N\in \left(S\mathrm{GrpHom}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\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}}}{\upharpoonright }_{𝑠}\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}}}{\upharpoonright }_{𝑠}\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}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)$$
14	13	cnmsgnsubg	$$⊢\left\{1,-1\right\}\in \mathrm{SubGrp}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)\right)$$
15	4	cnmsgnbas	$$⊢\left\{1,-1\right\}={\mathrm{Base}}_{\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left\{1,-1\right\}\right)}$$
16	3 15	ghmf	$$⊢N\in \left(S\mathrm{GrpHom}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\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	ffvelcdmda	$$⊢\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)\leftrightarrow \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)\leftrightarrow \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}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)\right){\upharpoonright }_{𝑠}\left\{1,-1\right\}={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left\{1,-1\right\}$$
32	20 30 31	mp2an	$$⊢\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)\right){\upharpoonright }_{𝑠}\left\{1,-1\right\}={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left\{1,-1\right\}$$
33	32	eqcomi	$$⊢{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left\{1,-1\right\}=\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)\right){\upharpoonright }_{𝑠}\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}}}{\upharpoonright }_{𝑠}\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}}}{\upharpoonright }_{𝑠}\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}}}{\upharpoonright }_{𝑠}\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}}}{\upharpoonright }_{𝑠}\left\{1,-1\right\}\right)\left(N\left(F\right)\right)$$
42	30 18	sselid	$$⊢\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)\leftrightarrow \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}}}{\upharpoonright }_{𝑠}\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\}\leftrightarrow \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)$$