Metamath Proof Explorer


Theorem ringcld

Description: Closure of the multiplication operation of a ring. (Contributed by SN, 29-Jul-2024)

Ref Expression
Hypotheses ringcld.b B=BaseR
ringcld.t ·˙=R
ringcld.r φRRing
ringcld.x φXB
ringcld.y φYB
Assertion ringcld φX·˙YB

Proof

Step Hyp Ref Expression
1 ringcld.b B=BaseR
2 ringcld.t ·˙=R
3 ringcld.r φRRing
4 ringcld.x φXB
5 ringcld.y φYB
6 1 2 ringcl RRingXBYBX·˙YB
7 3 4 5 6 syl3anc φX·˙YB