Metamath Proof Explorer


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=LIdealopprR
isridlrng.b B=BaseR
isridlrng.t ·˙=R
Assertion isridlrng RRngISubGrpRIUxByIy·˙xI

Proof

Step Hyp Ref Expression
1 isridlrng.u U=LIdealopprR
2 isridlrng.b B=BaseR
3 isridlrng.t ·˙=R
4 eqid opprR=opprR
5 4 opprrng RRngopprRRng
6 4 opprsubg SubGrpR=SubGrpopprR
7 6 a1i RRngSubGrpR=SubGrpopprR
8 7 eleq2d RRngISubGrpRISubGrpopprR
9 8 biimpa RRngISubGrpRISubGrpopprR
10 4 2 opprbas B=BaseopprR
11 eqid opprR=opprR
12 1 10 11 dflidl2rng opprRRngISubGrpopprRIUxByIxopprRyI
13 5 9 12 syl2an2r RRngISubGrpRIUxByIxopprRyI
14 2 3 4 11 opprmul xopprRy=y·˙x
15 14 eleq1i xopprRyIy·˙xI
16 15 a1i RRngISubGrpRxByIxopprRyIy·˙xI
17 16 ralbidva RRngISubGrpRxByIxopprRyIyIy·˙xI
18 17 ralbidva RRngISubGrpRxByIxopprRyIxByIy·˙xI
19 13 18 bitrd RRngISubGrpRIUxByIy·˙xI