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 ˙ = 0 R
rnglidlmcl.b ⊢ B = Base R
rnglidlmcl.t ⊢ · ˙ = ⋅ R
rngridlmcl.u ⊢ U = LIdeal ⁡ opp r ⁡ R
Assertion rngridlmcl ⊢ R ∈ Rng ∧ I ∈ U ∧ 0 ˙ ∈ I ∧ X ∈ B ∧ Y ∈ I → Y · ˙ X ∈ I

Proof

Step Hyp Ref Expression
1 rnglidlmcl.z ⊢ 0 ˙ = 0 R
2 rnglidlmcl.b ⊢ B = Base R
3 rnglidlmcl.t ⊢ · ˙ = ⋅ R
4 rngridlmcl.u ⊢ U = LIdeal ⁡ opp r ⁡ R
5 eqid ⊢ opp r ⁡ R = opp r ⁡ R
6 eqid ⊢ ⋅ opp r ⁡ R = ⋅ opp r ⁡ R
7 2 3 5 6 opprmul ⊢ X ⋅ opp r ⁡ R Y = Y · ˙ X
8 5 opprrng ⊢ R ∈ Rng → opp r ⁡ R ∈ Rng
9 id ⊢ I ∈ U → I ∈ U
10 1 eleq1i ⊢ 0 ˙ ∈ I ↔ 0 R ∈ I
11 10 biimpi ⊢ 0 ˙ ∈ I → 0 R ∈ I
12 eqid ⊢ 0 R = 0 R
13 5 12 oppr0 ⊢ 0 R = 0 opp r ⁡ R
14 5 2 opprbas ⊢ B = Base opp r ⁡ R
15 13 14 6 4 rnglidlmcl ⊢ opp r ⁡ R ∈ Rng ∧ I ∈ U ∧ 0 R ∈ I ∧ X ∈ B ∧ Y ∈ I → X ⋅ opp r ⁡ R Y ∈ I
16 8 9 11 15 syl3anl ⊢ R ∈ Rng ∧ I ∈ U ∧ 0 ˙ ∈ I ∧ X ∈ B ∧ Y ∈ I → X ⋅ opp r ⁡ R Y ∈ I
17 7 16 eqeltrrid ⊢ R ∈ Rng ∧ I ∈ U ∧ 0 ˙ ∈ I ∧ X ∈ B ∧ Y ∈ I → Y · ˙ X ∈ I