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

Proof

Step	Hyp	Ref	Expression
1		isridl.u	$⊢ U = LIdeal ({opp}_{r} (R))$
2		isridl.b	$⊢ B = {Base}_{R}$
3		isridl.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		eqid	$⊢ {opp}_{r} (R) = {opp}_{r} (R)$
5	4	opprring	$⊢ R \in Ring \to {opp}_{r} (R) \in Ring$
6	4 2	opprbas	$⊢ B = {Base}_{{opp}_{r} (R)}$
7		eqid	$⊢ \cdot_{{opp}_{r} (R)} = \cdot_{{opp}_{r} (R)}$
8	1 6 7	dflidl2	$⊢ {opp}_{r} (R) \in Ring \to (I \in U \leftrightarrow (I \in SubGrp ({opp}_{r} (R)) \land \forall x \in B \forall y \in I x \cdot_{{opp}_{r} (R)} y \in I))$
9	5 8	syl	$⊢ R \in Ring \to (I \in U \leftrightarrow (I \in SubGrp ({opp}_{r} (R)) \land \forall x \in B \forall y \in I x \cdot_{{opp}_{r} (R)} y \in I))$
10	4	opprsubg	$⊢ SubGrp (R) = SubGrp ({opp}_{r} (R))$
11	10	eqcomi	$⊢ SubGrp ({opp}_{r} (R)) = SubGrp (R)$
12	11	a1i	$⊢ R \in Ring \to SubGrp ({opp}_{r} (R)) = SubGrp (R)$
13	12	eleq2d	$⊢ R \in Ring \to (I \in SubGrp ({opp}_{r} (R)) \leftrightarrow I \in SubGrp (R))$
14	2 3 4 7	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 Ring \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 Ring \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 Ring \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	anbi12d	$⊢ R \in Ring \to ((I \in SubGrp ({opp}_{r} (R)) \land \forall x \in B \forall y \in I x \cdot_{{opp}_{r} (R)} y \in I) \leftrightarrow (I \in SubGrp (R) \land \forall x \in B \forall y \in I y \underset{˙}{\cdot} x \in I))$
20	9 19	bitrd	$⊢ R \in Ring \to (I \in U \leftrightarrow (I \in SubGrp (R) \land \forall x \in B \forall y \in I y \underset{˙}{\cdot} x \in I))$

Metamath Proof Explorer

Theorem isridl

Proof