Theorem psgnsn

Description: The permutation sign function for a singleton. (Contributed by AV, 6-Aug-2019)

	Ref	Expression
Hypotheses	psgnsn.0	$$⊢D=\left\{A\right\}$$
	psgnsn.g	$$⊢G=\mathrm{SymGrp}\left(D\right)$$
	psgnsn.b	$$⊢B={\mathrm{Base}}_G$$
	psgnsn.n	$$⊢N=\mathrm{pmSgn}\left(D\right)$$
Assertion	psgnsn	$$⊢\left(A\in V\wedge X\in B\right)\to N\left(X\right)=1$$

Proof

Step	Hyp	Ref	Expression
1		psgnsn.0	$$⊢D=\left\{A\right\}$$
2		psgnsn.g	$$⊢G=\mathrm{SymGrp}\left(D\right)$$
3		psgnsn.b	$$⊢B={\mathrm{Base}}_G$$
4		psgnsn.n	$$⊢N=\mathrm{pmSgn}\left(D\right)$$
5		eqid	$$⊢0_G=0_G$$
6	5	gsum0	$$⊢{\sum }_G\varnothing =0_G$$
7	2 3 1	symg1bas	$$⊢A\in V\to B=\left\{\left\{⟨A,A⟩\right\}\right\}$$
8	7	eleq2d	$$⊢A\in V\to \left(X\in B\leftrightarrow X\in \left\{\left\{⟨A,A⟩\right\}\right\}\right)$$
9	8	biimpa	$$⊢\left(A\in V\wedge X\in B\right)\to X\in \left\{\left\{⟨A,A⟩\right\}\right\}$$
10		elsni	$$⊢X\in \left\{\left\{⟨A,A⟩\right\}\right\}\to X=\left\{⟨A,A⟩\right\}$$
11	1	reseq2i	$$⊢{\mathrm{I}\upharpoonright }_D={\mathrm{I}\upharpoonright }_{\left\{A\right\}}$$
12		snex	$$⊢\left\{A\right\}\in \mathrm{V}$$
13	12	snid	$$⊢\left\{A\right\}\in \left\{\left\{A\right\}\right\}$$
14	1 13	eqeltri	$$⊢D\in \left\{\left\{A\right\}\right\}$$
15	2	symgid	$$⊢D\in \left\{\left\{A\right\}\right\}\to {\mathrm{I}\upharpoonright }_D=0_G$$
16	14 15	mp1i	$$⊢A\in V\to {\mathrm{I}\upharpoonright }_D=0_G$$
17		restidsing	$$⊢{\mathrm{I}\upharpoonright }_{\left\{A\right\}}=\left\{A\right\}\times \left\{A\right\}$$
18		xpsng	$$⊢\left(A\in V\wedge A\in V\right)\to \left\{A\right\}\times \left\{A\right\}=\left\{⟨A,A⟩\right\}$$
19	18	anidms	$$⊢A\in V\to \left\{A\right\}\times \left\{A\right\}=\left\{⟨A,A⟩\right\}$$
20	17 19	eqtrid	$$⊢A\in V\to {\mathrm{I}\upharpoonright }_{\left\{A\right\}}=\left\{⟨A,A⟩\right\}$$
21	11 16 20	3eqtr3a	$$⊢A\in V\to 0_G=\left\{⟨A,A⟩\right\}$$
22	21	adantr	$$⊢\left(A\in V\wedge X\in B\right)\to 0_G=\left\{⟨A,A⟩\right\}$$
23		id	$$⊢\left\{⟨A,A⟩\right\}=X\to \left\{⟨A,A⟩\right\}=X$$
24	23	eqcoms	$$⊢X=\left\{⟨A,A⟩\right\}\to \left\{⟨A,A⟩\right\}=X$$
25	22 24	sylan9eqr	$$⊢\left(X=\left\{⟨A,A⟩\right\}\wedge \left(A\in V\wedge X\in B\right)\right)\to 0_G=X$$
26	25	ex	$$⊢X=\left\{⟨A,A⟩\right\}\to \left(\left(A\in V\wedge X\in B\right)\to 0_G=X\right)$$
27	10 26	syl	$$⊢X\in \left\{\left\{⟨A,A⟩\right\}\right\}\to \left(\left(A\in V\wedge X\in B\right)\to 0_G=X\right)$$
28	9 27	mpcom	$$⊢\left(A\in V\wedge X\in B\right)\to 0_G=X$$
29	6 28	eqtr2id	$$⊢\left(A\in V\wedge X\in B\right)\to X={\sum }_G\varnothing$$
30	29	fveq2d	$$⊢\left(A\in V\wedge X\in B\right)\to N\left(X\right)=N\left({\sum }_G\varnothing \right)$$
31	1 12	eqeltri	$$⊢D\in \mathrm{V}$$
32		wrd0	$$⊢\varnothing \in \mathrm{Word}\varnothing$$
33	31 32	pm3.2i	$$⊢\left(D\in \mathrm{V}\wedge \varnothing \in \mathrm{Word}\varnothing \right)$$
34	1	fveq2i	$$⊢\mathrm{pmTrsp}\left(D\right)=\mathrm{pmTrsp}\left(\left\{A\right\}\right)$$
35		pmtrsn	$$⊢\mathrm{pmTrsp}\left(\left\{A\right\}\right)=\varnothing$$
36	34 35	eqtri	$$⊢\mathrm{pmTrsp}\left(D\right)=\varnothing$$
37	36	rneqi	$$⊢\mathrm{ran}\mathrm{pmTrsp}\left(D\right)=\mathrm{ran}\varnothing$$
38		rn0	$$⊢\mathrm{ran}\varnothing =\varnothing$$
39	37 38	eqtr2i	$$⊢\varnothing =\mathrm{ran}\mathrm{pmTrsp}\left(D\right)$$
40	2 39 4	psgnvalii	$$⊢\left(D\in \mathrm{V}\wedge \varnothing \in \mathrm{Word}\varnothing \right)\to N\left({\sum }_G\varnothing \right)={\left(-1\right)}^{\left|\varnothing \right|}$$
41	33 40	mp1i	$$⊢\left(A\in V\wedge X\in B\right)\to N\left({\sum }_G\varnothing \right)={\left(-1\right)}^{\left|\varnothing \right|}$$
42		hash0	$$⊢\left|\varnothing \right|=0$$
43	42	oveq2i	$$⊢{\left(-1\right)}^{\left|\varnothing \right|}={\left(-1\right)}^0$$
44		neg1cn	$$⊢-1\in ℂ$$
45		exp0	$$⊢-1\in ℂ\to {\left(-1\right)}^0=1$$
46	44 45	ax-mp	$$⊢{\left(-1\right)}^0=1$$
47	43 46	eqtri	$$⊢{\left(-1\right)}^{\left|\varnothing \right|}=1$$
48	47	a1i	$$⊢\left(A\in V\wedge X\in B\right)\to {\left(-1\right)}^{\left|\varnothing \right|}=1$$
49	30 41 48	3eqtrd	$$⊢\left(A\in V\wedge X\in B\right)\to N\left(X\right)=1$$