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 ({opp}_{r} (R))$
	isridlrng.b	$⊢ B = {Base}_{R}$
	isridlrng.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
Assertion	isridlrng	$⊢ (R \in Rng \land I \in SubGrp (R)) \to (I \in U \leftrightarrow \forall x \in B \forall y \in I y \underset{˙}{\cdot} x \in I)$

Proof

Step	Hyp	Ref	Expression
1		isridlrng.u	$⊢ U = LIdeal ({opp}_{r} (R))$
2		isridlrng.b	$⊢ B = {Base}_{R}$
3		isridlrng.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		eqid	$⊢ {opp}_{r} (R) = {opp}_{r} (R)$
5	4	opprrng	$⊢ R \in Rng \to {opp}_{r} (R) \in Rng$
6	4	opprsubg	$⊢ SubGrp (R) = SubGrp ({opp}_{r} (R))$
7	6	a1i	$⊢ R \in Rng \to SubGrp (R) = SubGrp ({opp}_{r} (R))$
8	7	eleq2d	$⊢ R \in Rng \to (I \in SubGrp (R) \leftrightarrow I \in SubGrp ({opp}_{r} (R)))$
9	8	biimpa	$⊢ (R \in Rng \land I \in SubGrp (R)) \to I \in SubGrp ({opp}_{r} (R))$
10	4 2	opprbas	$⊢ B = {Base}_{{opp}_{r} (R)}$
11		eqid	$⊢ \cdot_{{opp}_{r} (R)} = \cdot_{{opp}_{r} (R)}$
12	1 10 11	dflidl2rng	$⊢ ({opp}_{r} (R) \in Rng \land I \in SubGrp ({opp}_{r} (R))) \to (I \in U \leftrightarrow \forall x \in B \forall y \in I x \cdot_{{opp}_{r} (R)} y \in I)$
13	5 9 12	syl2an2r	$⊢ (R \in Rng \land I \in SubGrp (R)) \to (I \in U \leftrightarrow \forall x \in B \forall y \in I x \cdot_{{opp}_{r} (R)} y \in I)$
14	2 3 4 11	opprmul	$⊢ x \cdot_{{opp}_{r} (R)} y = y \underset{˙}{\cdot} x$
15	14	eleq1i	$⊢ x \cdot_{{opp}_{r} (R)} y \in I \leftrightarrow y \underset{˙}{\cdot} x \in I$
16	15	a1i	$⊢ (((R \in Rng \land I \in SubGrp (R)) \land x \in B) \land y \in I) \to (x \cdot_{{opp}_{r} (R)} y \in I \leftrightarrow y \underset{˙}{\cdot} x \in I)$
17	16	ralbidva	$⊢ ((R \in Rng \land I \in SubGrp (R)) \land x \in B) \to (\forall y \in I x \cdot_{{opp}_{r} (R)} y \in I \leftrightarrow \forall y \in I y \underset{˙}{\cdot} x \in I)$
18	17	ralbidva	$⊢ (R \in Rng \land I \in SubGrp (R)) \to (\forall x \in B \forall y \in I x \cdot_{{opp}_{r} (R)} y \in I \leftrightarrow \forall x \in B \forall y \in I y \underset{˙}{\cdot} x \in I)$
19	13 18	bitrd	$⊢ (R \in Rng \land I \in SubGrp (R)) \to (I \in U \leftrightarrow \forall x \in B \forall y \in I y \underset{˙}{\cdot} x \in I)$

Metamath Proof Explorer

Theorem isridlrng

Proof