Metamath Proof Explorer


Theorem ringass

Description: Associative law for multiplication in a ring. (Contributed by NM, 27-Aug-2011) (Revised by Mario Carneiro, 6-Jan-2015)

Ref Expression
Hypotheses ringcl.b B = Base R
ringcl.t · ˙ = R
Assertion ringass R Ring X B Y B Z B X · ˙ Y · ˙ Z = X · ˙ Y · ˙ Z

Proof

Step Hyp Ref Expression
1 ringcl.b B = Base R
2 ringcl.t · ˙ = R
3 eqid mulGrp R = mulGrp R
4 3 ringmgp R Ring mulGrp R Mnd
5 3 1 mgpbas B = Base mulGrp R
6 3 2 mgpplusg · ˙ = + mulGrp R
7 5 6 mndass mulGrp R Mnd X B Y B Z B X · ˙ Y · ˙ Z = X · ˙ Y · ˙ Z
8 4 7 sylan R Ring X B Y B Z B X · ˙ Y · ˙ Z = X · ˙ Y · ˙ Z