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 \in Fin \land W \in Word T) \to \sum_{S} W \in B$

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 \in Fin \land W \in Word T) \to \sum_{S} W \in dom pmSgn (N)$
6	1 4 2	psgneldm	$⊢ \sum_{S} W \in dom pmSgn (N) \leftrightarrow (\sum_{S} W \in B \land dom ((\sum_{S}, W) ∖ I) \in Fin)$
7		ax-1	$⊢ \sum_{S} W \in B \to ((N \in Fin \land W \in Word T) \to \sum_{S} W \in B)$
8	7	adantr	$⊢ (\sum_{S} W \in B \land dom ((\sum_{S}, W) ∖ I) \in Fin) \to ((N \in Fin \land W \in Word T) \to \sum_{S} W \in B)$
9	6 8	sylbi	$⊢ \sum_{S} W \in dom pmSgn (N) \to ((N \in Fin \land W \in Word T) \to \sum_{S} W \in B)$
10	5 9	mpcom	$⊢ (N \in Fin \land W \in Word T) \to \sum_{S} W \in B$

Metamath Proof Explorer