Metamath Proof Explorer

Theorem isridlrng

Description: A right ideal is a left ideal of the opposite non-unital ring. This theorem shows that this definition corresponds to the usual textbook definition of a right ideal of a ring to be a subgroup of the additive group of the ring which is closed under right-multiplication by elements of the full ring. (Contributed by AV, 21-Mar-2025)

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

Proof

Step Hyp Ref Expression
1 isridlrng.u ⊢ 𝑈 = ( LIdeal ‘ ( oppr ‘ 𝑅 ) )
2 isridlrng.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
3 isridlrng.t ⊢ · = ( .r ‘ 𝑅 )
4 eqid ⊢ ( oppr ‘ 𝑅 ) = ( oppr ‘ 𝑅 )
5 4 opprrng ⊢ ( 𝑅 ∈ Rng → ( oppr ‘ 𝑅 ) ∈ Rng )
6 4 opprsubg ⊢ ( SubGrp ‘ 𝑅 ) = ( SubGrp ‘ ( oppr ‘ 𝑅 ) )
7 6 a1i ⊢ ( 𝑅 ∈ Rng → ( SubGrp ‘ 𝑅 ) = ( SubGrp ‘ ( oppr ‘ 𝑅 ) ) )
8 7 eleq2d ⊢ ( 𝑅 ∈ Rng → ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ↔ 𝐼 ∈ ( SubGrp ‘ ( oppr ‘ 𝑅 ) ) ) )
9 8 biimpa ⊢ ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ) → 𝐼 ∈ ( SubGrp ‘ ( oppr ‘ 𝑅 ) ) )
10 4 2 opprbas ⊢ 𝐵 = ( Base ‘ ( oppr ‘ 𝑅 ) )
11 eqid ⊢ ( .r ‘ ( oppr ‘ 𝑅 ) ) = ( .r ‘ ( oppr ‘ 𝑅 ) )
12 1 10 11 dflidl2rng ⊢ ( ( ( oppr ‘ 𝑅 ) ∈ Rng ∧ 𝐼 ∈ ( SubGrp ‘ ( oppr ‘ 𝑅 ) ) ) → ( 𝐼 ∈ 𝑈 ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( 𝑥 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑦 ) ∈ 𝐼 ) )
13 5 9 12 syl2an2r ⊢ ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ) → ( 𝐼 ∈ 𝑈 ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( 𝑥 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑦 ) ∈ 𝐼 ) )
14 2 3 4 11 opprmul ⊢ ( 𝑥 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑦 ) = ( 𝑦 · 𝑥 )
15 14 eleq1i ⊢ ( ( 𝑥 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑦 ) ∈ 𝐼 ↔ ( 𝑦 · 𝑥 ) ∈ 𝐼 )
16 15 a1i ⊢ ( ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐼 ) → ( ( 𝑥 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑦 ) ∈ 𝐼 ↔ ( 𝑦 · 𝑥 ) ∈ 𝐼 ) )
17 16 ralbidva ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( ∀ 𝑦 ∈ 𝐼 ( 𝑥 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑦 ) ∈ 𝐼 ↔ ∀ 𝑦 ∈ 𝐼 ( 𝑦 · 𝑥 ) ∈ 𝐼 ) )
18 17 ralbidva ⊢ ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( 𝑥 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑦 ) ∈ 𝐼 ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( 𝑦 · 𝑥 ) ∈ 𝐼 ) )
19 13 18 bitrd ⊢ ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ) → ( 𝐼 ∈ 𝑈 ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( 𝑦 · 𝑥 ) ∈ 𝐼 ) )