2idlelbas

Description: The base set of a two-sided ideal as structure is a left and right ideal. (Contributed by AV, 20-Feb-2025)

	Ref	Expression
Hypotheses	2idlbas.i	$⊢ φ \to I \in 2Ideal (R)$
	2idlbas.j	$⊢ J = R ↾_{𝑠} I$
	2idlbas.b	$⊢ B = {Base}_{J}$
Assertion	2idlelbas	$⊢ φ \to (B \in LIdeal (R) \land B \in LIdeal ({opp}_{r} (R)))$

Step	Hyp	Ref	Expression
1		2idlbas.i	$⊢ φ \to I \in 2Ideal (R)$
2		2idlbas.j	$⊢ J = R ↾_{𝑠} I$
3		2idlbas.b	$⊢ B = {Base}_{J}$
4	1 2 3	2idlbas	$⊢ φ \to B = I$
5		eqid	$⊢ LIdeal (R) = LIdeal (R)$
6		eqid	$⊢ {opp}_{r} (R) = {opp}_{r} (R)$
7		eqid	$⊢ LIdeal ({opp}_{r} (R)) = LIdeal ({opp}_{r} (R))$
8		eqid	$⊢ 2Ideal (R) = 2Ideal (R)$
9	5 6 7 8	2idlelb	$⊢ I \in 2Ideal (R) \leftrightarrow (I \in LIdeal (R) \land I \in LIdeal ({opp}_{r} (R)))$
10	9	simplbi	$⊢ I \in 2Ideal (R) \to I \in LIdeal (R)$
11	1 10	syl	$⊢ φ \to I \in LIdeal (R)$
12	4 11	eqeltrd	$⊢ φ \to B \in LIdeal (R)$
13	9	simprbi	$⊢ I \in 2Ideal (R) \to I \in LIdeal ({opp}_{r} (R))$
14	1 13	syl	$⊢ φ \to I \in LIdeal ({opp}_{r} (R))$
15	4 14	eqeltrd	$⊢ φ \to B \in LIdeal ({opp}_{r} (R))$
16	12 15	jca	$⊢ φ \to (B \in LIdeal (R) \land B \in LIdeal ({opp}_{r} (R)))$

Metamath Proof Explorer