Theorem rngqiprnglin

Description: F is linear with respect to the multiplication. (Contributed by AV, 28-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	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)$$

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}}_Q={\mathrm{Base}}_Q$$
14		eqid	$$⊢{\mathrm{Base}}_J={\mathrm{Base}}_J$$
15	9	ovexi	$$⊢Q\in \mathrm{V}$$
16	15	a1i	$$⊢\left(\phi \wedge \left(a\in B\wedge b\in B\right)\right)\to Q\in \mathrm{V}$$
17	4	adantr	$$⊢\left(\phi \wedge \left(a\in B\wedge b\in B\right)\right)\to J\in \mathrm{Ring}$$
18		simpl	$$⊢\left(a\in B\wedge b\in B\right)\to a\in B$$
19	8 9 5 13	quseccl0	$$⊢\left(R\in \mathrm{Rng}\wedge a\in B\right)\to \left[a\right]\underset{\dot{}}{\sim }\in {\mathrm{Base}}_Q$$
20	1 18 19	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$$
21	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$$
22	18 21	sylan2	$$⊢\left(\phi \wedge \left(a\in B\wedge b\in B\right)\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}a\in {\mathrm{Base}}_J$$
23		simpr	$$⊢\left(a\in B\wedge b\in B\right)\to b\in B$$
24	8 9 5 13	quseccl0	$$⊢\left(R\in \mathrm{Rng}\wedge b\in B\right)\to \left[b\right]\underset{\dot{}}{\sim }\in {\mathrm{Base}}_Q$$
25	1 23 24	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$$
26	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$$
27	23 26	sylan2	$$⊢\left(\phi \wedge \left(a\in B\wedge b\in B\right)\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}b\in {\mathrm{Base}}_J$$
28	1 2 3 4 5 6 7 8 9	rngqiprnglinlem3	$$⊢\left(\phi \wedge \left(a\in B\wedge b\in B\right)\right)\to \left[a\right]\underset{\dot{}}{\sim }{\cdot }_Q\left[b\right]\underset{\dot{}}{\sim }\in {\mathrm{Base}}_Q$$
29		eqid	$$⊢{\cdot }_J={\cdot }_J$$
30	14 29 17 22 27	ringcld	$$⊢\left(\phi \wedge \left(a\in B\wedge b\in B\right)\right)\to \left(\underset{\dot{}}{1}\underset{\dot{}}{·}a\right){\cdot }_J\left(\underset{\dot{}}{1}\underset{\dot{}}{·}b\right)\in {\mathrm{Base}}_J$$
31		eqid	$$⊢{\cdot }_Q={\cdot }_Q$$
32		eqid	$$⊢{\cdot }_P={\cdot }_P$$
33	11 13 14 16 17 20 22 25 27 28 30 31 29 32	xpsmul	$$⊢\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⟩{\cdot }_P⟨\left[b\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}b⟩=⟨\left[a\right]\underset{\dot{}}{\sim }{\cdot }_Q\left[b\right]\underset{\dot{}}{\sim },\left(\underset{\dot{}}{1}\underset{\dot{}}{·}a\right){\cdot }_J\left(\underset{\dot{}}{1}\underset{\dot{}}{·}b\right)⟩$$
34	1 2 3 4 5 6 7 8 9	rngqiprnglinlem2	$$⊢\left(\phi \wedge \left(a\in B\wedge b\in B\right)\right)\to \left[\left(a\underset{\dot{}}{·}b\right)\right]\underset{\dot{}}{\sim }=\left[a\right]\underset{\dot{}}{\sim }{\cdot }_Q\left[b\right]\underset{\dot{}}{\sim }$$
35	34	eqcomd	$$⊢\left(\phi \wedge \left(a\in B\wedge b\in B\right)\right)\to \left[a\right]\underset{\dot{}}{\sim }{\cdot }_Q\left[b\right]\underset{\dot{}}{\sim }=\left[\left(a\underset{\dot{}}{·}b\right)\right]\underset{\dot{}}{\sim }$$
36	2	adantr	$$⊢\left(\phi \wedge \left(a\in B\wedge b\in B\right)\right)\to I\in \mathrm{2Ideal}\left(R\right)$$
37	3 6	ressmulr	$$⊢I\in \mathrm{2Ideal}\left(R\right)\to \underset{\dot{}}{·}={\cdot }_J$$
38	36 37	syl	$$⊢\left(\phi \wedge \left(a\in B\wedge b\in B\right)\right)\to \underset{\dot{}}{·}={\cdot }_J$$
39	38	eqcomd	$$⊢\left(\phi \wedge \left(a\in B\wedge b\in B\right)\right)\to {\cdot }_J=\underset{\dot{}}{·}$$
40	39	oveqd	$$⊢\left(\phi \wedge \left(a\in B\wedge b\in B\right)\right)\to \left(\underset{\dot{}}{1}\underset{\dot{}}{·}a\right){\cdot }_J\left(\underset{\dot{}}{1}\underset{\dot{}}{·}b\right)=\left(\underset{\dot{}}{1}\underset{\dot{}}{·}a\right)\underset{\dot{}}{·}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}b\right)$$
41	1 2 3 4 5 6 7	rngqiprnglinlem1	$$⊢\left(\phi \wedge \left(a\in B\wedge b\in B\right)\right)\to \left(\underset{\dot{}}{1}\underset{\dot{}}{·}a\right)\underset{\dot{}}{·}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}b\right)=\underset{\dot{}}{1}\underset{\dot{}}{·}\left(a\underset{\dot{}}{·}b\right)$$
42	40 41	eqtrd	$$⊢\left(\phi \wedge \left(a\in B\wedge b\in B\right)\right)\to \left(\underset{\dot{}}{1}\underset{\dot{}}{·}a\right){\cdot }_J\left(\underset{\dot{}}{1}\underset{\dot{}}{·}b\right)=\underset{\dot{}}{1}\underset{\dot{}}{·}\left(a\underset{\dot{}}{·}b\right)$$
43	35 42	opeq12d	$$⊢\left(\phi \wedge \left(a\in B\wedge b\in B\right)\right)\to ⟨\left[a\right]\underset{\dot{}}{\sim }{\cdot }_Q\left[b\right]\underset{\dot{}}{\sim },\left(\underset{\dot{}}{1}\underset{\dot{}}{·}a\right){\cdot }_J\left(\underset{\dot{}}{1}\underset{\dot{}}{·}b\right)⟩=⟨\left[\left(a\underset{\dot{}}{·}b\right)\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}\left(a\underset{\dot{}}{·}b\right)⟩$$
44	33 43	eqtr2d	$$⊢\left(\phi \wedge \left(a\in B\wedge b\in B\right)\right)\to ⟨\left[\left(a\underset{\dot{}}{·}b\right)\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}\left(a\underset{\dot{}}{·}b\right)⟩=⟨\left[a\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}a⟩{\cdot }_P⟨\left[b\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}b⟩$$
45	1	anim1i	$$⊢\left(\phi \wedge \left(a\in B\wedge b\in B\right)\right)\to \left(R\in \mathrm{Rng}\wedge \left(a\in B\wedge b\in B\right)\right)$$
46		3anass	$$⊢\left(R\in \mathrm{Rng}\wedge a\in B\wedge b\in B\right)\leftrightarrow \left(R\in \mathrm{Rng}\wedge \left(a\in B\wedge b\in B\right)\right)$$
47	45 46	sylibr	$$⊢\left(\phi \wedge \left(a\in B\wedge b\in B\right)\right)\to \left(R\in \mathrm{Rng}\wedge a\in B\wedge b\in B\right)$$
48	5 6	rngcl	$$⊢\left(R\in \mathrm{Rng}\wedge a\in B\wedge b\in B\right)\to a\underset{\dot{}}{·}b\in B$$
49	47 48	syl	$$⊢\left(\phi \wedge \left(a\in B\wedge b\in B\right)\right)\to a\underset{\dot{}}{·}b\in B$$
50	1 2 3 4 5 6 7 8 9 10 11 12	rngqiprngimfv	$$⊢\left(\phi \wedge a\underset{\dot{}}{·}b\in B\right)\to F\left(a\underset{\dot{}}{·}b\right)=⟨\left[\left(a\underset{\dot{}}{·}b\right)\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}\left(a\underset{\dot{}}{·}b\right)⟩$$
51	49 50	syldan	$$⊢\left(\phi \wedge \left(a\in B\wedge b\in B\right)\right)\to F\left(a\underset{\dot{}}{·}b\right)=⟨\left[\left(a\underset{\dot{}}{·}b\right)\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}\left(a\underset{\dot{}}{·}b\right)⟩$$
52	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⟩$$
53	18 52	sylan2	$$⊢\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⟩$$
54	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⟩$$
55	23 54	sylan2	$$⊢\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⟩$$
56	53 55	oveq12d	$$⊢\left(\phi \wedge \left(a\in B\wedge b\in B\right)\right)\to F\left(a\right){\cdot }_{P}F\left(b\right)=⟨\left[a\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}a⟩{\cdot }_P⟨\left[b\right]\underset{\dot{}}{\sim },\underset{\dot{}}{1}\underset{\dot{}}{·}b⟩$$
57	44 51 56	3eqtr4d	$$⊢\left(\phi \wedge \left(a\in B\wedge b\in B\right)\right)\to F\left(a\underset{\dot{}}{·}b\right)=F\left(a\right){\cdot }_{P}F\left(b\right)$$
58	57	ralrimivva	$$⊢\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)$$