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 ⊢ G = SymGrp ⁡ D
psgnval.t ⊢ T = ran ⁡ pmTrsp ⁡ D
psgnval.n ⊢ N = pmSgn ⁡ D
Assertion psgnpmtr ⊢ P ∈ T → N ⁡ P = − 1

Proof

Step Hyp Ref Expression
1 psgnval.g ⊢ G = SymGrp ⁡ D
2 psgnval.t ⊢ T = ran ⁡ pmTrsp ⁡ D
3 psgnval.n ⊢ N = pmSgn ⁡ D
4 eqid ⊢ Base G = Base G
5 2 1 4 symgtrf ⊢ T ⊆ Base G
6 5 sseli ⊢ P ∈ T → P ∈ Base G
7 4 gsumws1 ⊢ P ∈ Base G → ∑ G ⟨“ P ”⟩ = P
8 6 7 syl ⊢ P ∈ T → ∑ G ⟨“ P ”⟩ = P
9 8 fveq2d ⊢ P ∈ T → N ⁡ ∑ G ⟨“ P ”⟩ = N ⁡ P
10 1 4 elbasfv ⊢ P ∈ Base G → D ∈ V
11 6 10 syl ⊢ P ∈ T → D ∈ V
12 s1cl ⊢ P ∈ T → ⟨“ P ”⟩ ∈ Word T
13 1 2 3 psgnvalii ⊢ D ∈ V ∧ ⟨“ P ”⟩ ∈ Word T → N ⁡ ∑ G ⟨“ P ”⟩ = − 1 ⟨“ P ”⟩
14 11 12 13 syl2anc ⊢ P ∈ T → N ⁡ ∑ G ⟨“ P ”⟩ = − 1 ⟨“ P ”⟩
15 s1len ⊢ ⟨“ P ”⟩ = 1
16 15 oveq2i ⊢ − 1 ⟨“ P ”⟩ = − 1 1
17 neg1cn ⊢ − 1 ∈ ℂ
18 exp1 ⊢ − 1 ∈ ℂ → − 1 1 = − 1
19 17 18 ax-mp ⊢ − 1 1 = − 1
20 16 19 eqtri ⊢ − 1 ⟨“ P ”⟩ = − 1
21 14 20 eqtrdi ⊢ P ∈ T → N ⁡ ∑ G ⟨“ P ”⟩ = − 1
22 9 21 eqtr3d ⊢ P ∈ T → N ⁡ P = − 1