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 ` R )
	rnglidlmcl.b	|- B = ( Base ` R )
	rnglidlmcl.t	|- .x. = ( .r ` R )
	rngridlmcl.u	|- U = ( LIdeal ` ( oppR ` R ) )
Assertion	rngridlmcl	|- ( ( ( R e. Rng /\ I e. U /\ .0. e. I ) /\ ( X e. B /\ Y e. I ) ) -> ( Y .x. X ) e. I )

Proof

Step	Hyp	Ref	Expression
1		rnglidlmcl.z	|- .0. = ( 0g ` R )
2		rnglidlmcl.b	|- B = ( Base ` R )
3		rnglidlmcl.t	|- .x. = ( .r ` R )
4		rngridlmcl.u	|- U = ( LIdeal ` ( oppR ` R ) )
5		eqid	|- ( oppR ` R ) = ( oppR ` R )
6		eqid	|- ( .r ` ( oppR ` R ) ) = ( .r ` ( oppR ` R ) )
7	2 3 5 6	opprmul	|- ( X ( .r ` ( oppR ` R ) ) Y ) = ( Y .x. X )
8	5	opprrng	|- ( R e. Rng -> ( oppR ` R ) e. Rng )
9		id	|- ( I e. U -> I e. U )
10	1	eleq1i	|- ( .0. e. I <-> ( 0g ` R ) e. I )
11	10	biimpi	|- ( .0. e. I -> ( 0g ` R ) e. I )
12		eqid	|- ( 0g ` R ) = ( 0g ` R )
13	5 12	oppr0	|- ( 0g ` R ) = ( 0g ` ( oppR ` R ) )
14	5 2	opprbas	|- B = ( Base ` ( oppR ` R ) )
15	13 14 6 4	rnglidlmcl	|- ( ( ( ( oppR ` R ) e. Rng /\ I e. U /\ ( 0g ` R ) e. I ) /\ ( X e. B /\ Y e. I ) ) -> ( X ( .r ` ( oppR ` R ) ) Y ) e. I )
16	8 9 11 15	syl3anl	|- ( ( ( R e. Rng /\ I e. U /\ .0. e. I ) /\ ( X e. B /\ Y e. I ) ) -> ( X ( .r ` ( oppR ` R ) ) Y ) e. I )
17	7 16	eqeltrrid	|- ( ( ( R e. Rng /\ I e. U /\ .0. e. I ) /\ ( X e. B /\ Y e. I ) ) -> ( Y .x. X ) e. I )