Theorem 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	⊢ ( 𝜑 → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
	2idlbas.j	⊢ 𝐽 = ( 𝑅 ↾s 𝐼 )
	2idlbas.b	⊢ 𝐵 = ( Base ‘ 𝐽 )
Assertion	2idlelbas	⊢ ( 𝜑 → ( 𝐵 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐵 ∈ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		2idlbas.i	⊢ ( 𝜑 → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
2		2idlbas.j	⊢ 𝐽 = ( 𝑅 ↾s 𝐼 )
3		2idlbas.b	⊢ 𝐵 = ( Base ‘ 𝐽 )
4	1 2 3	2idlbas	⊢ ( 𝜑 → 𝐵 = 𝐼 )
5		eqid	⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
6		eqid	⊢ ( oppr ‘ 𝑅 ) = ( oppr ‘ 𝑅 )
7		eqid	⊢ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) = ( LIdeal ‘ ( oppr ‘ 𝑅 ) )
8		eqid	⊢ ( 2Ideal ‘ 𝑅 ) = ( 2Ideal ‘ 𝑅 )
9	5 6 7 8	2idlelb	⊢ ( 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) ↔ ( 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ∈ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) ) )
10	9	simplbi	⊢ ( 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) → 𝐼 ∈ ( LIdeal ‘ 𝑅 ) )
11	1 10	syl	⊢ ( 𝜑 → 𝐼 ∈ ( LIdeal ‘ 𝑅 ) )
12	4 11	eqeltrd	⊢ ( 𝜑 → 𝐵 ∈ ( LIdeal ‘ 𝑅 ) )
13	9	simprbi	⊢ ( 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) → 𝐼 ∈ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) )
14	1 13	syl	⊢ ( 𝜑 → 𝐼 ∈ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) )
15	4 14	eqeltrd	⊢ ( 𝜑 → 𝐵 ∈ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) )
16	12 15	jca	⊢ ( 𝜑 → ( 𝐵 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐵 ∈ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) ) )