Metamath Proof Explorer

Theorem dflidl2

Description: Alternate (the usual textbook) definition of a (left) ideal of a ring to be a subgroup of the additive group of the ring which is closed under left-multiplication by elements of the full ring. (Contributed by AV, 13-Feb-2025) (Proof shortened by AV, 18-Apr-2025)

Ref Expression
Hypotheses dflidl2.u ⊢ U = LIdeal ⁡ R
dflidl2.b ⊢ B = Base R
dflidl2.t ⊢ · ˙ = ⋅ R
Assertion dflidl2 ⊢ R ∈ Ring → I ∈ U ↔ I ∈ SubGrp ⁡ R ∧ ∀ x ∈ B ∀ y ∈ I x · ˙ y ∈ I

Proof

Step Hyp Ref Expression
1 dflidl2.u ⊢ U = LIdeal ⁡ R
2 dflidl2.b ⊢ B = Base R
3 dflidl2.t ⊢ · ˙ = ⋅ R
4 1 lidlsubg ⊢ R ∈ Ring ∧ I ∈ U → I ∈ SubGrp ⁡ R
5 ringrng ⊢ R ∈ Ring → R ∈ Rng
6 1 2 3 dflidl2rng ⊢ R ∈ Rng ∧ I ∈ SubGrp ⁡ R → I ∈ U ↔ ∀ x ∈ B ∀ y ∈ I x · ˙ y ∈ I
7 5 6 sylan ⊢ R ∈ Ring ∧ I ∈ SubGrp ⁡ R → I ∈ U ↔ ∀ x ∈ B ∀ y ∈ I x · ˙ y ∈ I
8 4 7 biadanid ⊢ R ∈ Ring → I ∈ U ↔ I ∈ SubGrp ⁡ R ∧ ∀ x ∈ B ∀ y ∈ I x · ˙ y ∈ I