Metamath Proof Explorer


Theorem rngcl

Description: Closure of the multiplication operation of a non-unital ring. (Contributed by AV, 17-Apr-2020)

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

Proof

Step Hyp Ref Expression
1 rngcl.b B = Base R
2 rngcl.t · ˙ = R
3 eqid mulGrp R = mulGrp R
4 3 rngmgp R Rng mulGrp R Smgrp
5 sgrpmgm mulGrp R Smgrp mulGrp R Mgm
6 4 5 syl R Rng mulGrp R Mgm
7 3 1 mgpbas B = Base mulGrp R
8 3 2 mgpplusg · ˙ = + mulGrp R
9 7 8 mgmcl mulGrp R Mgm X B Y B X · ˙ Y B
10 6 9 syl3an1 R Rng X B Y B X · ˙ Y B