Theorem psgnpmtr

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

	Ref	Expression
Hypotheses	psgnval.g	⊢ 𝐺 = ( SymGrp ‘ 𝐷 )
	psgnval.t	⊢ 𝑇 = ran ( pmTrsp ‘ 𝐷 )
	psgnval.n	⊢ 𝑁 = ( pmSgn ‘ 𝐷 )
Assertion	psgnpmtr	⊢ ( 𝑃 ∈ 𝑇 → ( 𝑁 ‘ 𝑃 ) = - 1 )

Proof

Step	Hyp	Ref	Expression
1		psgnval.g	⊢ 𝐺 = ( SymGrp ‘ 𝐷 )
2		psgnval.t	⊢ 𝑇 = ran ( pmTrsp ‘ 𝐷 )
3		psgnval.n	⊢ 𝑁 = ( pmSgn ‘ 𝐷 )
4		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
5	2 1 4	symgtrf	⊢ 𝑇 ⊆ ( Base ‘ 𝐺 )
6	5	sseli	⊢ ( 𝑃 ∈ 𝑇 → 𝑃 ∈ ( Base ‘ 𝐺 ) )
7	4	gsumws1	⊢ ( 𝑃 ∈ ( Base ‘ 𝐺 ) → ( 𝐺 Σg ⟨“ 𝑃 ”⟩ ) = 𝑃 )
8	6 7	syl	⊢ ( 𝑃 ∈ 𝑇 → ( 𝐺 Σg ⟨“ 𝑃 ”⟩ ) = 𝑃 )
9	8	fveq2d	⊢ ( 𝑃 ∈ 𝑇 → ( 𝑁 ‘ ( 𝐺 Σg ⟨“ 𝑃 ”⟩ ) ) = ( 𝑁 ‘ 𝑃 ) )
10	1 4	elbasfv	⊢ ( 𝑃 ∈ ( Base ‘ 𝐺 ) → 𝐷 ∈ V )
11	6 10	syl	⊢ ( 𝑃 ∈ 𝑇 → 𝐷 ∈ V )
12		s1cl	⊢ ( 𝑃 ∈ 𝑇 → ⟨“ 𝑃 ”⟩ ∈ Word 𝑇 )
13	1 2 3	psgnvalii	⊢ ( ( 𝐷 ∈ V ∧ ⟨“ 𝑃 ”⟩ ∈ Word 𝑇 ) → ( 𝑁 ‘ ( 𝐺 Σg ⟨“ 𝑃 ”⟩ ) ) = ( - 1 ↑ ( ♯ ‘ ⟨“ 𝑃 ”⟩ ) ) )
14	11 12 13	syl2anc	⊢ ( 𝑃 ∈ 𝑇 → ( 𝑁 ‘ ( 𝐺 Σg ⟨“ 𝑃 ”⟩ ) ) = ( - 1 ↑ ( ♯ ‘ ⟨“ 𝑃 ”⟩ ) ) )
15		s1len	⊢ ( ♯ ‘ ⟨“ 𝑃 ”⟩ ) = 1
16	15	oveq2i	⊢ ( - 1 ↑ ( ♯ ‘ ⟨“ 𝑃 ”⟩ ) ) = ( - 1 ↑ 1 )
17		neg1cn	⊢ - 1 ∈ ℂ
18		exp1	⊢ ( - 1 ∈ ℂ → ( - 1 ↑ 1 ) = - 1 )
19	17 18	ax-mp	⊢ ( - 1 ↑ 1 ) = - 1
20	16 19	eqtri	⊢ ( - 1 ↑ ( ♯ ‘ ⟨“ 𝑃 ”⟩ ) ) = - 1
21	14 20	eqtrdi	⊢ ( 𝑃 ∈ 𝑇 → ( 𝑁 ‘ ( 𝐺 Σg ⟨“ 𝑃 ”⟩ ) ) = - 1 )
22	9 21	eqtr3d	⊢ ( 𝑃 ∈ 𝑇 → ( 𝑁 ‘ 𝑃 ) = - 1 )