Database
BASIC ALGEBRAIC STRUCTURES
Subring algebras and ideals
Left ideals and spans
dflidl2
Metamath Proof Explorer
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
⊢ 𝑈 = ( 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
ringrng
⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Rng )
6
1 2 3
dflidl2rng
⊢ ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ) → ( 𝐼 ∈ 𝑈 ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( 𝑥 · 𝑦 ) ∈ 𝐼 ) )
7
5 6
sylan
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ) → ( 𝐼 ∈ 𝑈 ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( 𝑥 · 𝑦 ) ∈ 𝐼 ) )
8
4 7
biadanid
⊢ ( 𝑅 ∈ Ring → ( 𝐼 ∈ 𝑈 ↔ ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( 𝑥 · 𝑦 ) ∈ 𝐼 ) ) )