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 | ||
rngass.t | |||
Assertion | rngass |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rngass.b | ||
2 | rngass.t | ||
3 | eqid | ||
4 | 3 | rngmgp | |
5 | 3 1 | mgpbas | |
6 | 3 2 | mgpplusg | |
7 | 5 6 | sgrpass | |
8 | 4 7 | sylan |