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	$$⊢\phi \to R\in \mathrm{Rng}$$
	rng2idlring.i	$$⊢\phi \to I\in \mathrm{2Ideal}\left(R\right)$$
	rng2idlring.j	$$⊢J=R{\upharpoonright }_{𝑠}I$$
	rng2idlring.u	$$⊢\phi \to J\in \mathrm{Ring}$$
	rng2idlring.b	$$⊢B={\mathrm{Base}}_R$$
	rng2idlring.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	rng2idlring.1	$$⊢\underset{\dot{}}{1}=1_J$$
Assertion	rngqiprng1elbas	$$⊢\phi \to \underset{\dot{}}{1}\in B$$

Proof

Step	Hyp	Ref	Expression
1		rng2idlring.r	$$⊢\phi \to R\in \mathrm{Rng}$$
2		rng2idlring.i	$$⊢\phi \to I\in \mathrm{2Ideal}\left(R\right)$$
3		rng2idlring.j	$$⊢J=R{\upharpoonright }_{𝑠}I$$
4		rng2idlring.u	$$⊢\phi \to J\in \mathrm{Ring}$$
5		rng2idlring.b	$$⊢B={\mathrm{Base}}_R$$
6		rng2idlring.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
7		rng2idlring.1	$$⊢\underset{\dot{}}{1}=1_J$$
8	3 5	ressbasss	$$⊢{\mathrm{Base}}_J\subseteq B$$
9		eqid	$$⊢{\mathrm{Base}}_J={\mathrm{Base}}_J$$
10	9 7	ringidcl	$$⊢J\in \mathrm{Ring}\to \underset{\dot{}}{1}\in {\mathrm{Base}}_J$$
11	4 10	syl	$$⊢\phi \to \underset{\dot{}}{1}\in {\mathrm{Base}}_J$$
12	8 11	sselid	$$⊢\phi \to \underset{\dot{}}{1}\in B$$