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

Metamath Proof Explorer

Theorem subrgmcld

Description: A subring is closed under multiplication. (Contributed by Thierry Arnoux, 6-Jul-2025)

Ref Expression
Hypotheses subrgmcld.1 ⊢ · = ( .r ‘ 𝑅 )
subrgmcld.2 ⊢ ( 𝜑 → 𝐴 ∈ ( SubRing ‘ 𝑅 ) )
subrgmcld.3 ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
subrgmcld.4 ⊢ ( 𝜑 → 𝑌 ∈ 𝐴 )
Assertion subrgmcld ( 𝜑 → ( 𝑋 · 𝑌 ) ∈ 𝐴 )

Proof

Step Hyp Ref Expression
1 subrgmcld.1 ⊢ · = ( .r ‘ 𝑅 )
2 subrgmcld.2 ⊢ ( 𝜑 → 𝐴 ∈ ( SubRing ‘ 𝑅 ) )
3 subrgmcld.3 ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
4 subrgmcld.4 ⊢ ( 𝜑 → 𝑌 ∈ 𝐴 )
5 1 subrgmcl ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( 𝑋 · 𝑌 ) ∈ 𝐴 )
6 2 3 4 5 syl3anc ⊢ ( 𝜑 → ( 𝑋 · 𝑌 ) ∈ 𝐴 )