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

Metamath Proof Explorer

Theorem 2idlbas

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

Ref Expression
Hypotheses 2idlbas.i ⊢ φ → I ∈ 2Ideal ⁡ R
2idlbas.j ⊢ J = R ↾ 𝑠 I
2idlbas.b ⊢ B = Base J
Assertion 2idlbas ⊢ φ → B = I

Proof

Step Hyp Ref Expression
1 2idlbas.i ⊢ φ → I ∈ 2Ideal ⁡ R
2 2idlbas.j ⊢ J = R ↾ 𝑠 I
3 2idlbas.b ⊢ B = Base J
4 eqid ⊢ Base R = Base R
5 eqid ⊢ 2Ideal ⁡ R = 2Ideal ⁡ R
6 4 5 2idlss ⊢ I ∈ 2Ideal ⁡ R → I ⊆ Base R
7 2 4 ressbas2 ⊢ I ⊆ Base R → I = Base J
8 1 6 7 3syl ⊢ φ → I = Base J
9 3 8 eqtr4id ⊢ φ → B = I