Theorem rngqiprngfu

Description: The function value of F at the constructed expected ring unity of R is the ring unity of the product of the quotient with the two-sided ideal and the two-sided ideal. (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}$$
	rngqiprngfu.f	$$⊢F=\left(x\in B⟼⟨\left[x\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}x⟩\right)$$
Assertion	rngqiprngfu	$$⊢\phi \to F\left(U\right)=⟨\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		rngqiprngfu.f	$$⊢F=\left(x\in B⟼⟨\left[x\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}x⟩\right)$$
16	1 2 3 4 5 6 7 8 9 10 11 12 13 14	rngqiprngfulem3	$$⊢\phi \to U\in B$$
17		eqid	$$⊢{\mathrm{Base}}_Q={\mathrm{Base}}_Q$$
18		eqid	$$⊢Q{\times }_{𝑠}J=Q{\times }_{𝑠}J$$
19	1 2 3 4 5 6 7 8 9 17 18 15	rngqiprngimfv	$$⊢\left(\phi \wedge U\in B\right)\to F\left(U\right)=⟨\left[U\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}U⟩$$
20	16 19	mpdan	$$⊢\phi \to F\left(U\right)=⟨\left[U\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}U⟩$$
21	1 2 3 4 5 6 7 8 9 10 11 12 13 14	rngqiprngfulem4	$$⊢\phi \to \left[U\right]\underset{\dot{}}{\sim }=\left[E\right]\underset{\dot{}}{\sim }$$
22	1 2 3 4 5 6 7 8 9 10 11 12 13 14	rngqiprngfulem5	$$⊢\phi \to \underset{\dot{}}{1}\underset{\dot{}}{·}U=\underset{\dot{}}{1}$$
23	21 22	opeq12d	$$⊢\phi \to ⟨\left[U\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}U⟩=⟨\left[E\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}⟩$$
24	20 23	eqtrd	$$⊢\phi \to F\left(U\right)=⟨\left[E\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}⟩$$