Theorem rngqiprngghm

Description: F is a homomorphism of the additive groups of non-unital rings. (Contributed by AV, 24-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	rngqiprngghm	$$⊢\phi \to F\in \left(R\mathrm{GrpHom}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		eqid	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_P$$
14		eqid	$$⊢{+}_R={+}_R$$
15		eqid	$$⊢{+}_P={+}_P$$
16		rnggrp	$$⊢R\in \mathrm{Rng}\to R\in \mathrm{Grp}$$
17	1 16	syl	$$⊢\phi \to R\in \mathrm{Grp}$$
18	1 2 3 4 5 6 7 8 9 10 11	rngqiprng	$$⊢\phi \to P\in \mathrm{Rng}$$
19		rnggrp	$$⊢P\in \mathrm{Rng}\to P\in \mathrm{Grp}$$
20	18 19	syl	$$⊢\phi \to P\in \mathrm{Grp}$$
21	1 2 3 4 5 6 7 8 9 10 11 12	rngqiprngimf	$$⊢\phi \to F:B⟶C\times I$$
22	1 2 3 4 5 6 7 8 9 10 11	rngqipbas	$$⊢\phi \to {\mathrm{Base}}_P=C\times I$$
23	22	feq3d	$$⊢\phi \to \left(F:B⟶{\mathrm{Base}}_P\leftrightarrow F:B⟶C\times I\right)$$
24	21 23	mpbird	$$⊢\phi \to F:B⟶{\mathrm{Base}}_P$$
25		ringrng	$$⊢J\in \mathrm{Ring}\to J\in \mathrm{Rng}$$
26	4 25	syl	$$⊢\phi \to J\in \mathrm{Rng}$$
27	3 26	eqeltrrid	$$⊢\phi \to R{\upharpoonright }_{𝑠}I\in \mathrm{Rng}$$
28	1 2 27	rng2idlnsg	$$⊢\phi \to I\in \mathrm{NrmSGrp}\left(R\right)$$
29	28 5 8 9	ecqusaddd	$$⊢\left(\phi \wedge \left(a\in B\wedge b\in B\right)\right)\to \left[\left(a{+}_{R}b\right)\right]\underset{\dot{}}{\sim }=\left[a\right]\underset{\dot{}}{\sim }{+}_Q\left[b\right]\underset{\dot{}}{\sim }$$
30	1 2 3 4 5 6 7	rngqiprngghmlem3	$$⊢\left(\phi \wedge \left(a\in B\wedge b\in B\right)\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}\left(a{+}_{R}b\right)=\left(\underset{\dot{}}{1}\underset{\dot{}}{·}a\right){+}_J\left(\underset{\dot{}}{1}\underset{\dot{}}{·}b\right)$$
31	29 30	opeq12d	$$⊢\left(\phi \wedge \left(a\in B\wedge b\in B\right)\right)\to ⟨\left[\left(a{+}_{R}b\right)\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}\left(a{+}_{R}b\right)⟩=⟨\left[a\right]\underset{\dot{}}{\sim }{+}_Q\left[b\right]\underset{\dot{}}{\sim },\left(\underset{\dot{}}{1}\underset{\dot{}}{·}a\right){+}_J\left(\underset{\dot{}}{1}\underset{\dot{}}{·}b\right)⟩$$
32		eqid	$$⊢{\mathrm{Base}}_Q={\mathrm{Base}}_Q$$
33		eqid	$$⊢{\mathrm{Base}}_J={\mathrm{Base}}_J$$
34	9	ovexi	$$⊢Q\in \mathrm{V}$$
35	34	a1i	$$⊢\left(\phi \wedge \left(a\in B\wedge b\in B\right)\right)\to Q\in \mathrm{V}$$
36	4	adantr	$$⊢\left(\phi \wedge \left(a\in B\wedge b\in B\right)\right)\to J\in \mathrm{Ring}$$
37		simpl	$$⊢\left(a\in B\wedge b\in B\right)\to a\in B$$
38	8 9 5 32	quseccl0	$$⊢\left(R\in \mathrm{Rng}\wedge a\in B\right)\to \left[a\right]\underset{\dot{}}{\sim }\in {\mathrm{Base}}_Q$$
39	1 37 38	syl2an	$$⊢\left(\phi \wedge \left(a\in B\wedge b\in B\right)\right)\to \left[a\right]\underset{\dot{}}{\sim }\in {\mathrm{Base}}_Q$$
40	1 2 3 4 5 6 7	rngqiprngghmlem1	$$⊢\left(\phi \wedge a\in B\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}a\in {\mathrm{Base}}_J$$
41	40	adantrr	$$⊢\left(\phi \wedge \left(a\in B\wedge b\in B\right)\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}a\in {\mathrm{Base}}_J$$
42		simpr	$$⊢\left(a\in B\wedge b\in B\right)\to b\in B$$
43	8 9 5 32	quseccl0	$$⊢\left(R\in \mathrm{Rng}\wedge b\in B\right)\to \left[b\right]\underset{\dot{}}{\sim }\in {\mathrm{Base}}_Q$$
44	1 42 43	syl2an	$$⊢\left(\phi \wedge \left(a\in B\wedge b\in B\right)\right)\to \left[b\right]\underset{\dot{}}{\sim }\in {\mathrm{Base}}_Q$$
45	1 2 3 4 5 6 7	rngqiprngghmlem1	$$⊢\left(\phi \wedge b\in B\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}b\in {\mathrm{Base}}_J$$
46	45	adantrl	$$⊢\left(\phi \wedge \left(a\in B\wedge b\in B\right)\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}b\in {\mathrm{Base}}_J$$
47	28 5 8 9	ecqusaddcl	$$⊢\left(\phi \wedge \left(a\in B\wedge b\in B\right)\right)\to \left[a\right]\underset{\dot{}}{\sim }{+}_Q\left[b\right]\underset{\dot{}}{\sim }\in {\mathrm{Base}}_Q$$
48	1 2 3 4 5 6 7	rngqiprngghmlem2	$$⊢\left(\phi \wedge \left(a\in B\wedge b\in B\right)\right)\to \left(\underset{\dot{}}{1}\underset{\dot{}}{·}a\right){+}_J\left(\underset{\dot{}}{1}\underset{\dot{}}{·}b\right)\in {\mathrm{Base}}_J$$
49		eqid	$$⊢{+}_Q={+}_Q$$
50		eqid	$$⊢{+}_J={+}_J$$
51	11 32 33 35 36 39 41 44 46 47 48 49 50 15	xpsadd	$$⊢\left(\phi \wedge \left(a\in B\wedge b\in B\right)\right)\to ⟨\left[a\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}a⟩{+}_P⟨\left[b\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}b⟩=⟨\left[a\right]\underset{\dot{}}{\sim }{+}_Q\left[b\right]\underset{\dot{}}{\sim },\left(\underset{\dot{}}{1}\underset{\dot{}}{·}a\right){+}_J\left(\underset{\dot{}}{1}\underset{\dot{}}{·}b\right)⟩$$
52	31 51	eqtr4d	$$⊢\left(\phi \wedge \left(a\in B\wedge b\in B\right)\right)\to ⟨\left[\left(a{+}_{R}b\right)\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}\left(a{+}_{R}b\right)⟩=⟨\left[a\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}a⟩{+}_P⟨\left[b\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}b⟩$$
53	1	adantr	$$⊢\left(\phi \wedge \left(a\in B\wedge b\in B\right)\right)\to R\in \mathrm{Rng}$$
54	37	adantl	$$⊢\left(\phi \wedge \left(a\in B\wedge b\in B\right)\right)\to a\in B$$
55	42	adantl	$$⊢\left(\phi \wedge \left(a\in B\wedge b\in B\right)\right)\to b\in B$$
56	5 14	rngacl	$$⊢\left(R\in \mathrm{Rng}\wedge a\in B\wedge b\in B\right)\to a{+}_{R}b\in B$$
57	53 54 55 56	syl3anc	$$⊢\left(\phi \wedge \left(a\in B\wedge b\in B\right)\right)\to a{+}_{R}b\in B$$
58	1 2 3 4 5 6 7 8 9 10 11 12	rngqiprngimfv	$$⊢\left(\phi \wedge a{+}_{R}b\in B\right)\to F\left(a{+}_{R}b\right)=⟨\left[\left(a{+}_{R}b\right)\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}\left(a{+}_{R}b\right)⟩$$
59	57 58	syldan	$$⊢\left(\phi \wedge \left(a\in B\wedge b\in B\right)\right)\to F\left(a{+}_{R}b\right)=⟨\left[\left(a{+}_{R}b\right)\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}\left(a{+}_{R}b\right)⟩$$
60	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⟩$$
61	60	adantrr	$$⊢\left(\phi \wedge \left(a\in B\wedge b\in B\right)\right)\to F\left(a\right)=⟨\left[a\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}a⟩$$
62	1 2 3 4 5 6 7 8 9 10 11 12	rngqiprngimfv	$$⊢\left(\phi \wedge b\in B\right)\to F\left(b\right)=⟨\left[b\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}b⟩$$
63	62	adantrl	$$⊢\left(\phi \wedge \left(a\in B\wedge b\in B\right)\right)\to F\left(b\right)=⟨\left[b\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}b⟩$$
64	61 63	oveq12d	$$⊢\left(\phi \wedge \left(a\in B\wedge b\in B\right)\right)\to F\left(a\right){+}_{P}F\left(b\right)=⟨\left[a\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}a⟩{+}_P⟨\left[b\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}b⟩$$
65	52 59 64	3eqtr4d	$$⊢\left(\phi \wedge \left(a\in B\wedge b\in B\right)\right)\to F\left(a{+}_{R}b\right)=F\left(a\right){+}_{P}F\left(b\right)$$
66	5 13 14 15 17 20 24 65	isghmd	$$⊢\phi \to F\in \left(R\mathrm{GrpHom}P\right)$$