Theorem deg1gprod

Description: Degree multiplication is a homomorphism. (Contributed by metakunt, 6-May-2025)

	Ref	Expression
Hypotheses	deg1gprod.1	$$⊢\phi \to R\in \mathrm{IDomn}$$
	deg1gprod.2	$$⊢\phi \to N\in \mathrm{Fin}$$
	deg1gprod.3	$$⊢\phi \to \forall x\in N\left(C\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}\wedge C\ne 0_{{\mathrm{Poly}}_1\left(R\right)}\right)$$
Assertion	deg1gprod	$$⊢\phi \to \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in N}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in N}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in N}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		deg1gprod.1	$$⊢\phi \to R\in \mathrm{IDomn}$$
2		deg1gprod.2	$$⊢\phi \to N\in \mathrm{Fin}$$
3		deg1gprod.3	$$⊢\phi \to \forall x\in N\left(C\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}\wedge C\ne 0_{{\mathrm{Poly}}_1\left(R\right)}\right)$$
4		mpteq1	$$⊢a=\varnothing \to \left(x\in a⟼C\right)=\left(x\in \varnothing ⟼C\right)$$
5	4	oveq2d	$$⊢a=\varnothing \to \underset{x\in a}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C=\underset{x\in \varnothing }{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C$$
6	5	fveq2d	$$⊢a=\varnothing \to {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in a}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)={\mathrm{deg}}_1\left(R\right)\left(\underset{x\in \varnothing }{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)$$
7		sumeq1	$$⊢a=\varnothing \to \sum _{n\in a}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)=\sum _{n\in \varnothing }{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)$$
8	6 7	eqeq12d	$$⊢a=\varnothing \to \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in a}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in a}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\leftrightarrow {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in \varnothing }{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in \varnothing }{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\right)$$
9	6	breq2d	$$⊢a=\varnothing \to \left(0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in a}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\leftrightarrow 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in \varnothing }{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)$$
10	8 9	anbi12d	$$⊢a=\varnothing \to \left(\left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in a}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in a}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in a}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\leftrightarrow \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in \varnothing }{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in \varnothing }{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in \varnothing }{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\right)$$
11		mpteq1	$$⊢a=b\to \left(x\in a⟼C\right)=\left(x\in b⟼C\right)$$
12	11	oveq2d	$$⊢a=b\to \underset{x\in a}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C=\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C$$
13	12	fveq2d	$$⊢a=b\to {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in a}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)={\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)$$
14		sumeq1	$$⊢a=b\to \sum _{n\in a}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)$$
15	13 14	eqeq12d	$$⊢a=b\to \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in a}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in a}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\leftrightarrow {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\right)$$
16	13	breq2d	$$⊢a=b\to \left(0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in a}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\leftrightarrow 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)$$
17	15 16	anbi12d	$$⊢a=b\to \left(\left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in a}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in a}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in a}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\leftrightarrow \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\right)$$
18		mpteq1	$$⊢a=b\cup \left\{c\right\}\to \left(x\in a⟼C\right)=\left(x\in \left(b\cup \left\{c\right\}\right)⟼C\right)$$
19	18	oveq2d	$$⊢a=b\cup \left\{c\right\}\to \underset{x\in a}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C=\underset{x\in b\cup \left\{c\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C$$
20	19	fveq2d	$$⊢a=b\cup \left\{c\right\}\to {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in a}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)={\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b\cup \left\{c\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)$$
21		sumeq1	$$⊢a=b\cup \left\{c\right\}\to \sum _{n\in a}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)=\sum _{n\in b\cup \left\{c\right\}}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)$$
22	20 21	eqeq12d	$$⊢a=b\cup \left\{c\right\}\to \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in a}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in a}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\leftrightarrow {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b\cup \left\{c\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b\cup \left\{c\right\}}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\right)$$
23	20	breq2d	$$⊢a=b\cup \left\{c\right\}\to \left(0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in a}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\leftrightarrow 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b\cup \left\{c\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)$$
24	22 23	anbi12d	$$⊢a=b\cup \left\{c\right\}\to \left(\left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in a}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in a}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in a}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\leftrightarrow \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b\cup \left\{c\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b\cup \left\{c\right\}}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b\cup \left\{c\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\right)$$
25		mpteq1	$$⊢a=N\to \left(x\in a⟼C\right)=\left(x\in N⟼C\right)$$
26	25	oveq2d	$$⊢a=N\to \underset{x\in a}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C=\underset{x\in N}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C$$
27	26	fveq2d	$$⊢a=N\to {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in a}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)={\mathrm{deg}}_1\left(R\right)\left(\underset{x\in N}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)$$
28		sumeq1	$$⊢a=N\to \sum _{n\in a}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)=\sum _{n\in N}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)$$
29	27 28	eqeq12d	$$⊢a=N\to \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in a}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in a}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\leftrightarrow {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in N}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in N}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\right)$$
30	27	breq2d	$$⊢a=N\to \left(0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in a}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\leftrightarrow 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in N}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)$$
31	29 30	anbi12d	$$⊢a=N\to \left(\left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in a}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in a}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in a}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\leftrightarrow \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in N}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in N}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in N}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\right)$$
32		mpt0	$$⊢\left(x\in \varnothing ⟼C\right)=\varnothing$$
33	32	a1i	$$⊢\phi \to \left(x\in \varnothing ⟼C\right)=\varnothing$$
34	33	oveq2d	$$⊢\phi \to \underset{x\in \varnothing }{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C={\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}\varnothing$$
35		eqid	$$⊢0_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}=0_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}$$
36	35	gsum0	$$⊢{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}\varnothing =0_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}$$
37	36	a1i	$$⊢\phi \to {\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}\varnothing =0_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}$$
38	34 37	eqtrd	$$⊢\phi \to \underset{x\in \varnothing }{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C=0_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}$$
39	38	fveq2d	$$⊢\phi \to {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in \varnothing }{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)={\mathrm{deg}}_1\left(R\right)\left(0_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}\right)$$
40	1	idomringd	$$⊢\phi \to R\in \mathrm{Ring}$$
41		eqid	$$⊢{\mathrm{Poly}}_1\left(R\right)={\mathrm{Poly}}_1\left(R\right)$$
42		eqid	$$⊢\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)=\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)$$
43		eqid	$$⊢1_R=1_R$$
44		eqid	$$⊢{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}={\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}$$
45		eqid	$$⊢1_{{\mathrm{Poly}}_1\left(R\right)}=1_{{\mathrm{Poly}}_1\left(R\right)}$$
46	44 45	ringidval	$$⊢1_{{\mathrm{Poly}}_1\left(R\right)}=0_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}$$
47	46	eqcomi	$$⊢0_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}=1_{{\mathrm{Poly}}_1\left(R\right)}$$
48	41 42 43 47	ply1scl1	$$⊢R\in \mathrm{Ring}\to \mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(1_R\right)=0_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}$$
49	40 48	syl	$$⊢\phi \to \mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(1_R\right)=0_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}$$
50	49	eqcomd	$$⊢\phi \to 0_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}=\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(1_R\right)$$
51	50	fveq2d	$$⊢\phi \to {\mathrm{deg}}_1\left(R\right)\left(0_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}\right)={\mathrm{deg}}_1\left(R\right)\left(\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(1_R\right)\right)$$
52		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
53	52 43	ringidcl	$$⊢R\in \mathrm{Ring}\to 1_R\in {\mathrm{Base}}_R$$
54	40 53	syl	$$⊢\phi \to 1_R\in {\mathrm{Base}}_R$$
55	1	idomdomd	$$⊢\phi \to R\in \mathrm{Domn}$$
56		domnnzr	$$⊢R\in \mathrm{Domn}\to R\in \mathrm{NzRing}$$
57	55 56	syl	$$⊢\phi \to R\in \mathrm{NzRing}$$
58		eqid	$$⊢0_R=0_R$$
59	43 58	nzrnz	$$⊢R\in \mathrm{NzRing}\to 1_R\ne 0_R$$
60	57 59	syl	$$⊢\phi \to 1_R\ne 0_R$$
61		eqid	$$⊢{\mathrm{deg}}_1\left(R\right)={\mathrm{deg}}_1\left(R\right)$$
62	61 41 52 42 58	deg1scl	$$⊢\left(R\in \mathrm{Ring}\wedge 1_R\in {\mathrm{Base}}_R\wedge 1_R\ne 0_R\right)\to {\mathrm{deg}}_1\left(R\right)\left(\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(1_R\right)\right)=0$$
63	40 54 60 62	syl3anc	$$⊢\phi \to {\mathrm{deg}}_1\left(R\right)\left(\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(1_R\right)\right)=0$$
64	51 63	eqtrd	$$⊢\phi \to {\mathrm{deg}}_1\left(R\right)\left(0_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}\right)=0$$
65	39 64	eqtrd	$$⊢\phi \to {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in \varnothing }{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=0$$
66		sum0	$$⊢\sum _{n\in \varnothing }{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)=0$$
67	66	eqcomi	$$⊢0=\sum _{n\in \varnothing }{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)$$
68	67	a1i	$$⊢\phi \to 0=\sum _{n\in \varnothing }{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)$$
69	65 68	eqtrd	$$⊢\phi \to {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in \varnothing }{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in \varnothing }{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)$$
70		0red	$$⊢\phi \to 0\in ℝ$$
71	70	leidd	$$⊢\phi \to 0\le 0$$
72	65	eqcomd	$$⊢\phi \to 0={\mathrm{deg}}_1\left(R\right)\left(\underset{x\in \varnothing }{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)$$
73	71 72	breqtrd	$$⊢\phi \to 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in \varnothing }{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)$$
74	69 73	jca	$$⊢\phi \to \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in \varnothing }{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in \varnothing }{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in \varnothing }{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)$$
75		nfcv	$$⊢\underset{\_}{Ⅎ}yC$$
76		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋y/x⦌C$$
77		csbeq1a	$$⊢x=y\to C=⦋y/x⦌C$$
78	75 76 77	cbvmpt	$$⊢\left(x\in \left(b\cup \left\{c\right\}\right)⟼C\right)=\left(y\in \left(b\cup \left\{c\right\}\right)⟼⦋y/x⦌C\right)$$
79	78	a1i	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\right)\to \left(x\in \left(b\cup \left\{c\right\}\right)⟼C\right)=\left(y\in \left(b\cup \left\{c\right\}\right)⟼⦋y/x⦌C\right)$$
80	79	oveq2d	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\right)\to \underset{x\in b\cup \left\{c\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C=\underset{y\in b\cup \left\{c\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}⦋y/x⦌C$$
81	80	fveq2d	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\right)\to {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b\cup \left\{c\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)={\mathrm{deg}}_1\left(R\right)\left(\underset{y\in b\cup \left\{c\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}⦋y/x⦌C\right)$$
82		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}$$
83		eqid	$$⊢{+}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}={+}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}$$
84		isidom	$$⊢R\in \mathrm{IDomn}\leftrightarrow \left(R\in \mathrm{CRing}\wedge R\in \mathrm{Domn}\right)$$
85	1 84	sylib	$$⊢\phi \to \left(R\in \mathrm{CRing}\wedge R\in \mathrm{Domn}\right)$$
86	85	simpld	$$⊢\phi \to R\in \mathrm{CRing}$$
87	41	ply1crng	$$⊢R\in \mathrm{CRing}\to {\mathrm{Poly}}_1\left(R\right)\in \mathrm{CRing}$$
88	86 87	syl	$$⊢\phi \to {\mathrm{Poly}}_1\left(R\right)\in \mathrm{CRing}$$
89	44	crngmgp	$$⊢{\mathrm{Poly}}_1\left(R\right)\in \mathrm{CRing}\to {\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}\in \mathrm{CMnd}$$
90	88 89	syl	$$⊢\phi \to {\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}\in \mathrm{CMnd}$$
91	90	adantr	$$⊢\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\to {\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}\in \mathrm{CMnd}$$
92	91	adantr	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\right)\to {\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}\in \mathrm{CMnd}$$
93	2	ad2antrr	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\right)\to N\in \mathrm{Fin}$$
94		simplrl	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\right)\to b\subseteq N$$
95	93 94	ssfid	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\right)\to b\in \mathrm{Fin}$$
96	94	sselda	$$⊢\left(\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\right)\wedge y\in b\right)\to y\in N$$
97		r19.26	$$⊢\forall x\in N\left(C\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}\wedge C\ne 0_{{\mathrm{Poly}}_1\left(R\right)}\right)\leftrightarrow \left(\forall x\in NC\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}\wedge \forall x\in NC\ne 0_{{\mathrm{Poly}}_1\left(R\right)}\right)$$
98	97	biimpi	$$⊢\forall x\in N\left(C\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}\wedge C\ne 0_{{\mathrm{Poly}}_1\left(R\right)}\right)\to \left(\forall x\in NC\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}\wedge \forall x\in NC\ne 0_{{\mathrm{Poly}}_1\left(R\right)}\right)$$
99	3 98	syl	$$⊢\phi \to \left(\forall x\in NC\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}\wedge \forall x\in NC\ne 0_{{\mathrm{Poly}}_1\left(R\right)}\right)$$
100	99	simpld	$$⊢\phi \to \forall x\in NC\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
101	100	ad3antrrr	$$⊢\left(\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\right)\wedge y\in b\right)\to \forall x\in NC\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
102		rspcsbela	$$⊢\left(y\in N\wedge \forall x\in NC\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}\right)\to ⦋y/x⦌C\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
103	96 101 102	syl2anc	$$⊢\left(\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\right)\wedge y\in b\right)\to ⦋y/x⦌C\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
104		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
105	44 104	mgpbas	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}$$
106	103 105	eleqtrdi	$$⊢\left(\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\right)\wedge y\in b\right)\to ⦋y/x⦌C\in {\mathrm{Base}}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}$$
107		eldifi	$$⊢c\in \left(N\setminus b\right)\to c\in N$$
108	107	adantl	$$⊢\left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\to c\in N$$
109	108	adantl	$$⊢\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\to c\in N$$
110	109	adantr	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\right)\to c\in N$$
111		eldifn	$$⊢c\in \left(N\setminus b\right)\to \neg c\in b$$
112	111	adantl	$$⊢\left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\to \neg c\in b$$
113	112	adantl	$$⊢\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\to \neg c\in b$$
114	113	adantr	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\right)\to \neg c\in b$$
115	100	ad2antrr	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\right)\to \forall x\in NC\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
116		rspcsbela	$$⊢\left(c\in N\wedge \forall x\in NC\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}\right)\to ⦋c/x⦌C\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
117	110 115 116	syl2anc	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\right)\to ⦋c/x⦌C\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
118	117 105	eleqtrdi	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\right)\to ⦋c/x⦌C\in {\mathrm{Base}}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}$$
119		csbeq1	$$⊢y=c\to ⦋y/x⦌C=⦋c/x⦌C$$
120	82 83 92 95 106 110 114 118 119	gsumunsn	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\right)\to \underset{y\in b\cup \left\{c\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}⦋y/x⦌C=\left(\underset{y\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}},⦋y/x⦌C\right){+}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}⦋c/x⦌C$$
121	120	fveq2d	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\right)\to {\mathrm{deg}}_1\left(R\right)\left(\underset{y\in b\cup \left\{c\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}⦋y/x⦌C\right)={\mathrm{deg}}_1\left(R\right)\left(\left(\underset{y\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}},⦋y/x⦌C\right){+}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}⦋c/x⦌C\right)$$
122		eqid	$$⊢{\cdot }_{{\mathrm{Poly}}_1\left(R\right)}={\cdot }_{{\mathrm{Poly}}_1\left(R\right)}$$
123	44 122	mgpplusg	$$⊢{\cdot }_{{\mathrm{Poly}}_1\left(R\right)}={+}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}$$
124	123	eqcomi	$$⊢{+}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}={\cdot }_{{\mathrm{Poly}}_1\left(R\right)}$$
125		eqid	$$⊢0_{{\mathrm{Poly}}_1\left(R\right)}=0_{{\mathrm{Poly}}_1\left(R\right)}$$
126	55	adantr	$$⊢\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\to R\in \mathrm{Domn}$$
127	126	adantr	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\right)\to R\in \mathrm{Domn}$$
128	103	ralrimiva	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\right)\to \forall y\in b⦋y/x⦌C\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
129	105 92 95 128	gsummptcl	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\right)\to \underset{y\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}⦋y/x⦌C\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
130	41	ply1idom	$$⊢R\in \mathrm{IDomn}\to {\mathrm{Poly}}_1\left(R\right)\in \mathrm{IDomn}$$
131	1 130	syl	$$⊢\phi \to {\mathrm{Poly}}_1\left(R\right)\in \mathrm{IDomn}$$
132	131	adantr	$$⊢\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\to {\mathrm{Poly}}_1\left(R\right)\in \mathrm{IDomn}$$
133	132	adantr	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\right)\to {\mathrm{Poly}}_1\left(R\right)\in \mathrm{IDomn}$$
134	99	simprd	$$⊢\phi \to \forall x\in NC\ne 0_{{\mathrm{Poly}}_1\left(R\right)}$$
135	134	ad3antrrr	$$⊢\left(\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\right)\wedge y\in b\right)\to \forall x\in NC\ne 0_{{\mathrm{Poly}}_1\left(R\right)}$$
136		rspcsbnea	$$⊢\left(y\in N\wedge \forall x\in NC\ne 0_{{\mathrm{Poly}}_1\left(R\right)}\right)\to ⦋y/x⦌C\ne 0_{{\mathrm{Poly}}_1\left(R\right)}$$
137	96 135 136	syl2anc	$$⊢\left(\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\right)\wedge y\in b\right)\to ⦋y/x⦌C\ne 0_{{\mathrm{Poly}}_1\left(R\right)}$$
138	44 133 95 103 137	idomnnzgmulnz	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\right)\to \underset{y\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}⦋y/x⦌C\ne 0_{{\mathrm{Poly}}_1\left(R\right)}$$
139	134	ad2antrr	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\right)\to \forall x\in NC\ne 0_{{\mathrm{Poly}}_1\left(R\right)}$$
140		rspcsbnea	$$⊢\left(c\in N\wedge \forall x\in NC\ne 0_{{\mathrm{Poly}}_1\left(R\right)}\right)\to ⦋c/x⦌C\ne 0_{{\mathrm{Poly}}_1\left(R\right)}$$
141	110 139 140	syl2anc	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\right)\to ⦋c/x⦌C\ne 0_{{\mathrm{Poly}}_1\left(R\right)}$$
142	61 41 104 124 125 127 129 138 117 141	deg1mul	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\right)\to {\mathrm{deg}}_1\left(R\right)\left(\left(\underset{y\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}},⦋y/x⦌C\right){+}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}⦋c/x⦌C\right)={\mathrm{deg}}_1\left(R\right)\left(\underset{y\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}⦋y/x⦌C\right)+{\mathrm{deg}}_1\left(R\right)\left(⦋c/x⦌C\right)$$
143	75 76 77	cbvmpt	$$⊢\left(x\in b⟼C\right)=\left(y\in b⟼⦋y/x⦌C\right)$$
144	143	eqcomi	$$⊢\left(y\in b⟼⦋y/x⦌C\right)=\left(x\in b⟼C\right)$$
145	144	a1i	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\right)\to \left(y\in b⟼⦋y/x⦌C\right)=\left(x\in b⟼C\right)$$
146	145	oveq2d	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\right)\to \underset{y\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}⦋y/x⦌C=\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C$$
147	146	fveq2d	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\right)\to {\mathrm{deg}}_1\left(R\right)\left(\underset{y\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}⦋y/x⦌C\right)={\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)$$
148	147	oveq1d	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\right)\to {\mathrm{deg}}_1\left(R\right)\left(\underset{y\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}⦋y/x⦌C\right)+{\mathrm{deg}}_1\left(R\right)\left(⦋c/x⦌C\right)={\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)+{\mathrm{deg}}_1\left(R\right)\left(⦋c/x⦌C\right)$$
149		simpl	$$⊢\left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\to {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)$$
150	149	adantl	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\right)\to {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)$$
151	150	oveq1d	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\right)\to {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)+{\mathrm{deg}}_1\left(R\right)\left(⦋c/x⦌C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)+{\mathrm{deg}}_1\left(R\right)\left(⦋c/x⦌C\right)$$
152		nfv	$$⊢Ⅎn\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)$$
153		nfcv	$$⊢\underset{\_}{Ⅎ}n{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(c\right)\right)$$
154	2	adantr	$$⊢\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\to N\in \mathrm{Fin}$$
155		simprl	$$⊢\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\to b\subseteq N$$
156	154 155	ssfid	$$⊢\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\to b\in \mathrm{Fin}$$
157	75 76 77	cbvmpt	$$⊢\left(x\in N⟼C\right)=\left(y\in N⟼⦋y/x⦌C\right)$$
158	157	fveq1i	$$⊢\left(x\in N⟼C\right)\left(n\right)=\left(y\in N⟼⦋y/x⦌C\right)\left(n\right)$$
159	158	a1i	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge n\in b\right)\to \left(x\in N⟼C\right)\left(n\right)=\left(y\in N⟼⦋y/x⦌C\right)\left(n\right)$$
160	159	fveq2d	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge n\in b\right)\to {\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)={\mathrm{deg}}_1\left(R\right)\left(\left(y\in N⟼⦋y/x⦌C\right)\left(n\right)\right)$$
161		eqidd	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge n\in b\right)\to \left(y\in N⟼⦋y/x⦌C\right)=\left(y\in N⟼⦋y/x⦌C\right)$$
162		simpr	$$⊢\left(\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge n\in b\right)\wedge y=n\right)\to y=n$$
163	162	csbeq1d	$$⊢\left(\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge n\in b\right)\wedge y=n\right)\to ⦋y/x⦌C=⦋n/x⦌C$$
164	155	sselda	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge n\in b\right)\to n\in N$$
165	100	adantr	$$⊢\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\to \forall x\in NC\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
166	165	adantr	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge n\in b\right)\to \forall x\in NC\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
167		rspcsbela	$$⊢\left(n\in N\wedge \forall x\in NC\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}\right)\to ⦋n/x⦌C\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
168	164 166 167	syl2anc	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge n\in b\right)\to ⦋n/x⦌C\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
169	161 163 164 168	fvmptd	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge n\in b\right)\to \left(y\in N⟼⦋y/x⦌C\right)\left(n\right)=⦋n/x⦌C$$
170	169	fveq2d	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge n\in b\right)\to {\mathrm{deg}}_1\left(R\right)\left(\left(y\in N⟼⦋y/x⦌C\right)\left(n\right)\right)={\mathrm{deg}}_1\left(R\right)\left(⦋n/x⦌C\right)$$
171	40	adantr	$$⊢\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\to R\in \mathrm{Ring}$$
172	171	adantr	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge n\in b\right)\to R\in \mathrm{Ring}$$
173	134	ad2antrr	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge n\in b\right)\to \forall x\in NC\ne 0_{{\mathrm{Poly}}_1\left(R\right)}$$
174		rspcsbnea	$$⊢\left(n\in N\wedge \forall x\in NC\ne 0_{{\mathrm{Poly}}_1\left(R\right)}\right)\to ⦋n/x⦌C\ne 0_{{\mathrm{Poly}}_1\left(R\right)}$$
175	164 173 174	syl2anc	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge n\in b\right)\to ⦋n/x⦌C\ne 0_{{\mathrm{Poly}}_1\left(R\right)}$$
176	61 41 125 104	deg1nn0cl	$$⊢\left(R\in \mathrm{Ring}\wedge ⦋n/x⦌C\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}\wedge ⦋n/x⦌C\ne 0_{{\mathrm{Poly}}_1\left(R\right)}\right)\to {\mathrm{deg}}_1\left(R\right)\left(⦋n/x⦌C\right)\in {\mathbb{N}}_0$$
177	172 168 175 176	syl3anc	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge n\in b\right)\to {\mathrm{deg}}_1\left(R\right)\left(⦋n/x⦌C\right)\in {\mathbb{N}}_0$$
178	170 177	eqeltrd	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge n\in b\right)\to {\mathrm{deg}}_1\left(R\right)\left(\left(y\in N⟼⦋y/x⦌C\right)\left(n\right)\right)\in {\mathbb{N}}_0$$
179	160 178	eqeltrd	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge n\in b\right)\to {\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\in {\mathbb{N}}_0$$
180	179	nn0cnd	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge n\in b\right)\to {\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\in ℂ$$
181		2fveq3	$$⊢n=c\to {\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)={\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(c\right)\right)$$
182	109 165 116	syl2anc	$$⊢\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\to ⦋c/x⦌C\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
183		eqid	$$⊢\left(x\in N⟼C\right)=\left(x\in N⟼C\right)$$
184	183	fvmpts	$$⊢\left(c\in N\wedge ⦋c/x⦌C\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}\right)\to \left(x\in N⟼C\right)\left(c\right)=⦋c/x⦌C$$
185	109 182 184	syl2anc	$$⊢\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\to \left(x\in N⟼C\right)\left(c\right)=⦋c/x⦌C$$
186	185	fveq2d	$$⊢\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\to {\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(c\right)\right)={\mathrm{deg}}_1\left(R\right)\left(⦋c/x⦌C\right)$$
187	108 134 140	syl2anr	$$⊢\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\to ⦋c/x⦌C\ne 0_{{\mathrm{Poly}}_1\left(R\right)}$$
188	61 41 125 104	deg1nn0cl	$$⊢\left(R\in \mathrm{Ring}\wedge ⦋c/x⦌C\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}\wedge ⦋c/x⦌C\ne 0_{{\mathrm{Poly}}_1\left(R\right)}\right)\to {\mathrm{deg}}_1\left(R\right)\left(⦋c/x⦌C\right)\in {\mathbb{N}}_0$$
189	171 182 187 188	syl3anc	$$⊢\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\to {\mathrm{deg}}_1\left(R\right)\left(⦋c/x⦌C\right)\in {\mathbb{N}}_0$$
190	186 189	eqeltrd	$$⊢\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\to {\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(c\right)\right)\in {\mathbb{N}}_0$$
191	190	nn0cnd	$$⊢\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\to {\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(c\right)\right)\in ℂ$$
192	152 153 156 109 113 180 181 191	fsumsplitsn	$$⊢\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\to \sum _{n\in b\cup \left\{c\right\}}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)+{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(c\right)\right)$$
193	192	adantr	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\right)\to \sum _{n\in b\cup \left\{c\right\}}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)+{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(c\right)\right)$$
194	185	adantr	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\right)\to \left(x\in N⟼C\right)\left(c\right)=⦋c/x⦌C$$
195	194	fveq2d	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\right)\to {\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(c\right)\right)={\mathrm{deg}}_1\left(R\right)\left(⦋c/x⦌C\right)$$
196	195	oveq2d	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\right)\to \sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)+{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(c\right)\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)+{\mathrm{deg}}_1\left(R\right)\left(⦋c/x⦌C\right)$$
197	193 196	eqtrd	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\right)\to \sum _{n\in b\cup \left\{c\right\}}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)+{\mathrm{deg}}_1\left(R\right)\left(⦋c/x⦌C\right)$$
198	197	eqcomd	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\right)\to \sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)+{\mathrm{deg}}_1\left(R\right)\left(⦋c/x⦌C\right)=\sum _{n\in b\cup \left\{c\right\}}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)$$
199	151 198	eqtrd	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\right)\to {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)+{\mathrm{deg}}_1\left(R\right)\left(⦋c/x⦌C\right)=\sum _{n\in b\cup \left\{c\right\}}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)$$
200	148 199	eqtrd	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\right)\to {\mathrm{deg}}_1\left(R\right)\left(\underset{y\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}⦋y/x⦌C\right)+{\mathrm{deg}}_1\left(R\right)\left(⦋c/x⦌C\right)=\sum _{n\in b\cup \left\{c\right\}}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)$$
201	142 200	eqtrd	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\right)\to {\mathrm{deg}}_1\left(R\right)\left(\left(\underset{y\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}},⦋y/x⦌C\right){+}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}⦋c/x⦌C\right)=\sum _{n\in b\cup \left\{c\right\}}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)$$
202	121 201	eqtrd	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\right)\to {\mathrm{deg}}_1\left(R\right)\left(\underset{y\in b\cup \left\{c\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}⦋y/x⦌C\right)=\sum _{n\in b\cup \left\{c\right\}}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)$$
203	81 202	eqtrd	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\right)\to {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b\cup \left\{c\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b\cup \left\{c\right\}}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)$$
204	171	adantr	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\right)\to R\in \mathrm{Ring}$$
205	110	snssd	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\right)\to \left\{c\right\}\subseteq N$$
206	94 205	unssd	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\right)\to b\cup \left\{c\right\}\subseteq N$$
207	93 206	ssfid	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\right)\to b\cup \left\{c\right\}\in \mathrm{Fin}$$
208	165	adantr	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\right)\to \forall x\in NC\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
209		ssralv	$$⊢b\cup \left\{c\right\}\subseteq N\to \left(\forall x\in NC\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}\to \forall x\in \left(b\cup \left\{c\right\}\right)C\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}\right)$$
210	206 209	syl	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\right)\to \left(\forall x\in NC\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}\to \forall x\in \left(b\cup \left\{c\right\}\right)C\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}\right)$$
211	208 210	mpd	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\right)\to \forall x\in \left(b\cup \left\{c\right\}\right)C\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
212	105 92 207 211	gsummptcl	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\right)\to \underset{x\in b\cup \left\{c\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
213	78	oveq2i	$$⊢\underset{x\in b\cup \left\{c\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C=\underset{y\in b\cup \left\{c\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}⦋y/x⦌C$$
214	213	a1i	$$⊢\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\to \underset{x\in b\cup \left\{c\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C=\underset{y\in b\cup \left\{c\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}⦋y/x⦌C$$
215	109	snssd	$$⊢\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\to \left\{c\right\}\subseteq N$$
216	155 215	unssd	$$⊢\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\to b\cup \left\{c\right\}\subseteq N$$
217	154 216	ssfid	$$⊢\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\to b\cup \left\{c\right\}\in \mathrm{Fin}$$
218	216	sselda	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge y\in \left(b\cup \left\{c\right\}\right)\right)\to y\in N$$
219	165	adantr	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge y\in \left(b\cup \left\{c\right\}\right)\right)\to \forall x\in NC\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
220	218 219 102	syl2anc	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge y\in \left(b\cup \left\{c\right\}\right)\right)\to ⦋y/x⦌C\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
221	134	ad2antrr	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge y\in \left(b\cup \left\{c\right\}\right)\right)\to \forall x\in NC\ne 0_{{\mathrm{Poly}}_1\left(R\right)}$$
222	218 221 136	syl2anc	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge y\in \left(b\cup \left\{c\right\}\right)\right)\to ⦋y/x⦌C\ne 0_{{\mathrm{Poly}}_1\left(R\right)}$$
223	44 132 217 220 222	idomnnzgmulnz	$$⊢\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\to \underset{y\in b\cup \left\{c\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}⦋y/x⦌C\ne 0_{{\mathrm{Poly}}_1\left(R\right)}$$
224	214 223	eqnetrd	$$⊢\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\to \underset{x\in b\cup \left\{c\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\ne 0_{{\mathrm{Poly}}_1\left(R\right)}$$
225	224	adantr	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\right)\to \underset{x\in b\cup \left\{c\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\ne 0_{{\mathrm{Poly}}_1\left(R\right)}$$
226	61 41 125 104	deg1nn0cl	$$⊢\left(R\in \mathrm{Ring}\wedge \underset{x\in b\cup \left\{c\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}\wedge \underset{x\in b\cup \left\{c\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\ne 0_{{\mathrm{Poly}}_1\left(R\right)}\right)\to {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b\cup \left\{c\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\in {\mathbb{N}}_0$$
227	204 212 225 226	syl3anc	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\right)\to {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b\cup \left\{c\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\in {\mathbb{N}}_0$$
228	227	nn0ge0d	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\right)\to 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b\cup \left\{c\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)$$
229	203 228	jca	$$⊢\left(\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\wedge \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\right)\to \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b\cup \left\{c\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b\cup \left\{c\right\}}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b\cup \left\{c\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)$$
230	229	ex	$$⊢\left(\phi \wedge \left(b\subseteq N\wedge c\in \left(N\setminus b\right)\right)\right)\to \left(\left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\to \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b\cup \left\{c\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in b\cup \left\{c\right\}}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in b\cup \left\{c\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)\right)$$
231	10 17 24 31 74 230 2	findcard2d	$$⊢\phi \to \left({\mathrm{deg}}_1\left(R\right)\left(\underset{x\in N}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)=\sum _{n\in N}{\mathrm{deg}}_1\left(R\right)\left(\left(x\in N⟼C\right)\left(n\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(R\right)\left(\underset{x\in N}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}}C\right)\right)$$