Theorem psgnprfval

Description: The permutation sign function 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	psgnprfval	$$⊢X\in B\to N\left(X\right)=\left(\iota s|\exists w\in \mathrm{Word}T\left(X={\sum }_{G}w\wedge s={\left(-1\right)}^{\left|w\right|}\right)\right)$$

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		id	$$⊢X\in B\to X\in B$$
7		elpri	$$⊢X\in \left\{\left\{⟨1,1⟩,⟨2,2⟩\right\},\left\{⟨1,2⟩,⟨2,1⟩\right\}\right\}\to \left(X=\left\{⟨1,1⟩,⟨2,2⟩\right\}\vee X=\left\{⟨1,2⟩,⟨2,1⟩\right\}\right)$$
8		prfi	$$⊢\left\{⟨1,1⟩,⟨2,2⟩\right\}\in \mathrm{Fin}$$
9		eleq1	$$⊢X=\left\{⟨1,1⟩,⟨2,2⟩\right\}\to \left(X\in \mathrm{Fin}\leftrightarrow \left\{⟨1,1⟩,⟨2,2⟩\right\}\in \mathrm{Fin}\right)$$
10	8 9	mpbiri	$$⊢X=\left\{⟨1,1⟩,⟨2,2⟩\right\}\to X\in \mathrm{Fin}$$
11		prfi	$$⊢\left\{⟨1,2⟩,⟨2,1⟩\right\}\in \mathrm{Fin}$$
12		eleq1	$$⊢X=\left\{⟨1,2⟩,⟨2,1⟩\right\}\to \left(X\in \mathrm{Fin}\leftrightarrow \left\{⟨1,2⟩,⟨2,1⟩\right\}\in \mathrm{Fin}\right)$$
13	11 12	mpbiri	$$⊢X=\left\{⟨1,2⟩,⟨2,1⟩\right\}\to X\in \mathrm{Fin}$$
14	10 13	jaoi	$$⊢\left(X=\left\{⟨1,1⟩,⟨2,2⟩\right\}\vee X=\left\{⟨1,2⟩,⟨2,1⟩\right\}\right)\to X\in \mathrm{Fin}$$
15		diffi	$$⊢X\in \mathrm{Fin}\to X\setminus \mathrm{I}\in \mathrm{Fin}$$
16	14 15	syl	$$⊢\left(X=\left\{⟨1,1⟩,⟨2,2⟩\right\}\vee X=\left\{⟨1,2⟩,⟨2,1⟩\right\}\right)\to X\setminus \mathrm{I}\in \mathrm{Fin}$$
17		dmfi	$$⊢X\setminus \mathrm{I}\in \mathrm{Fin}\to \mathrm{dom}\left(X\setminus \mathrm{I}\right)\in \mathrm{Fin}$$
18	7 16 17	3syl	$$⊢X\in \left\{\left\{⟨1,1⟩,⟨2,2⟩\right\},\left\{⟨1,2⟩,⟨2,1⟩\right\}\right\}\to \mathrm{dom}\left(X\setminus \mathrm{I}\right)\in \mathrm{Fin}$$
19		1ex	$$⊢1\in \mathrm{V}$$
20		2nn	$$⊢2\in \mathbb{N}$$
21	2 3 1	symg2bas	$$⊢\left(1\in \mathrm{V}\wedge 2\in \mathbb{N}\right)\to B=\left\{\left\{⟨1,1⟩,⟨2,2⟩\right\},\left\{⟨1,2⟩,⟨2,1⟩\right\}\right\}$$
22	19 20 21	mp2an	$$⊢B=\left\{\left\{⟨1,1⟩,⟨2,2⟩\right\},\left\{⟨1,2⟩,⟨2,1⟩\right\}\right\}$$
23	18 22	eleq2s	$$⊢X\in B\to \mathrm{dom}\left(X\setminus \mathrm{I}\right)\in \mathrm{Fin}$$
24	2 5 3	psgneldm	$$⊢X\in \mathrm{dom}N\leftrightarrow \left(X\in B\wedge \mathrm{dom}\left(X\setminus \mathrm{I}\right)\in \mathrm{Fin}\right)$$
25	6 23 24	sylanbrc	$$⊢X\in B\to X\in \mathrm{dom}N$$
26	2 4 5	psgnval	$$⊢X\in \mathrm{dom}N\to N\left(X\right)=\left(\iota s|\exists w\in \mathrm{Word}T\left(X={\sum }_{G}w\wedge s={\left(-1\right)}^{\left|w\right|}\right)\right)$$
27	25 26	syl	$$⊢X\in B\to N\left(X\right)=\left(\iota s|\exists w\in \mathrm{Word}T\left(X={\sum }_{G}w\wedge s={\left(-1\right)}^{\left|w\right|}\right)\right)$$
28	6 27	syl	$$⊢X\in B\to N\left(X\right)=\left(\iota s|\exists w\in \mathrm{Word}T\left(X={\sum }_{G}w\wedge s={\left(-1\right)}^{\left|w\right|}\right)\right)$$