Theorem psgnid

Description: Permutation sign of the identity. (Contributed by Thierry Arnoux, 21-Aug-2020)

	Ref	Expression
Hypothesis	psgnid.s	$$⊢S=\mathrm{pmSgn}\left(D\right)$$
Assertion	psgnid	$$⊢D\in \mathrm{Fin}\to S\left({\mathrm{I}\upharpoonright }_D\right)=1$$

Proof

Step	Hyp	Ref	Expression
1		psgnid.s	$$⊢S=\mathrm{pmSgn}\left(D\right)$$
2		eqid	$$⊢\mathrm{SymGrp}\left(D\right)=\mathrm{SymGrp}\left(D\right)$$
3	2	symgid	$$⊢D\in \mathrm{Fin}\to {\mathrm{I}\upharpoonright }_D=0_{\mathrm{SymGrp}\left(D\right)}$$
4	3	fveq2d	$$⊢D\in \mathrm{Fin}\to S\left({\mathrm{I}\upharpoonright }_D\right)=S\left(0_{\mathrm{SymGrp}\left(D\right)}\right)$$
5		eqid	$$⊢{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left\{1,-1\right\}={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left\{1,-1\right\}$$
6	2 1 5	psgnghm2	$$⊢D\in \mathrm{Fin}\to S\in \left(\mathrm{SymGrp}\left(D\right)\mathrm{GrpHom}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left\{1,-1\right\}\right)\right)$$
7		eqid	$$⊢0_{\mathrm{SymGrp}\left(D\right)}=0_{\mathrm{SymGrp}\left(D\right)}$$
8		cnring	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}$$
9		eqid	$$⊢{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}$$
10	9	ringmgp	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}\to {\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\in \mathrm{Mnd}$$
11	8 10	ax-mp	$$⊢{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\in \mathrm{Mnd}$$
12		1ex	$$⊢1\in \mathrm{V}$$
13	12	prid1	$$⊢1\in \left\{1,-1\right\}$$
14		ax-1cn	$$⊢1\in ℂ$$
15		neg1cn	$$⊢-1\in ℂ$$
16		prssi	$$⊢\left(1\in ℂ\wedge -1\in ℂ\right)\to \left\{1,-1\right\}\subseteq ℂ$$
17	14 15 16	mp2an	$$⊢\left\{1,-1\right\}\subseteq ℂ$$
18		cnfldbas	$$⊢ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
19	9 18	mgpbas	$$⊢ℂ={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}$$
20		cnfld1	$$⊢1=1_{{ℂ}_{\mathrm{fld}}}$$
21	9 20	ringidval	$$⊢1=0_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}$$
22	5 19 21	ress0g	$$⊢\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\in \mathrm{Mnd}\wedge 1\in \left\{1,-1\right\}\wedge \left\{1,-1\right\}\subseteq ℂ\right)\to 1=0_{\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left\{1,-1\right\}\right)}$$
23	11 13 17 22	mp3an	$$⊢1=0_{\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left\{1,-1\right\}\right)}$$
24	7 23	ghmid	$$⊢S\in \left(\mathrm{SymGrp}\left(D\right)\mathrm{GrpHom}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left\{1,-1\right\}\right)\right)\to S\left(0_{\mathrm{SymGrp}\left(D\right)}\right)=1$$
25	6 24	syl	$$⊢D\in \mathrm{Fin}\to S\left(0_{\mathrm{SymGrp}\left(D\right)}\right)=1$$
26	4 25	eqtrd	$$⊢D\in \mathrm{Fin}\to S\left({\mathrm{I}\upharpoonright }_D\right)=1$$