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

Metamath Proof Explorer

Theorem df2idl2rng

Description: Alternate (the usual textbook) definition of a two-sided ideal of a non-unital ring to be a subgroup of the additive group of the ring which is closed under left- and right-multiplication by elements of the full ring. (Contributed by AV, 21-Mar-2025)

Ref Expression
Hypotheses df2idl2rng.u ⊢ U = 2Ideal ⁡ R
df2idl2rng.b ⊢ B = Base R
df2idl2rng.t ⊢ · ˙ = ⋅ R
Assertion df2idl2rng ⊢ R ∈ Rng ∧ I ∈ SubGrp ⁡ R → I ∈ U ↔ ∀ x ∈ B ∀ y ∈ I x · ˙ y ∈ I ∧ y · ˙ x ∈ I

Proof

Step Hyp Ref Expression
1 df2idl2rng.u ⊢ U = 2Ideal ⁡ R
2 df2idl2rng.b ⊢ B = Base R
3 df2idl2rng.t ⊢ · ˙ = ⋅ R
4 eqid ⊢ LIdeal ⁡ R = LIdeal ⁡ R
5 4 2 3 dflidl2rng ⊢ R ∈ Rng ∧ I ∈ SubGrp ⁡ R → I ∈ LIdeal ⁡ R ↔ ∀ x ∈ B ∀ y ∈ I x · ˙ y ∈ I
6 eqid ⊢ LIdeal ⁡ opp r ⁡ R = LIdeal ⁡ opp r ⁡ R
7 6 2 3 isridlrng ⊢ R ∈ Rng ∧ I ∈ SubGrp ⁡ R → I ∈ LIdeal ⁡ opp r ⁡ R ↔ ∀ x ∈ B ∀ y ∈ I y · ˙ x ∈ I
8 5 7 anbi12d ⊢ R ∈ Rng ∧ I ∈ SubGrp ⁡ R → I ∈ LIdeal ⁡ R ∧ I ∈ LIdeal ⁡ opp r ⁡ R ↔ ∀ x ∈ B ∀ y ∈ I x · ˙ y ∈ I ∧ ∀ x ∈ B ∀ y ∈ I y · ˙ x ∈ I
9 eqid ⊢ opp r ⁡ R = opp r ⁡ R
10 4 9 6 1 2idlelb ⊢ I ∈ U ↔ I ∈ LIdeal ⁡ R ∧ I ∈ LIdeal ⁡ opp r ⁡ R
11 r19.26-2 ⊢ ∀ x ∈ B ∀ y ∈ I x · ˙ y ∈ I ∧ y · ˙ x ∈ I ↔ ∀ x ∈ B ∀ y ∈ I x · ˙ y ∈ I ∧ ∀ x ∈ B ∀ y ∈ I y · ˙ x ∈ I
12 8 10 11 3bitr4g ⊢ R ∈ Rng ∧ I ∈ SubGrp ⁡ R → I ∈ U ↔ ∀ x ∈ B ∀ y ∈ I x · ˙ y ∈ I ∧ y · ˙ x ∈ I