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 𝑈 = ( LIdeal ‘ 𝑅 )
dflidl2.b 𝐵 = ( Base ‘ 𝑅 )
dflidl2.t · = ( .r𝑅 )
Assertion dflidl2 ( 𝑅 ∈ Ring → ( 𝐼𝑈 ↔ ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥𝐵𝑦𝐼 ( 𝑥 · 𝑦 ) ∈ 𝐼 ) ) )

Proof

Step Hyp Ref Expression
1 dflidl2.u 𝑈 = ( LIdeal ‘ 𝑅 )
2 dflidl2.b 𝐵 = ( Base ‘ 𝑅 )
3 dflidl2.t · = ( .r𝑅 )
4 1 lidlsubg ( ( 𝑅 ∈ Ring ∧ 𝐼𝑈 ) → 𝐼 ∈ ( SubGrp ‘ 𝑅 ) )
5 1 2 3 lidlmcl ( ( ( 𝑅 ∈ Ring ∧ 𝐼𝑈 ) ∧ ( 𝑥𝐵𝑦𝐼 ) ) → ( 𝑥 · 𝑦 ) ∈ 𝐼 )
6 5 ralrimivva ( ( 𝑅 ∈ Ring ∧ 𝐼𝑈 ) → ∀ 𝑥𝐵𝑦𝐼 ( 𝑥 · 𝑦 ) ∈ 𝐼 )
7 4 6 jca ( ( 𝑅 ∈ Ring ∧ 𝐼𝑈 ) → ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥𝐵𝑦𝐼 ( 𝑥 · 𝑦 ) ∈ 𝐼 ) )
8 1 2 3 dflidl2lem ( ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥𝐵𝑦𝐼 ( 𝑥 · 𝑦 ) ∈ 𝐼 ) → 𝐼𝑈 )
9 8 adantl ( ( 𝑅 ∈ Ring ∧ ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥𝐵𝑦𝐼 ( 𝑥 · 𝑦 ) ∈ 𝐼 ) ) → 𝐼𝑈 )
10 7 9 impbida ( 𝑅 ∈ Ring → ( 𝐼𝑈 ↔ ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥𝐵𝑦𝐼 ( 𝑥 · 𝑦 ) ∈ 𝐼 ) ) )