Theorem 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	⊢ 𝐵 = ( Base ‘ 𝐺 )
	mulgass.t	⊢ · = ( .g ‘ 𝐺 )
Assertion	mulgassr	⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑁 · 𝑀 ) · 𝑋 ) = ( 𝑀 · ( 𝑁 · 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		mulgass.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		mulgass.t	⊢ · = ( .g ‘ 𝐺 )
3		zcn	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
4	3	3ad2ant2	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → 𝑁 ∈ ℂ )
5		zcn	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ )
6	5	3ad2ant1	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → 𝑀 ∈ ℂ )
7	4 6	mulcomd	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 · 𝑀 ) = ( 𝑀 · 𝑁 ) )
8	7	adantl	⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) → ( 𝑁 · 𝑀 ) = ( 𝑀 · 𝑁 ) )
9	8	oveq1d	⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑁 · 𝑀 ) · 𝑋 ) = ( ( 𝑀 · 𝑁 ) · 𝑋 ) )
10	1 2	mulgass	⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑀 · 𝑁 ) · 𝑋 ) = ( 𝑀 · ( 𝑁 · 𝑋 ) ) )
11	9 10	eqtrd	⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑁 · 𝑀 ) · 𝑋 ) = ( 𝑀 · ( 𝑁 · 𝑋 ) ) )