This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = Base R
ringcld.t ⊢ · ˙ = ⋅ R
ringcld.r ⊢ φ → R ∈ Ring
ringcld.x ⊢ φ → X ∈ B
ringcld.y ⊢ φ → Y ∈ B
Assertion ringcld ⊢ φ → X · ˙ Y ∈ B

Proof

Step Hyp Ref Expression
1 ringcld.b ⊢ B = Base R
2 ringcld.t ⊢ · ˙ = ⋅ R
3 ringcld.r ⊢ φ → R ∈ Ring
4 ringcld.x ⊢ φ → X ∈ B
5 ringcld.y ⊢ φ → Y ∈ B
6 1 2 ringcl ⊢ R ∈ Ring ∧ X ∈ B ∧ Y ∈ B → X · ˙ Y ∈ B
7 3 4 5 6 syl3anc ⊢ φ → X · ˙ Y ∈ B