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

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 ⊢ 𝐺 = ( SymGrp ‘ 𝐷 )
psgnval.t ⊢ 𝑇 = ran ( pmTrsp ‘ 𝐷 )
psgnval.n ⊢ 𝑁 = ( pmSgn ‘ 𝐷 )
Assertion psgneldm2i ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇 ) → ( 𝐺 Σg 𝑊 ) ∈ dom 𝑁 )

Proof

Step Hyp Ref Expression
1 psgnval.g ⊢ 𝐺 = ( SymGrp ‘ 𝐷 )
2 psgnval.t ⊢ 𝑇 = ran ( pmTrsp ‘ 𝐷 )
3 psgnval.n ⊢ 𝑁 = ( pmSgn ‘ 𝐷 )
4 eqid ⊢ ( 𝐺 Σg 𝑊 ) = ( 𝐺 Σg 𝑊 )
5 oveq2 ⊢ ( 𝑤 = 𝑊 → ( 𝐺 Σg 𝑤 ) = ( 𝐺 Σg 𝑊 ) )
6 5 rspceeqv ⊢ ( ( 𝑊 ∈ Word 𝑇 ∧ ( 𝐺 Σg 𝑊 ) = ( 𝐺 Σg 𝑊 ) ) → ∃ 𝑤 ∈ Word 𝑇 ( 𝐺 Σg 𝑊 ) = ( 𝐺 Σg 𝑤 ) )
7 4 6 mpan2 ⊢ ( 𝑊 ∈ Word 𝑇 → ∃ 𝑤 ∈ Word 𝑇 ( 𝐺 Σg 𝑊 ) = ( 𝐺 Σg 𝑤 ) )
8 1 2 3 psgneldm2 ⊢ ( 𝐷 ∈ 𝑉 → ( ( 𝐺 Σg 𝑊 ) ∈ dom 𝑁 ↔ ∃ 𝑤 ∈ Word 𝑇 ( 𝐺 Σg 𝑊 ) = ( 𝐺 Σg 𝑤 ) ) )
9 8 biimpar ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ∃ 𝑤 ∈ Word 𝑇 ( 𝐺 Σg 𝑊 ) = ( 𝐺 Σg 𝑤 ) ) → ( 𝐺 Σg 𝑊 ) ∈ dom 𝑁 )
10 7 9 sylan2 ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇 ) → ( 𝐺 Σg 𝑊 ) ∈ dom 𝑁 )