Theorem rngqiprngimf1

Description: F is a one-to-one function from (the base set of) a non-unital ring to the product of the (base set of the) quotient with a two-sided ideal and the (base set of the) two-sided ideal. (Contributed by AV, 7-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$$
	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	rngqiprngimf1	$$⊢\phi \to F:B\underset{1-1}{⟶}C\times I$$

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		ringrng	$$⊢J\in \mathrm{Ring}\to J\in \mathrm{Rng}$$
14	4 13	syl	$$⊢\phi \to J\in \mathrm{Rng}$$
15	3 14	eqeltrrid	$$⊢\phi \to R{\upharpoonright }_{𝑠}I\in \mathrm{Rng}$$
16	1 2 15	rng2idlnsg	$$⊢\phi \to I\in \mathrm{NrmSGrp}\left(R\right)$$
17		nsgsubg	$$⊢I\in \mathrm{NrmSGrp}\left(R\right)\to I\in \mathrm{SubGrp}\left(R\right)$$
18	16 17	syl	$$⊢\phi \to I\in \mathrm{SubGrp}\left(R\right)$$
19	8	oveq2i	$$⊢R{/}_{𝑠}\underset{\dot{}}{\sim }=R{/}_{𝑠}\left(R{~}_{\mathit{QG}}I\right)$$
20	9 19	eqtri	$$⊢Q=R{/}_{𝑠}\left(R{~}_{\mathit{QG}}I\right)$$
21		eqid	$$⊢\mathrm{2Ideal}\left(R\right)=\mathrm{2Ideal}\left(R\right)$$
22	20 21	qus2idrng	$$⊢\left(R\in \mathrm{Rng}\wedge I\in \mathrm{2Ideal}\left(R\right)\wedge I\in \mathrm{SubGrp}\left(R\right)\right)\to Q\in \mathrm{Rng}$$
23	1 2 18 22	syl3anc	$$⊢\phi \to Q\in \mathrm{Rng}$$
24		rnggrp	$$⊢Q\in \mathrm{Rng}\to Q\in \mathrm{Grp}$$
25	24	grpmndd	$$⊢Q\in \mathrm{Rng}\to Q\in \mathrm{Mnd}$$
26	23 25	syl	$$⊢\phi \to Q\in \mathrm{Mnd}$$
27		ringmnd	$$⊢J\in \mathrm{Ring}\to J\in \mathrm{Mnd}$$
28	4 27	syl	$$⊢\phi \to J\in \mathrm{Mnd}$$
29	11	xpsmnd0	$$⊢\left(Q\in \mathrm{Mnd}\wedge J\in \mathrm{Mnd}\right)\to 0_P=⟨0_Q,0_J⟩$$
30	26 28 29	syl2anc	$$⊢\phi \to 0_P=⟨0_Q,0_J⟩$$
31	30	sneqd	$$⊢\phi \to \left\{0_P\right\}=\left\{⟨0_Q,0_J⟩\right\}$$
32	31	imaeq2d	$$⊢\phi \to F^{-1}\left[\left\{0_P\right\}\right]=F^{-1}\left[\left\{⟨0_Q,0_J⟩\right\}\right]$$
33		nfv	$$⊢Ⅎx\phi$$
34		opex	$$⊢⟨\left[x\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}x⟩\in \mathrm{V}$$
35	34	a1i	$$⊢\left(\phi \wedge x\in B\right)\to ⟨\left[x\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}x⟩\in \mathrm{V}$$
36	33 35 12	fnmptd	$$⊢\phi \to FFnB$$
37		fncnvima2	$$⊢FFnB\to F^{-1}\left[\left\{⟨0_Q,0_J⟩\right\}\right]=\left\{a\in B|F\left(a\right)\in \left\{⟨0_Q,0_J⟩\right\}\right\}$$
38	36 37	syl	$$⊢\phi \to F^{-1}\left[\left\{⟨0_Q,0_J⟩\right\}\right]=\left\{a\in B|F\left(a\right)\in \left\{⟨0_Q,0_J⟩\right\}\right\}$$
39	1 2 3 4 5 6 7 8 9 10 11 12	rngqiprngimfv	$$⊢\left(\phi \wedge a\in B\right)\to F\left(a\right)=⟨\left[a\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}a⟩$$
40	39	eleq1d	$$⊢\left(\phi \wedge a\in B\right)\to \left(F\left(a\right)\in \left\{⟨0_Q,0_J⟩\right\}\leftrightarrow ⟨\left[a\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}a⟩\in \left\{⟨0_Q,0_J⟩\right\}\right)$$
41	40	rabbidva	$$⊢\phi \to \left\{a\in B|F\left(a\right)\in \left\{⟨0_Q,0_J⟩\right\}\right\}=\left\{a\in B|⟨\left[a\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}a⟩\in \left\{⟨0_Q,0_J⟩\right\}\right\}$$
42		eceq1	$$⊢a=0_R\to \left[a\right]\underset{\dot{}}{\sim }=\left[0_R\right]\underset{\dot{}}{\sim }$$
43		oveq2	$$⊢a=0_R\to \underset{\dot{}}{1}\underset{\dot{}}{·}a=\underset{\dot{}}{1}\underset{\dot{}}{·}{0}_R$$
44	42 43	opeq12d	$$⊢a=0_R\to ⟨\left[a\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}a⟩=⟨\left[0_R\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}{0}_R⟩$$
45	44	eleq1d	$$⊢a=0_R\to \left(⟨\left[a\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}a⟩\in \left\{⟨0_Q,0_J⟩\right\}\leftrightarrow ⟨\left[0_R\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}{0}_R⟩\in \left\{⟨0_Q,0_J⟩\right\}\right)$$
46		rnggrp	$$⊢R\in \mathrm{Rng}\to R\in \mathrm{Grp}$$
47	1 46	syl	$$⊢\phi \to R\in \mathrm{Grp}$$
48	47	grpmndd	$$⊢\phi \to R\in \mathrm{Mnd}$$
49		eqid	$$⊢0_R=0_R$$
50	5 49	mndidcl	$$⊢R\in \mathrm{Mnd}\to 0_R\in B$$
51	48 50	syl	$$⊢\phi \to 0_R\in B$$
52	8	eceq2i	$$⊢\left[0_R\right]\underset{\dot{}}{\sim }=\left[0_R\right]\left(R{~}_{\mathit{QG}}I\right)$$
53	20 49	qus0	$$⊢I\in \mathrm{NrmSGrp}\left(R\right)\to \left[0_R\right]\left(R{~}_{\mathit{QG}}I\right)=0_Q$$
54	16 53	syl	$$⊢\phi \to \left[0_R\right]\left(R{~}_{\mathit{QG}}I\right)=0_Q$$
55	52 54	eqtrid	$$⊢\phi \to \left[0_R\right]\underset{\dot{}}{\sim }=0_Q$$
56	1 2 15	rng2idl0	$$⊢\phi \to 0_R\in I$$
57	5 21	2idlss	$$⊢I\in \mathrm{2Ideal}\left(R\right)\to I\subseteq B$$
58	2 57	syl	$$⊢\phi \to I\subseteq B$$
59	3 5 49	ress0g	$$⊢\left(R\in \mathrm{Mnd}\wedge 0_R\in I\wedge I\subseteq B\right)\to 0_R=0_J$$
60	48 56 58 59	syl3anc	$$⊢\phi \to 0_R=0_J$$
61	60	oveq2d	$$⊢\phi \to \underset{\dot{}}{1}\underset{\dot{}}{·}{0}_R=\underset{\dot{}}{1}\underset{\dot{}}{·}{0}_J$$
62	3 6	ressmulr	$$⊢I\in \mathrm{2Ideal}\left(R\right)\to \underset{\dot{}}{·}={\cdot }_J$$
63	2 62	syl	$$⊢\phi \to \underset{\dot{}}{·}={\cdot }_J$$
64	63	oveqd	$$⊢\phi \to \underset{\dot{}}{1}\underset{\dot{}}{·}{0}_J=\underset{\dot{}}{1}{\cdot }_J{0}_J$$
65		eqid	$$⊢{\mathrm{Base}}_J={\mathrm{Base}}_J$$
66	65 7	ringidcl	$$⊢J\in \mathrm{Ring}\to \underset{\dot{}}{1}\in {\mathrm{Base}}_J$$
67		eqid	$$⊢{\cdot }_J={\cdot }_J$$
68		eqid	$$⊢0_J=0_J$$
69	65 67 68	ringrz	$$⊢\left(J\in \mathrm{Ring}\wedge \underset{\dot{}}{1}\in {\mathrm{Base}}_J\right)\to \underset{\dot{}}{1}{\cdot }_J{0}_J=0_J$$
70	4 66 69	syl2anc2	$$⊢\phi \to \underset{\dot{}}{1}{\cdot }_J{0}_J=0_J$$
71	61 64 70	3eqtrd	$$⊢\phi \to \underset{\dot{}}{1}\underset{\dot{}}{·}{0}_R=0_J$$
72	55 71	opeq12d	$$⊢\phi \to ⟨\left[0_R\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}{0}_R⟩=⟨0_Q,0_J⟩$$
73		opex	$$⊢⟨\left[0_R\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}{0}_R⟩\in \mathrm{V}$$
74	73	elsn	$$⊢⟨\left[0_R\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}{0}_R⟩\in \left\{⟨0_Q,0_J⟩\right\}\leftrightarrow ⟨\left[0_R\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}{0}_R⟩=⟨0_Q,0_J⟩$$
75	72 74	sylibr	$$⊢\phi \to ⟨\left[0_R\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}{0}_R⟩\in \left\{⟨0_Q,0_J⟩\right\}$$
76		opex	$$⊢⟨\left[a\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}a⟩\in \mathrm{V}$$
77	76	elsn	$$⊢⟨\left[a\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}a⟩\in \left\{⟨0_Q,0_J⟩\right\}\leftrightarrow ⟨\left[a\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}a⟩=⟨0_Q,0_J⟩$$
78	8	ovexi	$$⊢\underset{\dot{}}{\sim }\in \mathrm{V}$$
79		ecexg	$$⊢\underset{\dot{}}{\sim }\in \mathrm{V}\to \left[a\right]\underset{\dot{}}{\sim }\in \mathrm{V}$$
80	78 79	ax-mp	$$⊢\left[a\right]\underset{\dot{}}{\sim }\in \mathrm{V}$$
81		ovex	$$⊢\underset{\dot{}}{1}\underset{\dot{}}{·}a\in \mathrm{V}$$
82	80 81	opth	$$⊢⟨\left[a\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}a⟩=⟨0_Q,0_J⟩\leftrightarrow \left(\left[a\right]\underset{\dot{}}{\sim }=0_Q\wedge \underset{\dot{}}{1}\underset{\dot{}}{·}a=0_J\right)$$
83	77 82	bitri	$$⊢⟨\left[a\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}a⟩\in \left\{⟨0_Q,0_J⟩\right\}\leftrightarrow \left(\left[a\right]\underset{\dot{}}{\sim }=0_Q\wedge \underset{\dot{}}{1}\underset{\dot{}}{·}a=0_J\right)$$
84	1 2 3 4 5 6 7 8 9	rngqiprngimf1lem	$$⊢\left(\phi \wedge a\in B\right)\to \left(\left(\left[a\right]\underset{\dot{}}{\sim }=0_Q\wedge \underset{\dot{}}{1}\underset{\dot{}}{·}a=0_J\right)\to a=0_R\right)$$
85	83 84	biimtrid	$$⊢\left(\phi \wedge a\in B\right)\to \left(⟨\left[a\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}a⟩\in \left\{⟨0_Q,0_J⟩\right\}\to a=0_R\right)$$
86	85	imp	$$⊢\left(\left(\phi \wedge a\in B\right)\wedge ⟨\left[a\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}a⟩\in \left\{⟨0_Q,0_J⟩\right\}\right)\to a=0_R$$
87	45 51 75 86	rabeqsnd	$$⊢\phi \to \left\{a\in B|⟨\left[a\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}a⟩\in \left\{⟨0_Q,0_J⟩\right\}\right\}=\left\{0_R\right\}$$
88	41 87	eqtrd	$$⊢\phi \to \left\{a\in B|F\left(a\right)\in \left\{⟨0_Q,0_J⟩\right\}\right\}=\left\{0_R\right\}$$
89	32 38 88	3eqtrd	$$⊢\phi \to F^{-1}\left[\left\{0_P\right\}\right]=\left\{0_R\right\}$$
90	1 2 3 4 5 6 7 8 9 10 11 12	rngqiprngghm	$$⊢\phi \to F\in \left(R\mathrm{GrpHom}P\right)$$
91		eqid	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_P$$
92		eqid	$$⊢0_P=0_P$$
93	5 91 49 92	kerf1ghm	$$⊢F\in \left(R\mathrm{GrpHom}P\right)\to \left(F:B\underset{1-1}{⟶}{\mathrm{Base}}_P\leftrightarrow F^{-1}\left[\left\{0_P\right\}\right]=\left\{0_R\right\}\right)$$
94	90 93	syl	$$⊢\phi \to \left(F:B\underset{1-1}{⟶}{\mathrm{Base}}_P\leftrightarrow F^{-1}\left[\left\{0_P\right\}\right]=\left\{0_R\right\}\right)$$
95	89 94	mpbird	$$⊢\phi \to F:B\underset{1-1}{⟶}{\mathrm{Base}}_P$$
96		eqidd	$$⊢\phi \to F=F$$
97		eqidd	$$⊢\phi \to B=B$$
98	1 2 3 4 5 6 7 8 9 10 11	rngqipbas	$$⊢\phi \to {\mathrm{Base}}_P=C\times I$$
99	96 97 98	f1eq123d	$$⊢\phi \to \left(F:B\underset{1-1}{⟶}{\mathrm{Base}}_P\leftrightarrow F:B\underset{1-1}{⟶}C\times I\right)$$
100	95 99	mpbid	$$⊢\phi \to F:B\underset{1-1}{⟶}C\times I$$