Theorem lidlmcld

Description: An ideal is closed under left-multiplication by elements of the full ring. (Contributed by Thierry Arnoux, 3-Jun-2025)

	Ref	Expression
Hypotheses	lidlmcld.1	|- U = ( LIdeal ` R )
	lidlmcld.2	|- B = ( Base ` R )
	lidlmcld.3	|- .x. = ( .r ` R )
	lidlmcld.4	|- ( ph -> R e. Ring )
	lidlmcld.5	|- ( ph -> I e. U )
	lidlmcld.6	|- ( ph -> X e. B )
	lidlmcld.7	|- ( ph -> Y e. I )
Assertion	lidlmcld	|- ( ph -> ( X .x. Y ) e. I )

Proof

Step	Hyp	Ref	Expression
1		lidlmcld.1	|- U = ( LIdeal ` R )
2		lidlmcld.2	|- B = ( Base ` R )
3		lidlmcld.3	|- .x. = ( .r ` R )
4		lidlmcld.4	|- ( ph -> R e. Ring )
5		lidlmcld.5	|- ( ph -> I e. U )
6		lidlmcld.6	|- ( ph -> X e. B )
7		lidlmcld.7	|- ( ph -> Y e. I )
8	1 2 3	lidlmcl	|- ( ( ( R e. Ring /\ I e. U ) /\ ( X e. B /\ Y e. I ) ) -> ( X .x. Y ) e. I )
9	4 5 6 7 8	syl22anc	|- ( ph -> ( X .x. Y ) e. I )