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	⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
	lidlmcld.2	⊢ 𝐵 = ( Base ‘ 𝑅 )
	lidlmcld.3	⊢ · = ( .r ‘ 𝑅 )
	lidlmcld.4	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	lidlmcld.5	⊢ ( 𝜑 → 𝐼 ∈ 𝑈 )
	lidlmcld.6	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	lidlmcld.7	⊢ ( 𝜑 → 𝑌 ∈ 𝐼 )
Assertion	lidlmcld	⊢ ( 𝜑 → ( 𝑋 · 𝑌 ) ∈ 𝐼 )

Proof

Step	Hyp	Ref	Expression
1		lidlmcld.1	⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
2		lidlmcld.2	⊢ 𝐵 = ( Base ‘ 𝑅 )
3		lidlmcld.3	⊢ · = ( .r ‘ 𝑅 )
4		lidlmcld.4	⊢ ( 𝜑 → 𝑅 ∈ Ring )
5		lidlmcld.5	⊢ ( 𝜑 → 𝐼 ∈ 𝑈 )
6		lidlmcld.6	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
7		lidlmcld.7	⊢ ( 𝜑 → 𝑌 ∈ 𝐼 )
8	1 2 3	lidlmcl	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐼 ) ) → ( 𝑋 · 𝑌 ) ∈ 𝐼 )
9	4 5 6 7 8	syl22anc	⊢ ( 𝜑 → ( 𝑋 · 𝑌 ) ∈ 𝐼 )