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 ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( 𝑥 · 𝑦 ) ∈ 𝐼 ) ) )