Theorem 2idlbas

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

	Ref	Expression
Hypotheses	2idlbas.i	$$⊢\phi \to I\in \mathrm{2Ideal}\left(R\right)$$
	2idlbas.j	$$⊢J=R{\upharpoonright }_{𝑠}I$$
	2idlbas.b	$$⊢B={\mathrm{Base}}_J$$
Assertion	2idlbas	$$⊢\phi \to B=I$$

Proof

Step	Hyp	Ref	Expression
1		2idlbas.i	$$⊢\phi \to I\in \mathrm{2Ideal}\left(R\right)$$
2		2idlbas.j	$$⊢J=R{\upharpoonright }_{𝑠}I$$
3		2idlbas.b	$$⊢B={\mathrm{Base}}_J$$
4		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
5		eqid	$$⊢\mathrm{2Ideal}\left(R\right)=\mathrm{2Ideal}\left(R\right)$$
6	4 5	2idlss	$$⊢I\in \mathrm{2Ideal}\left(R\right)\to I\subseteq {\mathrm{Base}}_R$$
7	2 4	ressbas2	$$⊢I\subseteq {\mathrm{Base}}_R\to I={\mathrm{Base}}_J$$
8	1 6 7	3syl	$$⊢\phi \to I={\mathrm{Base}}_J$$
9	3 8	eqtr4id	$$⊢\phi \to B=I$$