Theorem psgnpmtr

Description: All transpositions are odd. (Contributed by Stefan O'Rear, 29-Aug-2015)

	Ref	Expression
Hypotheses	psgnval.g	$$⊢G=\mathrm{SymGrp}\left(D\right)$$
	psgnval.t	$$⊢T=\mathrm{ran}\mathrm{pmTrsp}\left(D\right)$$
	psgnval.n	$$⊢N=\mathrm{pmSgn}\left(D\right)$$
Assertion	psgnpmtr	$$⊢P\in T\to N\left(P\right)=-1$$

Proof

Step	Hyp	Ref	Expression
1		psgnval.g	$$⊢G=\mathrm{SymGrp}\left(D\right)$$
2		psgnval.t	$$⊢T=\mathrm{ran}\mathrm{pmTrsp}\left(D\right)$$
3		psgnval.n	$$⊢N=\mathrm{pmSgn}\left(D\right)$$
4		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
5	2 1 4	symgtrf	$$⊢T\subseteq {\mathrm{Base}}_G$$
6	5	sseli	$$⊢P\in T\to P\in {\mathrm{Base}}_G$$
7	4	gsumws1	$$⊢P\in {\mathrm{Base}}_G\to {\sum }_G⟨“P”⟩=P$$
8	6 7	syl	$$⊢P\in T\to {\sum }_G⟨“P”⟩=P$$
9	8	fveq2d	$$⊢P\in T\to N\left({\sum }_G⟨“P”⟩\right)=N\left(P\right)$$
10	1 4	elbasfv	$$⊢P\in {\mathrm{Base}}_G\to D\in \mathrm{V}$$
11	6 10	syl	$$⊢P\in T\to D\in \mathrm{V}$$
12		s1cl	$$⊢P\in T\to ⟨“P”⟩\in \mathrm{Word}T$$
13	1 2 3	psgnvalii	$$⊢\left(D\in \mathrm{V}\wedge ⟨“P”⟩\in \mathrm{Word}T\right)\to N\left({\sum }_G⟨“P”⟩\right)={\left(-1\right)}^{\left|⟨“P”⟩\right|}$$
14	11 12 13	syl2anc	$$⊢P\in T\to N\left({\sum }_G⟨“P”⟩\right)={\left(-1\right)}^{\left|⟨“P”⟩\right|}$$
15		s1len	$$⊢\left|⟨“P”⟩\right|=1$$
16	15	oveq2i	$$⊢{\left(-1\right)}^{\left|⟨“P”⟩\right|}={\left(-1\right)}^1$$
17		neg1cn	$$⊢-1\in ℂ$$
18		exp1	$$⊢-1\in ℂ\to {\left(-1\right)}^1=-1$$
19	17 18	ax-mp	$$⊢{\left(-1\right)}^1=-1$$
20	16 19	eqtri	$$⊢{\left(-1\right)}^{\left|⟨“P”⟩\right|}=-1$$
21	14 20	eqtrdi	$$⊢P\in T\to N\left({\sum }_G⟨“P”⟩\right)=-1$$
22	9 21	eqtr3d	$$⊢P\in T\to N\left(P\right)=-1$$