Theorem rngqiprngho

Description: F is a homomorphism 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	rngqiprngho	$$⊢\phi \to F\in \left(R\mathrm{RngHom}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	rngqiprng	$$⊢\phi \to P\in \mathrm{Rng}$$
14	1 2 3 4 5 6 7 8 9 10 11 12	rngqiprngghm	$$⊢\phi \to F\in \left(R\mathrm{GrpHom}P\right)$$
15	1 2 3 4 5 6 7 8 9 10 11 12	rngqiprnglin	$$⊢\phi \to \forall a\in B\forall b\in BF\left(a\underset{\dot{}}{·}b\right)=F\left(a\right){\cdot }_{P}F\left(b\right)$$
16	14 15	jca	$$⊢\phi \to \left(F\in \left(R\mathrm{GrpHom}P\right)\wedge \forall a\in B\forall b\in BF\left(a\underset{\dot{}}{·}b\right)=F\left(a\right){\cdot }_{P}F\left(b\right)\right)$$
17		eqid	$$⊢{\cdot }_P={\cdot }_P$$
18	5 6 17	isrnghm	$$⊢F\in \left(R\mathrm{RngHom}P\right)\leftrightarrow \left(\left(R\in \mathrm{Rng}\wedge P\in \mathrm{Rng}\right)\wedge \left(F\in \left(R\mathrm{GrpHom}P\right)\wedge \forall a\in B\forall b\in BF\left(a\underset{\dot{}}{·}b\right)=F\left(a\right){\cdot }_{P}F\left(b\right)\right)\right)$$
19	1 13 16 18	syl21anbrc	$$⊢\phi \to F\in \left(R\mathrm{RngHom}P\right)$$