Metamath Proof Explorer

Theorem psgneldm2i

Description: A sequence of transpositions describes a finitary permutation. (Contributed by Stefan O'Rear, 28-Aug-2015)

Ref Expression
Hypotheses psgnval.g ⊢ G = SymGrp ⁡ D
psgnval.t ⊢ T = ran ⁡ pmTrsp ⁡ D
psgnval.n ⊢ N = pmSgn ⁡ D
Assertion psgneldm2i ⊢ D ∈ V ∧ W ∈ Word T → ∑ G W ∈ dom ⁡ N

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 ⊢ ∑ G W = ∑ G W
5 oveq2 ⊢ w = W → ∑ G w = ∑ G W
6 5 rspceeqv ⊢ W ∈ Word T ∧ ∑ G W = ∑ G W → ∃ w ∈ Word T ∑ G W = ∑ G w
7 4 6 mpan2 ⊢ W ∈ Word T → ∃ w ∈ Word T ∑ G W = ∑ G w
8 1 2 3 psgneldm2 ⊢ D ∈ V → ∑ G W ∈ dom ⁡ N ↔ ∃ w ∈ Word T ∑ G W = ∑ G w
9 8 biimpar ⊢ D ∈ V ∧ ∃ w ∈ Word T ∑ G W = ∑ G w → ∑ G W ∈ dom ⁡ N
10 7 9 sylan2 ⊢ D ∈ V ∧ W ∈ Word T → ∑ G W ∈ dom ⁡ N