Metamath Proof Explorer

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	$⊢ \underset{˙}{0} = 0_{R}$
		rnglidlmcl.b	$⊢ B = {Base}_{R}$
		rnglidlmcl.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
		rngridlmcl.u	$⊢ U = LIdeal ({opp}_{r} (R))$
	Assertion	rngridlmcl	$⊢ ((R \in Rng \land I \in U \land \underset{˙}{0} \in I) \land (X \in B \land Y \in I)) \to Y \underset{˙}{\cdot} X \in I$

Proof

Step	Hyp	Ref	Expression
1		rnglidlmcl.z	$⊢ \underset{˙}{0} = 0_{R}$
2		rnglidlmcl.b	$⊢ B = {Base}_{R}$
3		rnglidlmcl.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		rngridlmcl.u	$⊢ U = LIdeal ({opp}_{r} (R))$
5		eqid	$⊢ {opp}_{r} (R) = {opp}_{r} (R)$
6		eqid	$⊢ \cdot_{{opp}_{r} (R)} = \cdot_{{opp}_{r} (R)}$
7	2 3 5 6	opprmul	$⊢ X \cdot_{{opp}_{r} (R)} Y = Y \underset{˙}{\cdot} X$
8	5	opprrng	$⊢ R \in Rng \to {opp}_{r} (R) \in Rng$
9		id	$⊢ I \in U \to I \in U$
10	1	eleq1i	$⊢ \underset{˙}{0} \in I \leftrightarrow 0_{R} \in I$
11	10	biimpi	$⊢ \underset{˙}{0} \in I \to 0_{R} \in I$
12		eqid	$⊢ 0_{R} = 0_{R}$
13	5 12	oppr0	$⊢ 0_{R} = 0_{{opp}_{r} (R)}$
14	5 2	opprbas	$⊢ B = {Base}_{{opp}_{r} (R)}$
15	13 14 6 4	rnglidlmcl	$⊢ (({opp}_{r} (R) \in Rng \land I \in U \land 0_{R} \in I) \land (X \in B \land Y \in I)) \to X \cdot_{{opp}_{r} (R)} Y \in I$
16	8 9 11 15	syl3anl	$⊢ ((R \in Rng \land I \in U \land \underset{˙}{0} \in I) \land (X \in B \land Y \in I)) \to X \cdot_{{opp}_{r} (R)} Y \in I$
17	7 16	eqeltrrid	$⊢ ((R \in Rng \land I \in U \land \underset{˙}{0} \in I) \land (X \in B \land Y \in I)) \to Y \underset{˙}{\cdot} X \in I$