This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑅 ) ) ) )