Theorem rngqipring1

Description: The ring unity of the product of the quotient with a two-sided ideal and the two-sided ideal, which both are rings. (Contributed by AV, 16-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}$$
	rngqipring1.p	$$⊢P=Q{\times }_{𝑠}J$$
Assertion	rngqipring1	$$⊢\phi \to 1_P=⟨\left[E\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}⟩$$

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		rngqipring1.p	$$⊢P=Q{\times }_{𝑠}J$$
16	15 10 4	xpsring1d	$$⊢\phi \to 1_P=⟨1_Q,1_J⟩$$
17	11	adantr	$$⊢\left(\phi \wedge x\in B\right)\to E\in 1_Q$$
18		eleq2	$$⊢1_Q=\left[x\right]\underset{\dot{}}{\sim }\to \left(E\in 1_Q\leftrightarrow E\in \left[x\right]\underset{\dot{}}{\sim }\right)$$
19	18	adantl	$$⊢\left(\left(\phi \wedge x\in B\right)\wedge 1_Q=\left[x\right]\underset{\dot{}}{\sim }\right)\to \left(E\in 1_Q\leftrightarrow E\in \left[x\right]\underset{\dot{}}{\sim }\right)$$
20		elecg	$$⊢\left(E\in 1_Q\wedge x\in B\right)\to \left(E\in \left[x\right]\underset{\dot{}}{\sim }\leftrightarrow x\underset{\dot{}}{\sim }E\right)$$
21	11 20	sylan	$$⊢\left(\phi \wedge x\in B\right)\to \left(E\in \left[x\right]\underset{\dot{}}{\sim }\leftrightarrow x\underset{\dot{}}{\sim }E\right)$$
22		ringrng	$$⊢J\in \mathrm{Ring}\to J\in \mathrm{Rng}$$
23	4 22	syl	$$⊢\phi \to J\in \mathrm{Rng}$$
24	3 23	eqeltrrid	$$⊢\phi \to R{\upharpoonright }_{𝑠}I\in \mathrm{Rng}$$
25	1 2 24	rng2idlnsg	$$⊢\phi \to I\in \mathrm{NrmSGrp}\left(R\right)$$
26		nsgsubg	$$⊢I\in \mathrm{NrmSGrp}\left(R\right)\to I\in \mathrm{SubGrp}\left(R\right)$$
27	25 26	syl	$$⊢\phi \to I\in \mathrm{SubGrp}\left(R\right)$$
28	27	adantr	$$⊢\left(\phi \wedge x\in B\right)\to I\in \mathrm{SubGrp}\left(R\right)$$
29	5 8	eqger	$$⊢I\in \mathrm{SubGrp}\left(R\right)\to \underset{\dot{}}{\sim }\mathrm{Er}B$$
30	28 29	syl	$$⊢\left(\phi \wedge x\in B\right)\to \underset{\dot{}}{\sim }\mathrm{Er}B$$
31		simpr	$$⊢\left(\phi \wedge x\in B\right)\to x\in B$$
32	30 31	erth	$$⊢\left(\phi \wedge x\in B\right)\to \left(x\underset{\dot{}}{\sim }E\leftrightarrow \left[x\right]\underset{\dot{}}{\sim }=\left[E\right]\underset{\dot{}}{\sim }\right)$$
33	32	biimpa	$$⊢\left(\left(\phi \wedge x\in B\right)\wedge x\underset{\dot{}}{\sim }E\right)\to \left[x\right]\underset{\dot{}}{\sim }=\left[E\right]\underset{\dot{}}{\sim }$$
34	33	eqcomd	$$⊢\left(\left(\phi \wedge x\in B\right)\wedge x\underset{\dot{}}{\sim }E\right)\to \left[E\right]\underset{\dot{}}{\sim }=\left[x\right]\underset{\dot{}}{\sim }$$
35	34	ex	$$⊢\left(\phi \wedge x\in B\right)\to \left(x\underset{\dot{}}{\sim }E\to \left[E\right]\underset{\dot{}}{\sim }=\left[x\right]\underset{\dot{}}{\sim }\right)$$
36	21 35	sylbid	$$⊢\left(\phi \wedge x\in B\right)\to \left(E\in \left[x\right]\underset{\dot{}}{\sim }\to \left[E\right]\underset{\dot{}}{\sim }=\left[x\right]\underset{\dot{}}{\sim }\right)$$
37	36	adantr	$$⊢\left(\left(\phi \wedge x\in B\right)\wedge 1_Q=\left[x\right]\underset{\dot{}}{\sim }\right)\to \left(E\in \left[x\right]\underset{\dot{}}{\sim }\to \left[E\right]\underset{\dot{}}{\sim }=\left[x\right]\underset{\dot{}}{\sim }\right)$$
38	19 37	sylbid	$$⊢\left(\left(\phi \wedge x\in B\right)\wedge 1_Q=\left[x\right]\underset{\dot{}}{\sim }\right)\to \left(E\in 1_Q\to \left[E\right]\underset{\dot{}}{\sim }=\left[x\right]\underset{\dot{}}{\sim }\right)$$
39	38	ex	$$⊢\left(\phi \wedge x\in B\right)\to \left(1_Q=\left[x\right]\underset{\dot{}}{\sim }\to \left(E\in 1_Q\to \left[E\right]\underset{\dot{}}{\sim }=\left[x\right]\underset{\dot{}}{\sim }\right)\right)$$
40	17 39	mpid	$$⊢\left(\phi \wedge x\in B\right)\to \left(1_Q=\left[x\right]\underset{\dot{}}{\sim }\to \left[E\right]\underset{\dot{}}{\sim }=\left[x\right]\underset{\dot{}}{\sim }\right)$$
41	40	imp	$$⊢\left(\left(\phi \wedge x\in B\right)\wedge 1_Q=\left[x\right]\underset{\dot{}}{\sim }\right)\to \left[E\right]\underset{\dot{}}{\sim }=\left[x\right]\underset{\dot{}}{\sim }$$
42		simpr	$$⊢\left(\left(\phi \wedge x\in B\right)\wedge 1_Q=\left[x\right]\underset{\dot{}}{\sim }\right)\to 1_Q=\left[x\right]\underset{\dot{}}{\sim }$$
43	41 42	eqtr4d	$$⊢\left(\left(\phi \wedge x\in B\right)\wedge 1_Q=\left[x\right]\underset{\dot{}}{\sim }\right)\to \left[E\right]\underset{\dot{}}{\sim }=1_Q$$
44	1 2 3 4 5 6 7 8 9 10	rngqiprngfulem1	$$⊢\phi \to \exists x\in B{1}_Q=\left[x\right]\underset{\dot{}}{\sim }$$
45	43 44	r19.29a	$$⊢\phi \to \left[E\right]\underset{\dot{}}{\sim }=1_Q$$
46	45	eqcomd	$$⊢\phi \to 1_Q=\left[E\right]\underset{\dot{}}{\sim }$$
47	7	eqcomi	$$⊢1_J=\underset{\dot{}}{1}$$
48	47	a1i	$$⊢\phi \to 1_J=\underset{\dot{}}{1}$$
49	46 48	opeq12d	$$⊢\phi \to ⟨1_Q,1_J⟩=⟨\left[E\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}⟩$$
50	16 49	eqtrd	$$⊢\phi \to 1_P=⟨\left[E\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}⟩$$