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 ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( 𝑦 · 𝑥 ) ∈ 𝐼 ) ) )