Theorem rngqiprng1elbas

Description: The ring unity of a two-sided ideal of a non-unital ring belongs to the base set of the ring. (Contributed by AV, 15-Mar-2025)

	Ref	Expression
Hypotheses	rng2idlring.r	|- ( ph -> R e. Rng )
	rng2idlring.i	|- ( ph -> I e. ( 2Ideal ` R ) )
	rng2idlring.j	|- J = ( R |`s I )
	rng2idlring.u	|- ( ph -> J e. Ring )
	rng2idlring.b	|- B = ( Base ` R )
	rng2idlring.t	|- .x. = ( .r ` R )
	rng2idlring.1	|- .1. = ( 1r ` J )
Assertion	rngqiprng1elbas	|- ( ph -> .1. e. B )

Proof

Step	Hyp	Ref	Expression
1		rng2idlring.r	|- ( ph -> R e. Rng )
2		rng2idlring.i	|- ( ph -> I e. ( 2Ideal ` R ) )
3		rng2idlring.j	|- J = ( R |`s I )
4		rng2idlring.u	|- ( ph -> J e. Ring )
5		rng2idlring.b	|- B = ( Base ` R )
6		rng2idlring.t	|- .x. = ( .r ` R )
7		rng2idlring.1	|- .1. = ( 1r ` J )
8	3 5	ressbasss	|- ( Base ` J ) C_ B
9		eqid	|- ( Base ` J ) = ( Base ` J )
10	9 7	ringidcl	|- ( J e. Ring -> .1. e. ( Base ` J ) )
11	4 10	syl	|- ( ph -> .1. e. ( Base ` J ) )
12	8 11	sselid	|- ( ph -> .1. e. B )