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=\mathrm{LIdeal}\left(R\right)$$
	lidlmcld.2	$$⊢B={\mathrm{Base}}_R$$
	lidlmcld.3	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	lidlmcld.4	$$⊢\phi \to R\in \mathrm{Ring}$$
	lidlmcld.5	$$⊢\phi \to I\in U$$
	lidlmcld.6	$$⊢\phi \to X\in B$$
	lidlmcld.7	$$⊢\phi \to Y\in I$$
Assertion	lidlmcld	$$⊢\phi \to X\underset{\dot{}}{·}Y\in I$$

Proof

Step	Hyp	Ref	Expression
1		lidlmcld.1	$$⊢U=\mathrm{LIdeal}\left(R\right)$$
2		lidlmcld.2	$$⊢B={\mathrm{Base}}_R$$
3		lidlmcld.3	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
4		lidlmcld.4	$$⊢\phi \to R\in \mathrm{Ring}$$
5		lidlmcld.5	$$⊢\phi \to I\in U$$
6		lidlmcld.6	$$⊢\phi \to X\in B$$
7		lidlmcld.7	$$⊢\phi \to Y\in I$$
8	1 2 3	lidlmcl	$$⊢\left(\left(R\in \mathrm{Ring}\wedge I\in U\right)\wedge \left(X\in B\wedge Y\in I\right)\right)\to X\underset{\dot{}}{·}Y\in I$$
9	4 5 6 7 8	syl22anc	$$⊢\phi \to X\underset{\dot{}}{·}Y\in I$$