Theorem 2idlbas

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

	Ref	Expression
Hypotheses	2idlbas.i	⊢ ( 𝜑 → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
	2idlbas.j	⊢ 𝐽 = ( 𝑅 ↾s 𝐼 )
	2idlbas.b	⊢ 𝐵 = ( Base ‘ 𝐽 )
Assertion	2idlbas	⊢ ( 𝜑 → 𝐵 = 𝐼 )

Proof

Step	Hyp	Ref	Expression
1		2idlbas.i	⊢ ( 𝜑 → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
2		2idlbas.j	⊢ 𝐽 = ( 𝑅 ↾s 𝐼 )
3		2idlbas.b	⊢ 𝐵 = ( Base ‘ 𝐽 )
4		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
5		eqid	⊢ ( 2Ideal ‘ 𝑅 ) = ( 2Ideal ‘ 𝑅 )
6	4 5	2idlss	⊢ ( 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) → 𝐼 ⊆ ( Base ‘ 𝑅 ) )
7	2 4	ressbas2	⊢ ( 𝐼 ⊆ ( Base ‘ 𝑅 ) → 𝐼 = ( Base ‘ 𝐽 ) )
8	1 6 7	3syl	⊢ ( 𝜑 → 𝐼 = ( Base ‘ 𝐽 ) )
9	3 8	eqtr4id	⊢ ( 𝜑 → 𝐵 = 𝐼 )