Theorem subrgmcld

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

	Ref	Expression
Hypotheses	subrgmcld.1	|- .x. = ( .r ` R )
	subrgmcld.2	|- ( ph -> A e. ( SubRing ` R ) )
	subrgmcld.3	|- ( ph -> X e. A )
	subrgmcld.4	|- ( ph -> Y e. A )
Assertion	subrgmcld	|- ( ph -> ( X .x. Y ) e. A )

Proof

Step	Hyp	Ref	Expression
1		subrgmcld.1	|- .x. = ( .r ` R )
2		subrgmcld.2	|- ( ph -> A e. ( SubRing ` R ) )
3		subrgmcld.3	|- ( ph -> X e. A )
4		subrgmcld.4	|- ( ph -> Y e. A )
5	1	subrgmcl	|- ( ( A e. ( SubRing ` R ) /\ X e. A /\ Y e. A ) -> ( X .x. Y ) e. A )
6	2 3 4 5	syl3anc	|- ( ph -> ( X .x. Y ) e. A )