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 
|- B = ( Base ` G )
mulgass.t 
|- .x. = ( .g ` G )
Assertion mulgassr 
|- ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> ( ( N x. M ) .x. X ) = ( M .x. ( N .x. X ) ) )

Proof

Step Hyp Ref Expression
1 mulgass.b 
 |-  B = ( Base ` G )
2 mulgass.t 
 |-  .x. = ( .g ` G )
3 zcn 
 |-  ( N e. ZZ -> N e. CC )
4 3 3ad2ant2 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ X e. B ) -> N e. CC )
5 zcn 
 |-  ( M e. ZZ -> M e. CC )
6 5 3ad2ant1 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ X e. B ) -> M e. CC )
7 4 6 mulcomd 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ X e. B ) -> ( N x. M ) = ( M x. N ) )
8 7 adantl 
 |-  ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> ( N x. M ) = ( M x. N ) )
9 8 oveq1d 
 |-  ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> ( ( N x. M ) .x. X ) = ( ( M x. N ) .x. X ) )
10 1 2 mulgass 
 |-  ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> ( ( M x. N ) .x. X ) = ( M .x. ( N .x. X ) ) )
11 9 10 eqtrd 
 |-  ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> ( ( N x. M ) .x. X ) = ( M .x. ( N .x. X ) ) )