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 ) ) )