Theorem rngqiprngu

Description: If a non-unital ring has a (two-sided) ideal which is unital, and the quotient of the ring and the ideal is also unital, then the ring is also unital with a ring unity which can be constructed from the ring unity of the ideal and a representative of the ring unity of the quotient. (Contributed by AV, 17-Mar-2025)

	Ref	Expression
Hypotheses	rngqiprngfu.r	$$⊢\phi \to R\in \mathrm{Rng}$$
	rngqiprngfu.i	$$⊢\phi \to I\in \mathrm{2Ideal}\left(R\right)$$
	rngqiprngfu.j	$$⊢J=R{\upharpoonright }_{𝑠}I$$
	rngqiprngfu.u	$$⊢\phi \to J\in \mathrm{Ring}$$
	rngqiprngfu.b	$$⊢B={\mathrm{Base}}_R$$
	rngqiprngfu.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	rngqiprngfu.1	$$⊢\underset{\dot{}}{1}=1_J$$
	rngqiprngfu.g	$$⊢\underset{\dot{}}{\sim }=R{~}_{\mathit{QG}}I$$
	rngqiprngfu.q	$$⊢Q=R{/}_{𝑠}\underset{\dot{}}{\sim }$$
	rngqiprngfu.v	$$⊢\phi \to Q\in \mathrm{Ring}$$
	rngqiprngfu.e	$$⊢\phi \to E\in 1_Q$$
	rngqiprngfu.m	$$⊢\underset{\dot{}}{-}={-}_R$$
	rngqiprngfu.a	$$⊢\underset{\dot{}}{+}={+}_R$$
	rngqiprngfu.n	$$⊢U=\left(E\underset{\dot{}}{-}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}E\right)\right)\underset{\dot{}}{+}\underset{\dot{}}{1}$$
Assertion	rngqiprngu	$$⊢\phi \to 1_R=U$$

Proof

