Theorem gsmtrcl

Description: The group sum of transpositions of a finite set is a permutation, see also psgneldm2i . (Contributed by AV, 19-Jan-2019)

	Ref	Expression
Hypotheses	gsmtrcl.s	⊢ 𝑆 = ( SymGrp ‘ 𝑁 )
	gsmtrcl.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
	gsmtrcl.t	⊢ 𝑇 = ran ( pmTrsp ‘ 𝑁 )
Assertion	gsmtrcl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑊 ∈ Word 𝑇 ) → ( 𝑆 Σg 𝑊 ) ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		gsmtrcl.s	⊢ 𝑆 = ( SymGrp ‘ 𝑁 )
2		gsmtrcl.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
3		gsmtrcl.t	⊢ 𝑇 = ran ( pmTrsp ‘ 𝑁 )
4		eqid	⊢ ( pmSgn ‘ 𝑁 ) = ( pmSgn ‘ 𝑁 )
5	1 3 4	psgneldm2i	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑊 ∈ Word 𝑇 ) → ( 𝑆 Σg 𝑊 ) ∈ dom ( pmSgn ‘ 𝑁 ) )
6	1 4 2	psgneldm	⊢ ( ( 𝑆 Σg 𝑊 ) ∈ dom ( pmSgn ‘ 𝑁 ) ↔ ( ( 𝑆 Σg 𝑊 ) ∈ 𝐵 ∧ dom ( ( 𝑆 Σg 𝑊 ) ∖ I ) ∈ Fin ) )
7		ax-1	⊢ ( ( 𝑆 Σg 𝑊 ) ∈ 𝐵 → ( ( 𝑁 ∈ Fin ∧ 𝑊 ∈ Word 𝑇 ) → ( 𝑆 Σg 𝑊 ) ∈ 𝐵 ) )
8	7	adantr	⊢ ( ( ( 𝑆 Σg 𝑊 ) ∈ 𝐵 ∧ dom ( ( 𝑆 Σg 𝑊 ) ∖ I ) ∈ Fin ) → ( ( 𝑁 ∈ Fin ∧ 𝑊 ∈ Word 𝑇 ) → ( 𝑆 Σg 𝑊 ) ∈ 𝐵 ) )
9	6 8	sylbi	⊢ ( ( 𝑆 Σg 𝑊 ) ∈ dom ( pmSgn ‘ 𝑁 ) → ( ( 𝑁 ∈ Fin ∧ 𝑊 ∈ Word 𝑇 ) → ( 𝑆 Σg 𝑊 ) ∈ 𝐵 ) )
10	5 9	mpcom	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑊 ∈ Word 𝑇 ) → ( 𝑆 Σg 𝑊 ) ∈ 𝐵 )