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

Metamath Proof Explorer

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 𝑊 ) ∈ 𝐵 )