Theorem rngridlmcl

Description: A right ideal (which is a left ideal over the opposite ring) containing the zero element is closed under right-multiplication by elements of the full non-unital ring. (Contributed by AV, 19-Feb-2025)

	Ref	Expression
Hypotheses	rnglidlmcl.z	⊢ 0 = ( 0g ‘ 𝑅 )
	rnglidlmcl.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	rnglidlmcl.t	⊢ · = ( .r ‘ 𝑅 )
	rngridlmcl.u	⊢ 𝑈 = ( LIdeal ‘ ( oppr ‘ 𝑅 ) )
Assertion	rngridlmcl	⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ 𝑈 ∧ 0 ∈ 𝐼 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐼 ) ) → ( 𝑌 · 𝑋 ) ∈ 𝐼 )

Proof

Step	Hyp	Ref	Expression
1		rnglidlmcl.z	⊢ 0 = ( 0g ‘ 𝑅 )
2		rnglidlmcl.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
3		rnglidlmcl.t	⊢ · = ( .r ‘ 𝑅 )
4		rngridlmcl.u	⊢ 𝑈 = ( LIdeal ‘ ( oppr ‘ 𝑅 ) )
5		eqid	⊢ ( oppr ‘ 𝑅 ) = ( oppr ‘ 𝑅 )
6		eqid	⊢ ( .r ‘ ( oppr ‘ 𝑅 ) ) = ( .r ‘ ( oppr ‘ 𝑅 ) )
7	2 3 5 6	opprmul	⊢ ( 𝑋 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑌 ) = ( 𝑌 · 𝑋 )
8	5	opprrng	⊢ ( 𝑅 ∈ Rng → ( oppr ‘ 𝑅 ) ∈ Rng )
9		id	⊢ ( 𝐼 ∈ 𝑈 → 𝐼 ∈ 𝑈 )
10	1	eleq1i	⊢ ( 0 ∈ 𝐼 ↔ ( 0g ‘ 𝑅 ) ∈ 𝐼 )
11	10	biimpi	⊢ ( 0 ∈ 𝐼 → ( 0g ‘ 𝑅 ) ∈ 𝐼 )
12		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
13	5 12	oppr0	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ ( oppr ‘ 𝑅 ) )
14	5 2	opprbas	⊢ 𝐵 = ( Base ‘ ( oppr ‘ 𝑅 ) )
15	13 14 6 4	rnglidlmcl	⊢ ( ( ( ( oppr ‘ 𝑅 ) ∈ Rng ∧ 𝐼 ∈ 𝑈 ∧ ( 0g ‘ 𝑅 ) ∈ 𝐼 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐼 ) ) → ( 𝑋 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑌 ) ∈ 𝐼 )
16	8 9 11 15	syl3anl	⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ 𝑈 ∧ 0 ∈ 𝐼 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐼 ) ) → ( 𝑋 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑌 ) ∈ 𝐼 )
17	7 16	eqeltrrid	⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ 𝑈 ∧ 0 ∈ 𝐼 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐼 ) ) → ( 𝑌 · 𝑋 ) ∈ 𝐼 )