Theorem psgnprfval1

Description: The permutation sign of the identity for a pair. (Contributed by AV, 11-Dec-2018)

	Ref	Expression
Hypotheses	psgnprfval.0	$$⊢D=\left\{1,2\right\}$$
	psgnprfval.g	$$⊢G=\mathrm{SymGrp}\left(D\right)$$
	psgnprfval.b	$$⊢B={\mathrm{Base}}_G$$
	psgnprfval.t	$$⊢T=\mathrm{ran}\mathrm{pmTrsp}\left(D\right)$$
	psgnprfval.n	$$⊢N=\mathrm{pmSgn}\left(D\right)$$
Assertion	psgnprfval1	$$⊢N\left(\left\{⟨1,1⟩,⟨2,2⟩\right\}\right)=1$$

Proof

Step	Hyp	Ref	Expression
1		psgnprfval.0	$$⊢D=\left\{1,2\right\}$$
2		psgnprfval.g	$$⊢G=\mathrm{SymGrp}\left(D\right)$$
3		psgnprfval.b	$$⊢B={\mathrm{Base}}_G$$
4		psgnprfval.t	$$⊢T=\mathrm{ran}\mathrm{pmTrsp}\left(D\right)$$
5		psgnprfval.n	$$⊢N=\mathrm{pmSgn}\left(D\right)$$
6		prex	$$⊢\left\{1,2\right\}\in \mathrm{V}$$
7	1 6	eqeltri	$$⊢D\in \mathrm{V}$$
8	2	symgid	$$⊢D\in \mathrm{V}\to {\mathrm{I}\upharpoonright }_D=0_G$$
9	7 8	ax-mp	$$⊢{\mathrm{I}\upharpoonright }_D=0_G$$
10	9	gsum0	$$⊢{\sum }_G\varnothing ={\mathrm{I}\upharpoonright }_D$$
11		reseq2	$$⊢D=\left\{1,2\right\}\to {\mathrm{I}\upharpoonright }_D={\mathrm{I}\upharpoonright }_{\left\{1,2\right\}}$$
12		1ex	$$⊢1\in \mathrm{V}$$
13		2nn	$$⊢2\in \mathbb{N}$$
14		residpr	$$⊢\left(1\in \mathrm{V}\wedge 2\in \mathbb{N}\right)\to {\mathrm{I}\upharpoonright }_{\left\{1,2\right\}}=\left\{⟨1,1⟩,⟨2,2⟩\right\}$$
15	12 13 14	mp2an	$$⊢{\mathrm{I}\upharpoonright }_{\left\{1,2\right\}}=\left\{⟨1,1⟩,⟨2,2⟩\right\}$$
16	11 15	eqtrdi	$$⊢D=\left\{1,2\right\}\to {\mathrm{I}\upharpoonright }_D=\left\{⟨1,1⟩,⟨2,2⟩\right\}$$
17	1 16	ax-mp	$$⊢{\mathrm{I}\upharpoonright }_D=\left\{⟨1,1⟩,⟨2,2⟩\right\}$$
18	10 17	eqtr2i	$$⊢\left\{⟨1,1⟩,⟨2,2⟩\right\}={\sum }_G\varnothing$$
19	18	fveq2i	$$⊢N\left(\left\{⟨1,1⟩,⟨2,2⟩\right\}\right)=N\left({\sum }_G\varnothing \right)$$
20		wrd0	$$⊢\varnothing \in \mathrm{Word}T$$
21	2 4 5	psgnvalii	$$⊢\left(D\in \mathrm{V}\wedge \varnothing \in \mathrm{Word}T\right)\to N\left({\sum }_G\varnothing \right)={\left(-1\right)}^{\left|\varnothing \right|}$$
22	7 20 21	mp2an	$$⊢N\left({\sum }_G\varnothing \right)={\left(-1\right)}^{\left|\varnothing \right|}$$
23		hash0	$$⊢\left|\varnothing \right|=0$$
24	23	oveq2i	$$⊢{\left(-1\right)}^{\left|\varnothing \right|}={\left(-1\right)}^0$$
25		neg1cn	$$⊢-1\in ℂ$$
26		exp0	$$⊢-1\in ℂ\to {\left(-1\right)}^0=1$$
27	25 26	ax-mp	$$⊢{\left(-1\right)}^0=1$$
28	24 27	eqtri	$$⊢{\left(-1\right)}^{\left|\varnothing \right|}=1$$
29	19 22 28	3eqtri	$$⊢N\left(\left\{⟨1,1⟩,⟨2,2⟩\right\}\right)=1$$