This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem df2idl2rng

Description: Alternate (the usual textbook) definition of a two-sided ideal of a non-unital 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, 21-Mar-2025)

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

Proof

Step Hyp Ref Expression
1 df2idl2rng.u ⊢ 𝑈 = ( 2Ideal ‘ 𝑅 )
2 df2idl2rng.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
3 df2idl2rng.t ⊢ · = ( .r ‘ 𝑅 )
4 eqid ⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
5 4 2 3 dflidl2rng ⊢ ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ) → ( 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( 𝑥 · 𝑦 ) ∈ 𝐼 ) )
6 eqid ⊢ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) = ( LIdeal ‘ ( oppr ‘ 𝑅 ) )
7 6 2 3 isridlrng ⊢ ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ) → ( 𝐼 ∈ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( 𝑦 · 𝑥 ) ∈ 𝐼 ) )
8 5 7 anbi12d ⊢ ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ) → ( ( 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ∈ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) ) ↔ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( 𝑥 · 𝑦 ) ∈ 𝐼 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( 𝑦 · 𝑥 ) ∈ 𝐼 ) ) )
9 eqid ⊢ ( oppr ‘ 𝑅 ) = ( oppr ‘ 𝑅 )
10 4 9 6 1 2idlelb ⊢ ( 𝐼 ∈ 𝑈 ↔ ( 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ∈ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) ) )
11 r19.26-2 ⊢ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( ( 𝑥 · 𝑦 ) ∈ 𝐼 ∧ ( 𝑦 · 𝑥 ) ∈ 𝐼 ) ↔ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( 𝑥 · 𝑦 ) ∈ 𝐼 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( 𝑦 · 𝑥 ) ∈ 𝐼 ) )
12 8 10 11 3bitr4g ⊢ ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ) → ( 𝐼 ∈ 𝑈 ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( ( 𝑥 · 𝑦 ) ∈ 𝐼 ∧ ( 𝑦 · 𝑥 ) ∈ 𝐼 ) ) )