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 · ˙ = G
Assertion mulgassr G Grp M N X B N M · ˙ X = M · ˙ N · ˙ X

Proof

Step Hyp Ref Expression
1 mulgass.b B = Base G
2 mulgass.t · ˙ = G
3 zcn N N
4 3 3ad2ant2 M N X B N
5 zcn M M
6 5 3ad2ant1 M N X B M
7 4 6 mulcomd M N X B N M = M N
8 7 adantl G Grp M N X B N M = M N
9 8 oveq1d G Grp M N X B N M · ˙ X = M N · ˙ X
10 1 2 mulgass G Grp M N X B M N · ˙ X = M · ˙ N · ˙ X
11 9 10 eqtrd G Grp M N X B N M · ˙ X = M · ˙ N · ˙ X