Theorem rngqiprngim

Description: F is an isomorphism of non-unital rings. (Contributed by AV, 21-Feb-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$$
	rngqiprngim.g	$$⊢\underset{\dot{}}{\sim }=R{~}_{\mathit{QG}}I$$
	rngqiprngim.q	$$⊢Q=R{/}_{𝑠}\underset{\dot{}}{\sim }$$
	rngqiprngim.c	$$⊢C={\mathrm{Base}}_Q$$
	rngqiprngim.p	$$⊢P=Q{\times }_{𝑠}J$$
	rngqiprngim.f	$$⊢F=\left(x\in B⟼⟨\left[x\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}x⟩\right)$$
Assertion	rngqiprngim	$$⊢\phi \to F\in \left(R\mathrm{RngIso}P\right)$$

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		rngqiprngim.g	$$⊢\underset{\dot{}}{\sim }=R{~}_{\mathit{QG}}I$$
9		rngqiprngim.q	$$⊢Q=R{/}_{𝑠}\underset{\dot{}}{\sim }$$
10		rngqiprngim.c	$$⊢C={\mathrm{Base}}_Q$$
11		rngqiprngim.p	$$⊢P=Q{\times }_{𝑠}J$$
12		rngqiprngim.f	$$⊢F=\left(x\in B⟼⟨\left[x\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}x⟩\right)$$
13	1 2 3 4 5 6 7 8 9 10 11 12	rngqiprngho	$$⊢\phi \to F\in \left(R\mathrm{RngHom}P\right)$$
14	1 2 3 4 5 6 7 8 9 10 11 12	rngqiprngimf1	$$⊢\phi \to F:B\underset{1-1}{⟶}C\times I$$
15	1 2 3 4 5 6 7 8 9 10 11 12	rngqiprngimfo	$$⊢\phi \to F:B\underset{onto}{⟶}C\times I$$
16		df-f1o	$$⊢F:B\underset{1-1\; onto}{⟶}C\times I\leftrightarrow \left(F:B\underset{1-1}{⟶}C\times I\wedge F:B\underset{onto}{⟶}C\times I\right)$$
17	14 15 16	sylanbrc	$$⊢\phi \to F:B\underset{1-1\; onto}{⟶}C\times I$$
18	1 2 3 4 5 6 7 8 9 10 11	rngqipbas	$$⊢\phi \to {\mathrm{Base}}_P=C\times I$$
19	18	f1oeq3d	$$⊢\phi \to \left(F:B\underset{1-1\; onto}{⟶}{\mathrm{Base}}_P\leftrightarrow F:B\underset{1-1\; onto}{⟶}C\times I\right)$$
20	17 19	mpbird	$$⊢\phi \to F:B\underset{1-1\; onto}{⟶}{\mathrm{Base}}_P$$
21	11	ovexi	$$⊢P\in \mathrm{V}$$
22		eqid	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_P$$
23	5 22	isrngim2	$$⊢\left(R\in \mathrm{Rng}\wedge P\in \mathrm{V}\right)\to \left(F\in \left(R\mathrm{RngIso}P\right)\leftrightarrow \left(F\in \left(R\mathrm{RngHom}P\right)\wedge F:B\underset{1-1\; onto}{⟶}{\mathrm{Base}}_P\right)\right)$$
24	1 21 23	sylancl	$$⊢\phi \to \left(F\in \left(R\mathrm{RngIso}P\right)\leftrightarrow \left(F\in \left(R\mathrm{RngHom}P\right)\wedge F:B\underset{1-1\; onto}{⟶}{\mathrm{Base}}_P\right)\right)$$
25	13 20 24	mpbir2and	$$⊢\phi \to F\in \left(R\mathrm{RngIso}P\right)$$