Theorem subrgmcld

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

	Ref	Expression
Hypotheses	subrgmcld.1	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	subrgmcld.2	$$⊢\phi \to A\in \mathrm{SubRing}\left(R\right)$$
	subrgmcld.3	$$⊢\phi \to X\in A$$
	subrgmcld.4	$$⊢\phi \to Y\in A$$
Assertion	subrgmcld	$$⊢\phi \to X\underset{\dot{}}{·}Y\in A$$

Proof

Step	Hyp	Ref	Expression
1		subrgmcld.1	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
2		subrgmcld.2	$$⊢\phi \to A\in \mathrm{SubRing}\left(R\right)$$
3		subrgmcld.3	$$⊢\phi \to X\in A$$
4		subrgmcld.4	$$⊢\phi \to Y\in A$$
5	1	subrgmcl	$$⊢\left(A\in \mathrm{SubRing}\left(R\right)\wedge X\in A\wedge Y\in A\right)\to X\underset{\dot{}}{·}Y\in A$$
6	2 3 4 5	syl3anc	$$⊢\phi \to X\underset{\dot{}}{·}Y\in A$$