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

Metamath Proof Explorer

Theorem rngridlmcl

Description: A right ideal (which is a left ideal over the opposite ring) containing the zero element is closed under right-multiplication by elements of the full non-unital ring. (Contributed by AV, 19-Feb-2025)

Ref Expression
Hypotheses rnglidlmcl.z ⊢ 0 = ( 0g ‘ 𝑅 )
rnglidlmcl.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
rnglidlmcl.t ⊢ · = ( .r ‘ 𝑅 )
rngridlmcl.u ⊢ 𝑈 = ( LIdeal ‘ ( oppr ‘ 𝑅 ) )
Assertion rngridlmcl ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ 𝑈 ∧ 0 ∈ 𝐼 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐼 ) ) → ( 𝑌 · 𝑋 ) ∈ 𝐼 )

Proof

Step Hyp Ref Expression
1 rnglidlmcl.z ⊢ 0 = ( 0g ‘ 𝑅 )
2 rnglidlmcl.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
3 rnglidlmcl.t ⊢ · = ( .r ‘ 𝑅 )
4 rngridlmcl.u ⊢ 𝑈 = ( LIdeal ‘ ( oppr ‘ 𝑅 ) )
5 eqid ⊢ ( oppr ‘ 𝑅 ) = ( oppr ‘ 𝑅 )
6 eqid ⊢ ( .r ‘ ( oppr ‘ 𝑅 ) ) = ( .r ‘ ( oppr ‘ 𝑅 ) )
7 2 3 5 6 opprmul ⊢ ( 𝑋 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑌 ) = ( 𝑌 · 𝑋 )
8 5 opprrng ⊢ ( 𝑅 ∈ Rng → ( oppr ‘ 𝑅 ) ∈ Rng )
9 id ⊢ ( 𝐼 ∈ 𝑈 → 𝐼 ∈ 𝑈 )
10 1 eleq1i ⊢ ( 0 ∈ 𝐼 ↔ ( 0g ‘ 𝑅 ) ∈ 𝐼 )
11 10 biimpi ⊢ ( 0 ∈ 𝐼 → ( 0g ‘ 𝑅 ) ∈ 𝐼 )
12 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
13 5 12 oppr0 ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ ( oppr ‘ 𝑅 ) )
14 5 2 opprbas ⊢ 𝐵 = ( Base ‘ ( oppr ‘ 𝑅 ) )
15 13 14 6 4 rnglidlmcl ⊢ ( ( ( ( oppr ‘ 𝑅 ) ∈ Rng ∧ 𝐼 ∈ 𝑈 ∧ ( 0g ‘ 𝑅 ) ∈ 𝐼 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐼 ) ) → ( 𝑋 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑌 ) ∈ 𝐼 )
16 8 9 11 15 syl3anl ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ 𝑈 ∧ 0 ∈ 𝐼 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐼 ) ) → ( 𝑋 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑌 ) ∈ 𝐼 )
17 7 16 eqeltrrid ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ 𝑈 ∧ 0 ∈ 𝐼 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐼 ) ) → ( 𝑌 · 𝑋 ) ∈ 𝐼 )