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)

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 1 2 3 lidlmcl ⊢ R ∈ Ring ∧ I ∈ U ∧ x ∈ B ∧ y ∈ I → x · ˙ y ∈ I
6 5 ralrimivva ⊢ R ∈ Ring ∧ I ∈ U → ∀ x ∈ B ∀ y ∈ I x · ˙ y ∈ I
7 4 6 jca ⊢ R ∈ Ring ∧ I ∈ U → I ∈ SubGrp ⁡ R ∧ ∀ x ∈ B ∀ y ∈ I x · ˙ y ∈ I
8 1 2 3 dflidl2lem ⊢ I ∈ SubGrp ⁡ R ∧ ∀ x ∈ B ∀ y ∈ I x · ˙ y ∈ I → I ∈ U
9 8 adantl ⊢ R ∈ Ring ∧ I ∈ SubGrp ⁡ R ∧ ∀ x ∈ B ∀ y ∈ I x · ˙ y ∈ I → I ∈ U
10 7 9 impbida ⊢ R ∈ Ring → I ∈ U ↔ I ∈ SubGrp ⁡ R ∧ ∀ x ∈ B ∀ y ∈ I x · ˙ y ∈ I