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)

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

Proof

Step	Hyp	Ref	Expression
1		df2idl2.u	⊢ 𝑈 = ( 2Ideal ‘ 𝑅 )
2		df2idl2.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
3		df2idl2.t	⊢ · = ( .r ‘ 𝑅 )
4		eqid	⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
5		eqid	⊢ ( oppr ‘ 𝑅 ) = ( oppr ‘ 𝑅 )
6		eqid	⊢ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) = ( LIdeal ‘ ( oppr ‘ 𝑅 ) )
7	4 5 6 1	2idlval	⊢ 𝑈 = ( ( LIdeal ‘ 𝑅 ) ∩ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) )
8	7	elin2	⊢ ( 𝐼 ∈ 𝑈 ↔ ( 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ∈ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) ) )
9	8	a1i	⊢ ( 𝑅 ∈ Ring → ( 𝐼 ∈ 𝑈 ↔ ( 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ∈ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) ) ) )
10	4 2 3	dflidl2	⊢ ( 𝑅 ∈ Ring → ( 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ↔ ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( 𝑥 · 𝑦 ) ∈ 𝐼 ) ) )
11	6 2 3	isridl	⊢ ( 𝑅 ∈ Ring → ( 𝐼 ∈ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) ↔ ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( 𝑦 · 𝑥 ) ∈ 𝐼 ) ) )
12	10 11	anbi12d	⊢ ( 𝑅 ∈ Ring → ( ( 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ∈ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) ) ↔ ( ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( 𝑥 · 𝑦 ) ∈ 𝐼 ) ∧ ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( 𝑦 · 𝑥 ) ∈ 𝐼 ) ) ) )
13		anandi	⊢ ( ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ∧ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( 𝑥 · 𝑦 ) ∈ 𝐼 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( 𝑦 · 𝑥 ) ∈ 𝐼 ) ) ↔ ( ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( 𝑥 · 𝑦 ) ∈ 𝐼 ) ∧ ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( 𝑦 · 𝑥 ) ∈ 𝐼 ) ) )
14		r19.26-2	⊢ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( ( 𝑥 · 𝑦 ) ∈ 𝐼 ∧ ( 𝑦 · 𝑥 ) ∈ 𝐼 ) ↔ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( 𝑥 · 𝑦 ) ∈ 𝐼 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( 𝑦 · 𝑥 ) ∈ 𝐼 ) )
15	14	bicomi	⊢ ( ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( 𝑥 · 𝑦 ) ∈ 𝐼 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( 𝑦 · 𝑥 ) ∈ 𝐼 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( ( 𝑥 · 𝑦 ) ∈ 𝐼 ∧ ( 𝑦 · 𝑥 ) ∈ 𝐼 ) )
16	15	a1i	⊢ ( 𝑅 ∈ Ring → ( ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( 𝑥 · 𝑦 ) ∈ 𝐼 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( 𝑦 · 𝑥 ) ∈ 𝐼 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( ( 𝑥 · 𝑦 ) ∈ 𝐼 ∧ ( 𝑦 · 𝑥 ) ∈ 𝐼 ) ) )
17	16	anbi2d	⊢ ( 𝑅 ∈ Ring → ( ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ∧ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( 𝑥 · 𝑦 ) ∈ 𝐼 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( 𝑦 · 𝑥 ) ∈ 𝐼 ) ) ↔ ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( ( 𝑥 · 𝑦 ) ∈ 𝐼 ∧ ( 𝑦 · 𝑥 ) ∈ 𝐼 ) ) ) )
18	13 17	bitr3id	⊢ ( 𝑅 ∈ Ring → ( ( ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( 𝑥 · 𝑦 ) ∈ 𝐼 ) ∧ ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( 𝑦 · 𝑥 ) ∈ 𝐼 ) ) ↔ ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( ( 𝑥 · 𝑦 ) ∈ 𝐼 ∧ ( 𝑦 · 𝑥 ) ∈ 𝐼 ) ) ) )
19	9 12 18	3bitrd	⊢ ( 𝑅 ∈ Ring → ( 𝐼 ∈ 𝑈 ↔ ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( ( 𝑥 · 𝑦 ) ∈ 𝐼 ∧ ( 𝑦 · 𝑥 ) ∈ 𝐼 ) ) ) )