Theorem isridlrng

Description: A right ideal is a left ideal of the opposite non-unital 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, 21-Mar-2025)

	Ref	Expression
Hypotheses	isridlrng.u	|- U = ( LIdeal ` ( oppR ` R ) )
	isridlrng.b	|- B = ( Base ` R )
	isridlrng.t	|- .x. = ( .r ` R )
Assertion	isridlrng	|- ( ( R e. Rng /\ I e. ( SubGrp ` R ) ) -> ( I e. U <-> A. x e. B A. y e. I ( y .x. x ) e. I ) )

Proof

Step	Hyp	Ref	Expression
1		isridlrng.u	|- U = ( LIdeal ` ( oppR ` R ) )
2		isridlrng.b	|- B = ( Base ` R )
3		isridlrng.t	|- .x. = ( .r ` R )
4		eqid	|- ( oppR ` R ) = ( oppR ` R )
5	4	opprrng	|- ( R e. Rng -> ( oppR ` R ) e. Rng )
6	4	opprsubg	|- ( SubGrp ` R ) = ( SubGrp ` ( oppR ` R ) )
7	6	a1i	|- ( R e. Rng -> ( SubGrp ` R ) = ( SubGrp ` ( oppR ` R ) ) )
8	7	eleq2d	|- ( R e. Rng -> ( I e. ( SubGrp ` R ) <-> I e. ( SubGrp ` ( oppR ` R ) ) ) )
9	8	biimpa	|- ( ( R e. Rng /\ I e. ( SubGrp ` R ) ) -> I e. ( SubGrp ` ( oppR ` R ) ) )
10	4 2	opprbas	|- B = ( Base ` ( oppR ` R ) )
11		eqid	|- ( .r ` ( oppR ` R ) ) = ( .r ` ( oppR ` R ) )
12	1 10 11	dflidl2rng	|- ( ( ( oppR ` R ) e. Rng /\ I e. ( SubGrp ` ( oppR ` R ) ) ) -> ( I e. U <-> A. x e. B A. y e. I ( x ( .r ` ( oppR ` R ) ) y ) e. I ) )
13	5 9 12	syl2an2r	|- ( ( R e. Rng /\ I e. ( SubGrp ` R ) ) -> ( I e. U <-> A. x e. B A. y e. I ( x ( .r ` ( oppR ` R ) ) y ) e. I ) )
14	2 3 4 11	opprmul	|- ( x ( .r ` ( oppR ` R ) ) y ) = ( y .x. x )
15	14	eleq1i	|- ( ( x ( .r ` ( oppR ` R ) ) y ) e. I <-> ( y .x. x ) e. I )
16	15	a1i	|- ( ( ( ( R e. Rng /\ I e. ( SubGrp ` R ) ) /\ x e. B ) /\ y e. I ) -> ( ( x ( .r ` ( oppR ` R ) ) y ) e. I <-> ( y .x. x ) e. I ) )
17	16	ralbidva	|- ( ( ( R e. Rng /\ I e. ( SubGrp ` R ) ) /\ x e. B ) -> ( A. y e. I ( x ( .r ` ( oppR ` R ) ) y ) e. I <-> A. y e. I ( y .x. x ) e. I ) )
18	17	ralbidva	|- ( ( R e. Rng /\ I e. ( SubGrp ` R ) ) -> ( A. x e. B A. y e. I ( x ( .r ` ( oppR ` R ) ) y ) e. I <-> A. x e. B A. y e. I ( y .x. x ) e. I ) )
19	13 18	bitrd	|- ( ( R e. Rng /\ I e. ( SubGrp ` R ) ) -> ( I e. U <-> A. x e. B A. y e. I ( y .x. x ) e. I ) )