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 𝑁 )