Theorem 2idlbas

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

	Ref	Expression
Hypotheses	2idlbas.i	|- ( ph -> I e. ( 2Ideal ` R ) )
	2idlbas.j	|- J = ( R |`s I )
	2idlbas.b	|- B = ( Base ` J )
Assertion	2idlbas	|- ( ph -> B = I )

Proof

Step	Hyp	Ref	Expression
1		2idlbas.i	|- ( ph -> I e. ( 2Ideal ` R ) )
2		2idlbas.j	|- J = ( R |`s I )
3		2idlbas.b	|- B = ( Base ` J )
4		eqid	|- ( Base ` R ) = ( Base ` R )
5		eqid	|- ( 2Ideal ` R ) = ( 2Ideal ` R )
6	4 5	2idlss	|- ( I e. ( 2Ideal ` R ) -> I C_ ( Base ` R ) )
7	2 4	ressbas2	|- ( I C_ ( Base ` R ) -> I = ( Base ` J ) )
8	1 6 7	3syl	|- ( ph -> I = ( Base ` J ) )
9	3 8	eqtr4id	|- ( ph -> B = I )