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	|- U = ( LIdeal ` ( oppR ` R ) )
	isridl.b	|- B = ( Base ` R )
	isridl.t	|- .x. = ( .r ` R )
Assertion	isridl	|- ( R e. Ring -> ( I e. U <-> ( I e. ( SubGrp ` R ) /\ A. x e. B A. y e. I ( y .x. x ) e. I ) ) )

Proof

Step	Hyp	Ref	Expression
1		isridl.u	|- U = ( LIdeal ` ( oppR ` R ) )
2		isridl.b	|- B = ( Base ` R )
3		isridl.t	|- .x. = ( .r ` R )
4		eqid	|- ( oppR ` R ) = ( oppR ` R )
5	4	opprring	|- ( R e. Ring -> ( oppR ` R ) e. Ring )
6	4 2	opprbas	|- B = ( Base ` ( oppR ` R ) )
7		eqid	|- ( .r ` ( oppR ` R ) ) = ( .r ` ( oppR ` R ) )
8	1 6 7	dflidl2	|- ( ( oppR ` R ) e. Ring -> ( I e. U <-> ( I e. ( SubGrp ` ( oppR ` R ) ) /\ A. x e. B A. y e. I ( x ( .r ` ( oppR ` R ) ) y ) e. I ) ) )
9	5 8	syl	|- ( R e. Ring -> ( I e. U <-> ( I e. ( SubGrp ` ( oppR ` R ) ) /\ A. x e. B A. y e. I ( x ( .r ` ( oppR ` R ) ) y ) e. I ) ) )
10	4	opprsubg	|- ( SubGrp ` R ) = ( SubGrp ` ( oppR ` R ) )
11	10	eqcomi	|- ( SubGrp ` ( oppR ` R ) ) = ( SubGrp ` R )
12	11	a1i	|- ( R e. Ring -> ( SubGrp ` ( oppR ` R ) ) = ( SubGrp ` R ) )
13	12	eleq2d	|- ( R e. Ring -> ( I e. ( SubGrp ` ( oppR ` R ) ) <-> I e. ( SubGrp ` R ) ) )
14	2 3 4 7	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. Ring /\ x e. B ) /\ y e. I ) -> ( ( x ( .r ` ( oppR ` R ) ) y ) e. I <-> ( y .x. x ) e. I ) )
17	16	ralbidva	|- ( ( R e. Ring /\ 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. Ring -> ( 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	anbi12d	|- ( R e. Ring -> ( ( I e. ( SubGrp ` ( oppR ` R ) ) /\ A. x e. B A. y e. I ( x ( .r ` ( oppR ` R ) ) y ) e. I ) <-> ( I e. ( SubGrp ` R ) /\ A. x e. B A. y e. I ( y .x. x ) e. I ) ) )
20	9 19	bitrd	|- ( R e. Ring -> ( I e. U <-> ( I e. ( SubGrp ` R ) /\ A. x e. B A. y e. I ( y .x. x ) e. I ) ) )