Metamath Proof Explorer


Theorem rngass

Description: Associative law for the multiplication operation of a non-unital ring. (Contributed by NM, 27-Aug-2011) (Revised by AV, 13-Feb-2025)

Ref Expression
Hypotheses rngass.b B = Base R
rngass.t · ˙ = R
Assertion rngass R Rng X B Y B Z B X · ˙ Y · ˙ Z = X · ˙ Y · ˙ Z

Proof

Step Hyp Ref Expression
1 rngass.b B = Base R
2 rngass.t · ˙ = R
3 eqid mulGrp R = mulGrp R
4 3 rngmgp R Rng mulGrp R Smgrp
5 3 1 mgpbas B = Base mulGrp R
6 3 2 mgpplusg · ˙ = + mulGrp R
7 5 6 sgrpass mulGrp R Smgrp X B Y B Z B X · ˙ Y · ˙ Z = X · ˙ Y · ˙ Z
8 4 7 sylan R Rng X B Y B Z B X · ˙ Y · ˙ Z = X · ˙ Y · ˙ Z