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	⊢ ( 𝜑 → ( 𝑋 · 𝑌 ) ∈ 𝐴 )