This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( 𝑋 · 𝑌 ) ∈ 𝐼 )