Theorem df2idl2

Description: Alternate (the usual textbook) definition of a two-sided ideal of a ring to be a subgroup of the additive group of the ring which is closed under left- and right-multiplication by elements of the full ring. (Contributed by AV, 13-Feb-2025) (Proof shortened by AV, 18-Apr-2025)

	Ref	Expression
Hypotheses	df2idl2rng.u	⊢ 𝑈 = ( 2Ideal ‘ 𝑅 )
	df2idl2rng.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	df2idl2rng.t	⊢ · = ( .r ‘ 𝑅 )
Assertion	df2idl2	⊢ ( 𝑅 ∈ Ring → ( 𝐼 ∈ 𝑈 ↔ ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( ( 𝑥 · 𝑦 ) ∈ 𝐼 ∧ ( 𝑦 · 𝑥 ) ∈ 𝐼 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		df2idl2rng.u	⊢ 𝑈 = ( 2Ideal ‘ 𝑅 )
2		df2idl2rng.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
3		df2idl2rng.t	⊢ · = ( .r ‘ 𝑅 )
4	1	eleq2i	⊢ ( 𝐼 ∈ 𝑈 ↔ 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
5	4	biimpi	⊢ ( 𝐼 ∈ 𝑈 → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
6	5	2idllidld	⊢ ( 𝐼 ∈ 𝑈 → 𝐼 ∈ ( LIdeal ‘ 𝑅 ) )
7		eqid	⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
8	7	lidlsubg	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) → 𝐼 ∈ ( SubGrp ‘ 𝑅 ) )
9	6 8	sylan2	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) → 𝐼 ∈ ( SubGrp ‘ 𝑅 ) )
10		ringrng	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Rng )
11	1 2 3	df2idl2rng	⊢ ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ) → ( 𝐼 ∈ 𝑈 ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( ( 𝑥 · 𝑦 ) ∈ 𝐼 ∧ ( 𝑦 · 𝑥 ) ∈ 𝐼 ) ) )
12	10 11	sylan	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ) → ( 𝐼 ∈ 𝑈 ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( ( 𝑥 · 𝑦 ) ∈ 𝐼 ∧ ( 𝑦 · 𝑥 ) ∈ 𝐼 ) ) )
13	9 12	biadanid	⊢ ( 𝑅 ∈ Ring → ( 𝐼 ∈ 𝑈 ↔ ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( ( 𝑥 · 𝑦 ) ∈ 𝐼 ∧ ( 𝑦 · 𝑥 ) ∈ 𝐼 ) ) ) )