This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database BASIC ALGEBRAIC STRUCTURES Subring algebras and ideals Left ideals and spans 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 ⊢ 𝑈 = ( 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 ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( 𝑥 · 𝑦 ) ∈ 𝐼 ) ) )