mulgassr

Description: Reversed product of group multiples. (Contributed by Paul Chapman, 17-Apr-2009) (Revised by AV, 30-Aug-2021)

	Ref	Expression
Hypotheses	mulgass.b	$⊢ B = {Base}_{G}$
	mulgass.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
Assertion	mulgassr	$⊢ (G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \to N \cdot M \underset{˙}{\cdot} X = M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X)$

Step	Hyp	Ref	Expression
1		mulgass.b	$⊢ B = {Base}_{G}$
2		mulgass.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
3		zcn	$⊢ N \in ℤ \to N \in ℂ$
4	3	3ad2ant2	$⊢ (M \in ℤ \land N \in ℤ \land X \in B) \to N \in ℂ$
5		zcn	$⊢ M \in ℤ \to M \in ℂ$
6	5	3ad2ant1	$⊢ (M \in ℤ \land N \in ℤ \land X \in B) \to M \in ℂ$
7	4 6	mulcomd	$⊢ (M \in ℤ \land N \in ℤ \land X \in B) \to N \cdot M = M \cdot N$
8	7	adantl	$⊢ (G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \to N \cdot M = M \cdot N$
9	8	oveq1d	$⊢ (G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \to N \cdot M \underset{˙}{\cdot} X = M \cdot N \underset{˙}{\cdot} X$
10	1 2	mulgass	$⊢ (G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \to M \cdot N \underset{˙}{\cdot} X = M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X)$
11	9 10	eqtrd	$⊢ (G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \to N \cdot M \underset{˙}{\cdot} X = M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X)$

Metamath Proof Explorer