Metamath Proof Explorer


Theorem isridl

Description: A right ideal is a left ideal of the opposite 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, 13-Feb-2025)

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

Proof

Step Hyp Ref Expression
1 isridl.u 𝑈 = ( LIdeal ‘ ( oppr𝑅 ) )
2 isridl.b 𝐵 = ( Base ‘ 𝑅 )
3 isridl.t · = ( .r𝑅 )
4 eqid ( oppr𝑅 ) = ( oppr𝑅 )
5 4 opprring ( 𝑅 ∈ Ring → ( oppr𝑅 ) ∈ Ring )
6 4 2 opprbas 𝐵 = ( Base ‘ ( oppr𝑅 ) )
7 eqid ( .r ‘ ( oppr𝑅 ) ) = ( .r ‘ ( oppr𝑅 ) )
8 1 6 7 dflidl2 ( ( oppr𝑅 ) ∈ Ring → ( 𝐼𝑈 ↔ ( 𝐼 ∈ ( SubGrp ‘ ( oppr𝑅 ) ) ∧ ∀ 𝑥𝐵𝑦𝐼 ( 𝑥 ( .r ‘ ( oppr𝑅 ) ) 𝑦 ) ∈ 𝐼 ) ) )
9 5 8 syl ( 𝑅 ∈ Ring → ( 𝐼𝑈 ↔ ( 𝐼 ∈ ( SubGrp ‘ ( oppr𝑅 ) ) ∧ ∀ 𝑥𝐵𝑦𝐼 ( 𝑥 ( .r ‘ ( oppr𝑅 ) ) 𝑦 ) ∈ 𝐼 ) ) )
10 4 opprsubg ( SubGrp ‘ 𝑅 ) = ( SubGrp ‘ ( oppr𝑅 ) )
11 10 eqcomi ( SubGrp ‘ ( oppr𝑅 ) ) = ( SubGrp ‘ 𝑅 )
12 11 a1i ( 𝑅 ∈ Ring → ( SubGrp ‘ ( oppr𝑅 ) ) = ( SubGrp ‘ 𝑅 ) )
13 12 eleq2d ( 𝑅 ∈ Ring → ( 𝐼 ∈ ( SubGrp ‘ ( oppr𝑅 ) ) ↔ 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ) )
14 2 3 4 7 opprmul ( 𝑥 ( .r ‘ ( oppr𝑅 ) ) 𝑦 ) = ( 𝑦 · 𝑥 )
15 14 eleq1i ( ( 𝑥 ( .r ‘ ( oppr𝑅 ) ) 𝑦 ) ∈ 𝐼 ↔ ( 𝑦 · 𝑥 ) ∈ 𝐼 )
16 15 a1i ( ( ( 𝑅 ∈ Ring ∧ 𝑥𝐵 ) ∧ 𝑦𝐼 ) → ( ( 𝑥 ( .r ‘ ( oppr𝑅 ) ) 𝑦 ) ∈ 𝐼 ↔ ( 𝑦 · 𝑥 ) ∈ 𝐼 ) )
17 16 ralbidva ( ( 𝑅 ∈ Ring ∧ 𝑥𝐵 ) → ( ∀ 𝑦𝐼 ( 𝑥 ( .r ‘ ( oppr𝑅 ) ) 𝑦 ) ∈ 𝐼 ↔ ∀ 𝑦𝐼 ( 𝑦 · 𝑥 ) ∈ 𝐼 ) )
18 17 ralbidva ( 𝑅 ∈ Ring → ( ∀ 𝑥𝐵𝑦𝐼 ( 𝑥 ( .r ‘ ( oppr𝑅 ) ) 𝑦 ) ∈ 𝐼 ↔ ∀ 𝑥𝐵𝑦𝐼 ( 𝑦 · 𝑥 ) ∈ 𝐼 ) )
19 13 18 anbi12d ( 𝑅 ∈ Ring → ( ( 𝐼 ∈ ( SubGrp ‘ ( oppr𝑅 ) ) ∧ ∀ 𝑥𝐵𝑦𝐼 ( 𝑥 ( .r ‘ ( oppr𝑅 ) ) 𝑦 ) ∈ 𝐼 ) ↔ ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥𝐵𝑦𝐼 ( 𝑦 · 𝑥 ) ∈ 𝐼 ) ) )
20 9 19 bitrd ( 𝑅 ∈ Ring → ( 𝐼𝑈 ↔ ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥𝐵𝑦𝐼 ( 𝑦 · 𝑥 ) ∈ 𝐼 ) ) )