This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )