Theorem psgnprfval2

Description: The permutation sign of the transposition for a pair. (Contributed by AV, 10-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	psgnprfval2	$$⊢N\left(\left\{⟨1,2⟩,⟨2,1⟩\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⟩,⟨2,1⟩\right\}\in \mathrm{V}$$
7	6	snid	$$⊢\left\{⟨1,2⟩,⟨2,1⟩\right\}\in \left\{\left\{⟨1,2⟩,⟨2,1⟩\right\}\right\}$$
8	1	fveq2i	$$⊢\mathrm{pmTrsp}\left(D\right)=\mathrm{pmTrsp}\left(\left\{1,2\right\}\right)$$
9	8	rneqi	$$⊢\mathrm{ran}\mathrm{pmTrsp}\left(D\right)=\mathrm{ran}\mathrm{pmTrsp}\left(\left\{1,2\right\}\right)$$
10		pmtrprfvalrn	$$⊢\mathrm{ran}\mathrm{pmTrsp}\left(\left\{1,2\right\}\right)=\left\{\left\{⟨1,2⟩,⟨2,1⟩\right\}\right\}$$
11	9 10	eqtri	$$⊢\mathrm{ran}\mathrm{pmTrsp}\left(D\right)=\left\{\left\{⟨1,2⟩,⟨2,1⟩\right\}\right\}$$
12	7 11	eleqtrri	$$⊢\left\{⟨1,2⟩,⟨2,1⟩\right\}\in \mathrm{ran}\mathrm{pmTrsp}\left(D\right)$$
13	12 4	eleqtrri	$$⊢\left\{⟨1,2⟩,⟨2,1⟩\right\}\in T$$
14	2 4 5	psgnpmtr	$$⊢\left\{⟨1,2⟩,⟨2,1⟩\right\}\in T\to N\left(\left\{⟨1,2⟩,⟨2,1⟩\right\}\right)=-1$$
15	13 14	ax-mp	$$⊢N\left(\left\{⟨1,2⟩,⟨2,1⟩\right\}\right)=-1$$