Step	Hyp	Ref	Expression
1		rngqiprngfu.r	$$⊢\phi \to R\in \mathrm{Rng}$$
2		rngqiprngfu.i	$$⊢\phi \to I\in \mathrm{2Ideal}\left(R\right)$$
3		rngqiprngfu.j	$$⊢J=R{\upharpoonright }_{𝑠}I$$
4		rngqiprngfu.u	$$⊢\phi \to J\in \mathrm{Ring}$$
5		rngqiprngfu.b	$$⊢B={\mathrm{Base}}_R$$
6		rngqiprngfu.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
7		rngqiprngfu.1	$$⊢\underset{\dot{}}{1}=1_J$$
8		rngqiprngfu.g	$$⊢\underset{\dot{}}{\sim }=R{~}_{\mathit{QG}}I$$
9		rngqiprngfu.q	$$⊢Q=R{/}_{𝑠}\underset{\dot{}}{\sim }$$
10		rngqiprngfu.v	$$⊢\phi \to Q\in \mathrm{Ring}$$
11		rngqiprngfu.e	$$⊢\phi \to E\in 1_Q$$
12		rngqiprngfu.m	$$⊢\underset{\dot{}}{-}={-}_R$$
13		rngqiprngfu.a	$$⊢\underset{\dot{}}{+}={+}_R$$
14		rngqiprngfu.n	$$⊢U=\left(E\underset{\dot{}}{-}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}E\right)\right)\underset{\dot{}}{+}\underset{\dot{}}{1}$$
15		eqid	$$⊢Q{\times }_{𝑠}J=Q{\times }_{𝑠}J$$
16	15 10 4	xpsringd	$$⊢\phi \to Q{\times }_{𝑠}J\in \mathrm{Ring}$$
17		eqid	$$⊢{\mathrm{Base}}_Q={\mathrm{Base}}_Q$$
18		eqid	$$⊢\left(x\in B⟼⟨\left[x\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}x⟩\right)=\left(x\in B⟼⟨\left[x\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}x⟩\right)$$
19	1 2 3 4 5 6 7 8 9 17 15 18	rngqiprngim	$$⊢\phi \to \left(x\in B⟼⟨\left[x\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}x⟩\right)\in \left(R\mathrm{RngIso}\left(Q{\times }_{𝑠}J\right)\right)$$
20		rngimcnv	$$⊢\left(x\in B⟼⟨\left[x\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}x⟩\right)\in \left(R\mathrm{RngIso}\left(Q{\times }_{𝑠}J\right)\right)\to {\left(x\in B⟼⟨\left[x\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}x⟩\right)}^{-1}\in \left(\left(Q{\times }_{𝑠}J\right)\mathrm{RngIso}R\right)$$
21	19 20	syl	$$⊢\phi \to {\left(x\in B⟼⟨\left[x\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}x⟩\right)}^{-1}\in \left(\left(Q{\times }_{𝑠}J\right)\mathrm{RngIso}R\right)$$
22		rngisomring1	$$⊢\left(Q{\times }_{𝑠}J\in \mathrm{Ring}\wedge R\in \mathrm{Rng}\wedge {\left(x\in B⟼⟨\left[x\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}x⟩\right)}^{-1}\in \left(\left(Q{\times }_{𝑠}J\right)\mathrm{RngIso}R\right)\right)\to 1_R={\left(x\in B⟼⟨\left[x\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}x⟩\right)}^{-1}\left(1_{\left(Q{\times }_{𝑠}J\right)}\right)$$
23	16 1 21 22	syl3anc	$$⊢\phi \to 1_R={\left(x\in B⟼⟨\left[x\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}x⟩\right)}^{-1}\left(1_{\left(Q{\times }_{𝑠}J\right)}\right)$$
24	1 2 3 4 5 6 7 8 9 10 11 12 13 14 18	rngqiprngfu	$$⊢\phi \to \left(x\in B⟼⟨\left[x\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}x⟩\right)\left(U\right)=⟨\left[E\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}⟩$$
25	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15	rngqipring1	$$⊢\phi \to 1_{\left(Q{\times }_{𝑠}J\right)}=⟨\left[E\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}⟩$$
26	24 25	eqtr4d	$$⊢\phi \to \left(x\in B⟼⟨\left[x\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}x⟩\right)\left(U\right)=1_{\left(Q{\times }_{𝑠}J\right)}$$
27		eqid	$$⊢{\mathrm{Base}}_{\left(Q{\times }_{𝑠}J\right)}={\mathrm{Base}}_{\left(Q{\times }_{𝑠}J\right)}$$
28	5 27	rngimf1o	$$⊢\left(x\in B⟼⟨\left[x\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}x⟩\right)\in \left(R\mathrm{RngIso}\left(Q{\times }_{𝑠}J\right)\right)\to \left(x\in B⟼⟨\left[x\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}x⟩\right):B\underset{1-1\; onto}{⟶}{\mathrm{Base}}_{\left(Q{\times }_{𝑠}J\right)}$$
29	19 28	syl	$$⊢\phi \to \left(x\in B⟼⟨\left[x\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}x⟩\right):B\underset{1-1\; onto}{⟶}{\mathrm{Base}}_{\left(Q{\times }_{𝑠}J\right)}$$
30	1 2 3 4 5 6 7 8 9 10 11 12 13 14	rngqiprngfulem3	$$⊢\phi \to U\in B$$
31		eqid	$$⊢1_{\left(Q{\times }_{𝑠}J\right)}=1_{\left(Q{\times }_{𝑠}J\right)}$$
32	27 31	ringidcl	$$⊢Q{\times }_{𝑠}J\in \mathrm{Ring}\to 1_{\left(Q{\times }_{𝑠}J\right)}\in {\mathrm{Base}}_{\left(Q{\times }_{𝑠}J\right)}$$
33	16 32	syl	$$⊢\phi \to 1_{\left(Q{\times }_{𝑠}J\right)}\in {\mathrm{Base}}_{\left(Q{\times }_{𝑠}J\right)}$$
34		f1ocnvfvb	$$⊢\left(\left(x\in B⟼⟨\left[x\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}x⟩\right):B\underset{1-1\; onto}{⟶}{\mathrm{Base}}_{\left(Q{\times }_{𝑠}J\right)}\wedge U\in B\wedge 1_{\left(Q{\times }_{𝑠}J\right)}\in {\mathrm{Base}}_{\left(Q{\times }_{𝑠}J\right)}\right)\to \left(\left(x\in B⟼⟨\left[x\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}x⟩\right)\left(U\right)=1_{\left(Q{\times }_{𝑠}J\right)}\leftrightarrow {\left(x\in B⟼⟨\left[x\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}x⟩\right)}^{-1}\left(1_{\left(Q{\times }_{𝑠}J\right)}\right)=U\right)$$
35	29 30 33 34	syl3anc	$$⊢\phi \to \left(\left(x\in B⟼⟨\left[x\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}x⟩\right)\left(U\right)=1_{\left(Q{\times }_{𝑠}J\right)}\leftrightarrow {\left(x\in B⟼⟨\left[x\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}x⟩\right)}^{-1}\left(1_{\left(Q{\times }_{𝑠}J\right)}\right)=U\right)$$
36	26 35	mpbid	$$⊢\phi \to {\left(x\in B⟼⟨\left[x\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}x⟩\right)}^{-1}\left(1_{\left(Q{\times }_{𝑠}J\right)}\right)=U$$
37	23 36	eqtrd	$$⊢\phi \to 1_R=U$$