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

Metamath Proof Explorer

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 ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑁 · 𝑀 ) · 𝑋 ) = ( 𝑀 · ( 𝑁 · 𝑋 ) ) )