Theorem rngqiprngimf

Description: F is a function from (the base set of) a non-unital ring to the product of the (base set C of the) quotient with a two-sided ideal and the (base set I of the) two-sided ideal (because of 2idlbas , ( BaseJ ) = I !) (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	rngqiprngimf	$$⊢\phi \to F:B⟶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	8	ovexi	$$⊢\underset{\dot{}}{\sim }\in \mathrm{V}$$
14	13	ecelqsi	$$⊢x\in B\to \left[x\right]\underset{\dot{}}{\sim }\in \left(B/\underset{\dot{}}{\sim }\right)$$
15	14	adantl	$$⊢\left(\phi \wedge x\in B\right)\to \left[x\right]\underset{\dot{}}{\sim }\in \left(B/\underset{\dot{}}{\sim }\right)$$
16	9	a1i	$$⊢\left(\phi \wedge x\in B\right)\to Q=R{/}_{𝑠}\underset{\dot{}}{\sim }$$
17	5	a1i	$$⊢\left(\phi \wedge x\in B\right)\to B={\mathrm{Base}}_R$$
18	13	a1i	$$⊢\left(\phi \wedge x\in B\right)\to \underset{\dot{}}{\sim }\in \mathrm{V}$$
19	1	adantr	$$⊢\left(\phi \wedge x\in B\right)\to R\in \mathrm{Rng}$$
20	16 17 18 19	qusbas	$$⊢\left(\phi \wedge x\in B\right)\to B/\underset{\dot{}}{\sim }={\mathrm{Base}}_Q$$
21	20 10	eqtr4di	$$⊢\left(\phi \wedge x\in B\right)\to B/\underset{\dot{}}{\sim }=C$$
22	15 21	eleqtrd	$$⊢\left(\phi \wedge x\in B\right)\to \left[x\right]\underset{\dot{}}{\sim }\in C$$
23		eqid	$$⊢{\mathrm{Base}}_J={\mathrm{Base}}_J$$
24	2 3 23	2idlbas	$$⊢\phi \to {\mathrm{Base}}_J=I$$
25	2 3 23	2idlelbas	$$⊢\phi \to \left({\mathrm{Base}}_J\in \mathrm{LIdeal}\left(R\right)\wedge {\mathrm{Base}}_J\in \mathrm{LIdeal}\left({opp}_r\left(R\right)\right)\right)$$
26	25	simprd	$$⊢\phi \to {\mathrm{Base}}_J\in \mathrm{LIdeal}\left({opp}_r\left(R\right)\right)$$
27	24 26	eqeltrrd	$$⊢\phi \to I\in \mathrm{LIdeal}\left({opp}_r\left(R\right)\right)$$
28		ringrng	$$⊢J\in \mathrm{Ring}\to J\in \mathrm{Rng}$$
29	4 28	syl	$$⊢\phi \to J\in \mathrm{Rng}$$
30	3 29	eqeltrrid	$$⊢\phi \to R{\upharpoonright }_{𝑠}I\in \mathrm{Rng}$$
31	1 2 30	rng2idl0	$$⊢\phi \to 0_R\in I$$
32	1 27 31	3jca	$$⊢\phi \to \left(R\in \mathrm{Rng}\wedge I\in \mathrm{LIdeal}\left({opp}_r\left(R\right)\right)\wedge 0_R\in I\right)$$
33	23 7	ringidcl	$$⊢J\in \mathrm{Ring}\to \underset{\dot{}}{1}\in {\mathrm{Base}}_J$$
34	4 33	syl	$$⊢\phi \to \underset{\dot{}}{1}\in {\mathrm{Base}}_J$$
35	34 24	eleqtrd	$$⊢\phi \to \underset{\dot{}}{1}\in I$$
36	35	anim1ci	$$⊢\left(\phi \wedge x\in B\right)\to \left(x\in B\wedge \underset{\dot{}}{1}\in I\right)$$
37		eqid	$$⊢0_R=0_R$$
38		eqid	$$⊢\mathrm{LIdeal}\left({opp}_r\left(R\right)\right)=\mathrm{LIdeal}\left({opp}_r\left(R\right)\right)$$
39	37 5 6 38	rngridlmcl	$$⊢\left(\left(R\in \mathrm{Rng}\wedge I\in \mathrm{LIdeal}\left({opp}_r\left(R\right)\right)\wedge 0_R\in I\right)\wedge \left(x\in B\wedge \underset{\dot{}}{1}\in I\right)\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}x\in I$$
40	32 36 39	syl2an2r	$$⊢\left(\phi \wedge x\in B\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}x\in I$$
41	22 40	opelxpd	$$⊢\left(\phi \wedge x\in B\right)\to ⟨\left[x\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}x⟩\in \left(C\times I\right)$$
42	41 12	fmptd	$$⊢\phi \to F:B⟶C\times I$$