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 ⊢ S = SymGrp ⁡ N
gsmtrcl.b ⊢ B = Base S
gsmtrcl.t ⊢ T = ran ⁡ pmTrsp ⁡ N
Assertion gsmtrcl ⊢ N ∈ Fin ∧ W ∈ Word T → ∑ S W ∈ B

Proof

Step Hyp Ref Expression
1 gsmtrcl.s ⊢ S = SymGrp ⁡ N
2 gsmtrcl.b ⊢ B = Base S
3 gsmtrcl.t ⊢ T = ran ⁡ pmTrsp ⁡ N
4 eqid ⊢ pmSgn ⁡ N = pmSgn ⁡ N
5 1 3 4 psgneldm2i ⊢ N ∈ Fin ∧ W ∈ Word T → ∑ S W ∈ dom ⁡ pmSgn ⁡ N
6 1 4 2 psgneldm ⊢ ∑ S W ∈ dom ⁡ pmSgn ⁡ N ↔ ∑ S W ∈ B ∧ dom ⁡ ∑ S W ∖ I ∈ Fin
7 ax-1 ⊢ ∑ S W ∈ B → N ∈ Fin ∧ W ∈ Word T → ∑ S W ∈ B
8 7 adantr ⊢ ∑ S W ∈ B ∧ dom ⁡ ∑ S W ∖ I ∈ Fin → N ∈ Fin ∧ W ∈ Word T → ∑ S W ∈ B
9 6 8 sylbi ⊢ ∑ S W ∈ dom ⁡ pmSgn ⁡ N → N ∈ Fin ∧ W ∈ Word T → ∑ S W ∈ B
10 5 9 mpcom ⊢ N ∈ Fin ∧ W ∈ Word T → ∑ S W ∈ B