Theorem aks6d1c5lem3

Description: Lemma for Claim 5, polynomial division with a linear power. (Contributed by metakunt, 5-May-2025)

	Ref	Expression
Hypotheses	aks6d1p5.1	$$⊢\phi \to K\in \mathrm{Field}$$
	aks6d1p5.2	$$⊢\phi \to P\in \mathbb{P}$$
	aks6d1c5.3	$$⊢P=\mathrm{chr}\left(K\right)$$
	aks6d1c5.4	$$⊢\phi \to A\in {\mathbb{N}}_0$$
	aks6d1c5.5	$$⊢\phi \to A<P$$
	aks6d1c5.6	$$⊢X={\mathrm{var}}_1\left(K\right)$$
	aks6d1c5.7	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}$$
	aks6d1c5.8	$$⊢G=\left(g\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)⟼\underset{i=0}{\overset{A}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}}}\left(g\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)\right)$$
	aks6d1c5p3.1	$$⊢\phi \to Y\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)$$
	aks6d1c5p3.2	$$⊢\phi \to W\in \left(0\dots A\right)$$
	aks6d1c5p3.3	$$⊢\phi \to C\in {\mathbb{N}}_0$$
	aks6d1c5p3.4	$$⊢\phi \to C\le Y\left(W\right)$$
	aks6d1c5p3.5	$$⊢Q={quot}_{\mathrm{1p}}\left(K\right)$$
	aks6d1c5p3.6	$$⊢S=\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)$$
	aks6d1c5p3.7	$$⊢M={\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}$$
Assertion	aks6d1c5lem3	$$⊢\phi \to G\left(Y\right)Q\left(C\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right)=\left(\left(Y\left(W\right)-C\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right){+}_M\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_M},\left(Y\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		aks6d1p5.1	$$⊢\phi \to K\in \mathrm{Field}$$
2		aks6d1p5.2	$$⊢\phi \to P\in \mathbb{P}$$
3		aks6d1c5.3	$$⊢P=\mathrm{chr}\left(K\right)$$
4		aks6d1c5.4	$$⊢\phi \to A\in {\mathbb{N}}_0$$
5		aks6d1c5.5	$$⊢\phi \to A<P$$
6		aks6d1c5.6	$$⊢X={\mathrm{var}}_1\left(K\right)$$
7		aks6d1c5.7	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}$$
8		aks6d1c5.8	$$⊢G=\left(g\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)⟼\underset{i=0}{\overset{A}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}}}\left(g\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)\right)$$
9		aks6d1c5p3.1	$$⊢\phi \to Y\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)$$
10		aks6d1c5p3.2	$$⊢\phi \to W\in \left(0\dots A\right)$$
11		aks6d1c5p3.3	$$⊢\phi \to C\in {\mathbb{N}}_0$$
12		aks6d1c5p3.4	$$⊢\phi \to C\le Y\left(W\right)$$
13		aks6d1c5p3.5	$$⊢Q={quot}_{\mathrm{1p}}\left(K\right)$$
14		aks6d1c5p3.6	$$⊢S=\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)$$
15		aks6d1c5p3.7	$$⊢M={\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}$$
16	1	fldcrngd	$$⊢\phi \to K\in \mathrm{CRing}$$
17		eqid	$$⊢{\mathrm{Poly}}_1\left(K\right)={\mathrm{Poly}}_1\left(K\right)$$
18	17	ply1crng	$$⊢K\in \mathrm{CRing}\to {\mathrm{Poly}}_1\left(K\right)\in \mathrm{CRing}$$
19	16 18	syl	$$⊢\phi \to {\mathrm{Poly}}_1\left(K\right)\in \mathrm{CRing}$$
20		crngring	$$⊢{\mathrm{Poly}}_1\left(K\right)\in \mathrm{CRing}\to {\mathrm{Poly}}_1\left(K\right)\in \mathrm{Ring}$$
21	19 20	syl	$$⊢\phi \to {\mathrm{Poly}}_1\left(K\right)\in \mathrm{Ring}$$
22		eqid	$$⊢{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}={\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}$$
23	22	ringmgp	$$⊢{\mathrm{Poly}}_1\left(K\right)\in \mathrm{Ring}\to {\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}\in \mathrm{Mnd}$$
24	21 23	syl	$$⊢\phi \to {\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}\in \mathrm{Mnd}$$
25	15 24	eqeltrid	$$⊢\phi \to M\in \mathrm{Mnd}$$
26	15	fveq2i	$$⊢{\mathrm{Base}}_M={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}$$
27		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
28	27	a1i	$$⊢\phi \to {\mathbb{N}}_0\in \mathrm{V}$$
29		ovexd	$$⊢\phi \to \left(0\dots A\right)\in \mathrm{V}$$
30		elmapg	$$⊢\left({\mathbb{N}}_0\in \mathrm{V}\wedge \left(0\dots A\right)\in \mathrm{V}\right)\to \left(Y\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)\leftrightarrow Y:\left(0\dots A\right)⟶{\mathbb{N}}_0\right)$$
31	28 29 30	syl2anc	$$⊢\phi \to \left(Y\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)\leftrightarrow Y:\left(0\dots A\right)⟶{\mathbb{N}}_0\right)$$
32	9 31	mpbid	$$⊢\phi \to Y:\left(0\dots A\right)⟶{\mathbb{N}}_0$$
33	32 10	ffvelcdmd	$$⊢\phi \to Y\left(W\right)\in {\mathbb{N}}_0$$
34	33	nn0zd	$$⊢\phi \to Y\left(W\right)\in \mathbb{Z}$$
35	11	nn0zd	$$⊢\phi \to C\in \mathbb{Z}$$
36	34 35	zsubcld	$$⊢\phi \to Y\left(W\right)-C\in \mathbb{Z}$$
37	33	nn0red	$$⊢\phi \to Y\left(W\right)\in ℝ$$
38	11	nn0red	$$⊢\phi \to C\in ℝ$$
39	37 38	subge0d	$$⊢\phi \to \left(0\le Y\left(W\right)-C\leftrightarrow C\le Y\left(W\right)\right)$$
40	12 39	mpbird	$$⊢\phi \to 0\le Y\left(W\right)-C$$
41	36 40	jca	$$⊢\phi \to \left(Y\left(W\right)-C\in \mathbb{Z}\wedge 0\le Y\left(W\right)-C\right)$$
42		elnn0z	$$⊢Y\left(W\right)-C\in {\mathbb{N}}_0\leftrightarrow \left(Y\left(W\right)-C\in \mathbb{Z}\wedge 0\le Y\left(W\right)-C\right)$$
43	41 42	sylibr	$$⊢\phi \to Y\left(W\right)-C\in {\mathbb{N}}_0$$
44	21	ringcmnd	$$⊢\phi \to {\mathrm{Poly}}_1\left(K\right)\in \mathrm{CMnd}$$
45		cmnmnd	$$⊢{\mathrm{Poly}}_1\left(K\right)\in \mathrm{CMnd}\to {\mathrm{Poly}}_1\left(K\right)\in \mathrm{Mnd}$$
46	44 45	syl	$$⊢\phi \to {\mathrm{Poly}}_1\left(K\right)\in \mathrm{Mnd}$$
47		crngring	$$⊢K\in \mathrm{CRing}\to K\in \mathrm{Ring}$$
48	16 47	syl	$$⊢\phi \to K\in \mathrm{Ring}$$
49		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
50	6 17 49	vr1cl	$$⊢K\in \mathrm{Ring}\to X\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
51	48 50	syl	$$⊢\phi \to X\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
52		eqid	$$⊢\mathrm{\mathbb{Z}RHom}\left(K\right)=\mathrm{\mathbb{Z}RHom}\left(K\right)$$
53	52	zrhrhm	$$⊢K\in \mathrm{Ring}\to \mathrm{\mathbb{Z}RHom}\left(K\right)\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}K\right)$$
54	48 53	syl	$$⊢\phi \to \mathrm{\mathbb{Z}RHom}\left(K\right)\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}K\right)$$
55		zringbas	$$⊢\mathbb{Z}={\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
56		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
57	55 56	rhmf	$$⊢\mathrm{\mathbb{Z}RHom}\left(K\right)\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}K\right)\to \mathrm{\mathbb{Z}RHom}\left(K\right):\mathbb{Z}⟶{\mathrm{Base}}_K$$
58	54 57	syl	$$⊢\phi \to \mathrm{\mathbb{Z}RHom}\left(K\right):\mathbb{Z}⟶{\mathrm{Base}}_K$$
59	10	elfzelzd	$$⊢\phi \to W\in \mathbb{Z}$$
60	58 59	ffvelcdmd	$$⊢\phi \to \mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\in {\mathrm{Base}}_K$$
61	17 14 56 49	ply1sclcl	$$⊢\left(K\in \mathrm{Ring}\wedge \mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\in {\mathrm{Base}}_K\right)\to S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
62	48 60 61	syl2anc	$$⊢\phi \to S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
63		eqid	$$⊢{+}_{{\mathrm{Poly}}_1\left(K\right)}={+}_{{\mathrm{Poly}}_1\left(K\right)}$$
64	49 63	mndcl	$$⊢\left({\mathrm{Poly}}_1\left(K\right)\in \mathrm{Mnd}\wedge X\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}\wedge S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}\right)\to X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
65	46 51 62 64	syl3anc	$$⊢\phi \to X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
66	22 49	mgpbas	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}$$
67	66	eqcomi	$$⊢{\mathrm{Base}}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
68	26 67	eqtri	$$⊢{\mathrm{Base}}_M={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
69	65 68	eleqtrrdi	$$⊢\phi \to X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\in {\mathrm{Base}}_M$$
70	26 7 24 43 69	mulgnn0cld	$$⊢\phi \to \left(Y\left(W\right)-C\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\in {\mathrm{Base}}_M$$
71		eqid	$$⊢{\mathrm{Base}}_M={\mathrm{Base}}_M$$
72	22	crngmgp	$$⊢{\mathrm{Poly}}_1\left(K\right)\in \mathrm{CRing}\to {\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}\in \mathrm{CMnd}$$
73	19 72	syl	$$⊢\phi \to {\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}\in \mathrm{CMnd}$$
74	15 73	eqeltrid	$$⊢\phi \to M\in \mathrm{CMnd}$$
75		fzfid	$$⊢\phi \to \left(0\dots A\right)\in \mathrm{Fin}$$
76		diffi	$$⊢\left(0\dots A\right)\in \mathrm{Fin}\to \left(0\dots A\right)\setminus \left\{W\right\}\in \mathrm{Fin}$$
77	75 76	syl	$$⊢\phi \to \left(0\dots A\right)\setminus \left\{W\right\}\in \mathrm{Fin}$$
78	24	adantr	$$⊢\left(\phi \wedge i\in \left(\left(0\dots A\right)\setminus \left\{W\right\}\right)\right)\to {\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}\in \mathrm{Mnd}$$
79	32	adantr	$$⊢\left(\phi \wedge i\in \left(\left(0\dots A\right)\setminus \left\{W\right\}\right)\right)\to Y:\left(0\dots A\right)⟶{\mathbb{N}}_0$$
80		eldifi	$$⊢i\in \left(\left(0\dots A\right)\setminus \left\{W\right\}\right)\to i\in \left(0\dots A\right)$$
81	80	adantl	$$⊢\left(\phi \wedge i\in \left(\left(0\dots A\right)\setminus \left\{W\right\}\right)\right)\to i\in \left(0\dots A\right)$$
82	79 81	ffvelcdmd	$$⊢\left(\phi \wedge i\in \left(\left(0\dots A\right)\setminus \left\{W\right\}\right)\right)\to Y\left(i\right)\in {\mathbb{N}}_0$$
83	46	adantr	$$⊢\left(\phi \wedge i\in \left(\left(0\dots A\right)\setminus \left\{W\right\}\right)\right)\to {\mathrm{Poly}}_1\left(K\right)\in \mathrm{Mnd}$$
84	51	adantr	$$⊢\left(\phi \wedge i\in \left(\left(0\dots A\right)\setminus \left\{W\right\}\right)\right)\to X\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
85	48	adantr	$$⊢\left(\phi \wedge i\in \left(\left(0\dots A\right)\setminus \left\{W\right\}\right)\right)\to K\in \mathrm{Ring}$$
86	85 53 57	3syl	$$⊢\left(\phi \wedge i\in \left(\left(0\dots A\right)\setminus \left\{W\right\}\right)\right)\to \mathrm{\mathbb{Z}RHom}\left(K\right):\mathbb{Z}⟶{\mathrm{Base}}_K$$
87		elfzelz	$$⊢i\in \left(0\dots A\right)\to i\in \mathbb{Z}$$
88	81 87	syl	$$⊢\left(\phi \wedge i\in \left(\left(0\dots A\right)\setminus \left\{W\right\}\right)\right)\to i\in \mathbb{Z}$$
89	86 88	ffvelcdmd	$$⊢\left(\phi \wedge i\in \left(\left(0\dots A\right)\setminus \left\{W\right\}\right)\right)\to \mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\in {\mathrm{Base}}_K$$
90	17 14 56 49	ply1sclcl	$$⊢\left(K\in \mathrm{Ring}\wedge \mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\in {\mathrm{Base}}_K\right)\to S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
91	85 89 90	syl2anc	$$⊢\left(\phi \wedge i\in \left(\left(0\dots A\right)\setminus \left\{W\right\}\right)\right)\to S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
92	49 63	mndcl	$$⊢\left({\mathrm{Poly}}_1\left(K\right)\in \mathrm{Mnd}\wedge X\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}\wedge S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}\right)\to X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
93	83 84 91 92	syl3anc	$$⊢\left(\phi \wedge i\in \left(\left(0\dots A\right)\setminus \left\{W\right\}\right)\right)\to X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
94	93 68	eleqtrrdi	$$⊢\left(\phi \wedge i\in \left(\left(0\dots A\right)\setminus \left\{W\right\}\right)\right)\to X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\in {\mathrm{Base}}_M$$
95	26 7	mulgnn0cl	$$⊢\left({\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}\in \mathrm{Mnd}\wedge Y\left(i\right)\in {\mathbb{N}}_0\wedge X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\in {\mathrm{Base}}_M\right)\to Y\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\in {\mathrm{Base}}_M$$
96	78 82 94 95	syl3anc	$$⊢\left(\phi \wedge i\in \left(\left(0\dots A\right)\setminus \left\{W\right\}\right)\right)\to Y\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\in {\mathrm{Base}}_M$$
97	96	ralrimiva	$$⊢\phi \to \forall i\in \left(\left(0\dots A\right)\setminus \left\{W\right\}\right)Y\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\in {\mathrm{Base}}_M$$
98	71 74 77 97	gsummptcl	$$⊢\phi \to \underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_M}\left(Y\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)\in {\mathrm{Base}}_M$$
99		eqid	$$⊢{+}_M={+}_M$$
100	71 99	mndcl	$$⊢\left(M\in \mathrm{Mnd}\wedge \left(Y\left(W\right)-C\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\in {\mathrm{Base}}_M\wedge \underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_M}\left(Y\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)\in {\mathrm{Base}}_M\right)\to \left(\left(Y\left(W\right)-C\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right){+}_M\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_M},\left(Y\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)\right)\in {\mathrm{Base}}_M$$
101	25 70 98 100	syl3anc	$$⊢\phi \to \left(\left(Y\left(W\right)-C\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right){+}_M\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_M},\left(Y\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)\right)\in {\mathrm{Base}}_M$$
102	101 68	eleqtrdi	$$⊢\phi \to \left(\left(Y\left(W\right)-C\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right){+}_M\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_M},\left(Y\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
103	71 99	cmncom	$$⊢\left(M\in \mathrm{CMnd}\wedge \left(Y\left(W\right)-C\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\in {\mathrm{Base}}_M\wedge \underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_M}\left(Y\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)\in {\mathrm{Base}}_M\right)\to \left(\left(Y\left(W\right)-C\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right){+}_M\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_M},\left(Y\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)\right)=\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_M},\left(Y\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)\right){+}_M\left(\left(Y\left(W\right)-C\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right)$$
104	74 70 98 103	syl3anc	$$⊢\phi \to \left(\left(Y\left(W\right)-C\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right){+}_M\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_M},\left(Y\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)\right)=\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_M},\left(Y\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)\right){+}_M\left(\left(Y\left(W\right)-C\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right)$$
105	104	oveq1d	$$⊢\phi \to \left(\left(\left(Y\left(W\right)-C\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right){+}_M\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_M},\left(Y\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)\right)\right){\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(C\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right)=\left(\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_M},\left(Y\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)\right){+}_M\left(\left(Y\left(W\right)-C\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right)\right){\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(C\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right)$$
106		eqid	$$⊢{\cdot }_{{\mathrm{Poly}}_1\left(K\right)}={\cdot }_{{\mathrm{Poly}}_1\left(K\right)}$$
107	15 106	mgpplusg	$$⊢{\cdot }_{{\mathrm{Poly}}_1\left(K\right)}={+}_M$$
108	107	eqcomi	$$⊢{+}_M={\cdot }_{{\mathrm{Poly}}_1\left(K\right)}$$
109	108	a1i	$$⊢\phi \to {+}_M={\cdot }_{{\mathrm{Poly}}_1\left(K\right)}$$
110	109	oveqd	$$⊢\phi \to \left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_M},\left(Y\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)\right){+}_M\left(\left(Y\left(W\right)-C\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right)=\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_M},\left(Y\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)\right){\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(\left(Y\left(W\right)-C\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right)$$
111	110	oveq1d	$$⊢\phi \to \left(\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_M},\left(Y\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)\right){+}_M\left(\left(Y\left(W\right)-C\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right)\right){\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(C\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right)=\left(\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_M},\left(Y\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)\right){\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(\left(Y\left(W\right)-C\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right)\right){\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(C\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right)$$
112	98 68	eleqtrdi	$$⊢\phi \to \underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_M}\left(Y\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
113	70 68	eleqtrdi	$$⊢\phi \to \left(Y\left(W\right)-C\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
114	66 7 24 11 65	mulgnn0cld	$$⊢\phi \to C\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
115	49 106 21 112 113 114	ringassd	$$⊢\phi \to \left(\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_M},\left(Y\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)\right){\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(\left(Y\left(W\right)-C\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right)\right){\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(C\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right)=\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_M},\left(Y\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)\right){\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(\left(\left(Y\left(W\right)-C\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right){\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(C\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right)\right)$$
116	111 115	eqtrd	$$⊢\phi \to \left(\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_M},\left(Y\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)\right){+}_M\left(\left(Y\left(W\right)-C\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right)\right){\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(C\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right)=\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_M},\left(Y\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)\right){\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(\left(\left(Y\left(W\right)-C\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right){\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(C\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right)\right)$$
117	105 116	eqtrd	$$⊢\phi \to \left(\left(\left(Y\left(W\right)-C\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right){+}_M\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_M},\left(Y\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)\right)\right){\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(C\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right)=\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_M},\left(Y\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)\right){\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(\left(\left(Y\left(W\right)-C\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right){\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(C\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right)\right)$$
118	117	oveq2d	$$⊢\phi \to G\left(Y\right){-}_{{\mathrm{Poly}}_1\left(K\right)}\left(\left(\left(\left(Y\left(W\right)-C\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right){+}_M\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_M},\left(Y\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)\right)\right){\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(C\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right)\right)=G\left(Y\right){-}_{{\mathrm{Poly}}_1\left(K\right)}\left(\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_M},\left(Y\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)\right){\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(\left(\left(Y\left(W\right)-C\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right){\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(C\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right)\right)\right)$$
119	37	recnd	$$⊢\phi \to Y\left(W\right)\in ℂ$$
120	38	recnd	$$⊢\phi \to C\in ℂ$$
121	119 120	npcand	$$⊢\phi \to Y\left(W\right)-C+C=Y\left(W\right)$$
122	121	eqcomd	$$⊢\phi \to Y\left(W\right)=Y\left(W\right)-C+C$$
123	122	oveq1d	$$⊢\phi \to Y\left(W\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)=\left(Y\left(W\right)-C+C\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)$$
124	66	a1i	$$⊢\phi \to {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}$$
125	65 124	eleqtrd	$$⊢\phi \to X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\in {\mathrm{Base}}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}$$
126	43 11 125	3jca	$$⊢\phi \to \left(Y\left(W\right)-C\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\wedge X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\in {\mathrm{Base}}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\right)$$
127		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}$$
128	22 106	mgpplusg	$$⊢{\cdot }_{{\mathrm{Poly}}_1\left(K\right)}={+}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}$$
129	127 7 128	mulgnn0dir	$$⊢\left({\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}\in \mathrm{Mnd}\wedge \left(Y\left(W\right)-C\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\wedge X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\in {\mathrm{Base}}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\right)\right)\to \left(Y\left(W\right)-C+C\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)=\left(\left(Y\left(W\right)-C\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right){\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(C\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right)$$
130	24 126 129	syl2anc	$$⊢\phi \to \left(Y\left(W\right)-C+C\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)=\left(\left(Y\left(W\right)-C\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right){\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(C\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right)$$
131	123 130	eqtr2d	$$⊢\phi \to \left(\left(Y\left(W\right)-C\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right){\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(C\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right)=Y\left(W\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)$$
132	131	oveq2d	$$⊢\phi \to \left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_M},\left(Y\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)\right){\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(\left(\left(Y\left(W\right)-C\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right){\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(C\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right)\right)=\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_M},\left(Y\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)\right){\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(Y\left(W\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right)$$
133	8	a1i	$$⊢\phi \to G=\left(g\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)⟼\underset{i=0}{\overset{A}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}}}\left(g\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)\right)$$
134	15	eqcomi	$$⊢{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}=M$$
135	134	a1i	$$⊢\left(\phi \wedge g=Y\right)\to {\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}=M$$
136		simplr	$$⊢\left(\left(\phi \wedge g=Y\right)\wedge i\in \left(0\dots A\right)\right)\to g=Y$$
137	136	fveq1d	$$⊢\left(\left(\phi \wedge g=Y\right)\wedge i\in \left(0\dots A\right)\right)\to g\left(i\right)=Y\left(i\right)$$
138	14	eqcomi	$$⊢\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)=S$$
139	138	a1i	$$⊢\left(\left(\phi \wedge g=Y\right)\wedge i\in \left(0\dots A\right)\right)\to \mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)=S$$
140	139	fveq1d	$$⊢\left(\left(\phi \wedge g=Y\right)\wedge i\in \left(0\dots A\right)\right)\to \mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)=S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)$$
141	140	oveq2d	$$⊢\left(\left(\phi \wedge g=Y\right)\wedge i\in \left(0\dots A\right)\right)\to X{+}_{{\mathrm{Poly}}_1\left(K\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)=X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)$$
142	137 141	oveq12d	$$⊢\left(\left(\phi \wedge g=Y\right)\wedge i\in \left(0\dots A\right)\right)\to g\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)=Y\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)$$
143	142	mpteq2dva	$$⊢\left(\phi \wedge g=Y\right)\to \left(i\in \left(0\dots A\right)⟼g\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)=\left(i\in \left(0\dots A\right)⟼Y\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)$$
144	135 143	oveq12d	$$⊢\left(\phi \wedge g=Y\right)\to \underset{i=0}{\overset{A}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}}}\left(g\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)=\underset{i=0}{\overset{A}{{\sum }_M}}\left(Y\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)$$
145		ovexd	$$⊢\phi \to \underset{i=0}{\overset{A}{{\sum }_M}}\left(Y\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)\in \mathrm{V}$$
146	133 144 9 145	fvmptd	$$⊢\phi \to G\left(Y\right)=\underset{i=0}{\overset{A}{{\sum }_M}}\left(Y\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)$$
147	10	snssd	$$⊢\phi \to \left\{W\right\}\subseteq \left(0\dots A\right)$$
148		undifr	$$⊢\left\{W\right\}\subseteq \left(0\dots A\right)\leftrightarrow \left(\left(0\dots A\right)\setminus \left\{W\right\}\right)\cup \left\{W\right\}=\left(0\dots A\right)$$
149	147 148	sylib	$$⊢\phi \to \left(\left(0\dots A\right)\setminus \left\{W\right\}\right)\cup \left\{W\right\}=\left(0\dots A\right)$$
150	149	eqcomd	$$⊢\phi \to \left(0\dots A\right)=\left(\left(0\dots A\right)\setminus \left\{W\right\}\right)\cup \left\{W\right\}$$
151	150	mpteq1d	$$⊢\phi \to \left(i\in \left(0\dots A\right)⟼Y\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)=\left(i\in \left(\left(\left(0\dots A\right)\setminus \left\{W\right\}\right)\cup \left\{W\right\}\right)⟼Y\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)$$
152	151	oveq2d	$$⊢\phi \to \underset{i=0}{\overset{A}{{\sum }_M}}\left(Y\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)=\underset{i\in \left(\left(0\dots A\right)\setminus \left\{W\right\}\right)\cup \left\{W\right\}}{{\sum }_M}\left(Y\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)$$
153	146 152	eqtrd	$$⊢\phi \to G\left(Y\right)=\underset{i\in \left(\left(0\dots A\right)\setminus \left\{W\right\}\right)\cup \left\{W\right\}}{{\sum }_M}\left(Y\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)$$
154		neldifsnd	$$⊢\phi \to \neg W\in \left(\left(0\dots A\right)\setminus \left\{W\right\}\right)$$
155	26 7 24 33 69	mulgnn0cld	$$⊢\phi \to Y\left(W\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\in {\mathrm{Base}}_M$$
156		fveq2	$$⊢i=W\to Y\left(i\right)=Y\left(W\right)$$
157		2fveq3	$$⊢i=W\to S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)=S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)$$
158	157	oveq2d	$$⊢i=W\to X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)=X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)$$
159	156 158	oveq12d	$$⊢i=W\to Y\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)=Y\left(W\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)$$
160	71 107 74 77 96 10 154 155 159	gsumunsn	$$⊢\phi \to \underset{i\in \left(\left(0\dots A\right)\setminus \left\{W\right\}\right)\cup \left\{W\right\}}{{\sum }_M}\left(Y\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)=\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_M},\left(Y\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)\right){\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(Y\left(W\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right)$$
161	153 160	eqtr2d	$$⊢\phi \to \left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_M},\left(Y\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)\right){\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(Y\left(W\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right)=G\left(Y\right)$$
162	132 161	eqtrd	$$⊢\phi \to \left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_M},\left(Y\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)\right){\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(\left(\left(Y\left(W\right)-C\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right){\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(C\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right)\right)=G\left(Y\right)$$
163	162	oveq2d	$$⊢\phi \to G\left(Y\right){-}_{{\mathrm{Poly}}_1\left(K\right)}\left(\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_M},\left(Y\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)\right){\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(\left(\left(Y\left(W\right)-C\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right){\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(C\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right)\right)\right)=G\left(Y\right){-}_{{\mathrm{Poly}}_1\left(K\right)}G\left(Y\right)$$
164	21	ringgrpd	$$⊢\phi \to {\mathrm{Poly}}_1\left(K\right)\in \mathrm{Grp}$$
165	1 2 3 4 5 6 7 8	aks6d1c5lem0	$$⊢\phi \to G:{{\mathbb{N}}_0}^{\left(0\dots A\right)}⟶{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
166	165 9	ffvelcdmd	$$⊢\phi \to G\left(Y\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
167		eqid	$$⊢0_{{\mathrm{Poly}}_1\left(K\right)}=0_{{\mathrm{Poly}}_1\left(K\right)}$$
168		eqid	$$⊢{-}_{{\mathrm{Poly}}_1\left(K\right)}={-}_{{\mathrm{Poly}}_1\left(K\right)}$$
169	49 167 168	grpsubid	$$⊢\left({\mathrm{Poly}}_1\left(K\right)\in \mathrm{Grp}\wedge G\left(Y\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}\right)\to G\left(Y\right){-}_{{\mathrm{Poly}}_1\left(K\right)}G\left(Y\right)=0_{{\mathrm{Poly}}_1\left(K\right)}$$
170	164 166 169	syl2anc	$$⊢\phi \to G\left(Y\right){-}_{{\mathrm{Poly}}_1\left(K\right)}G\left(Y\right)=0_{{\mathrm{Poly}}_1\left(K\right)}$$
171	163 170	eqtrd	$$⊢\phi \to G\left(Y\right){-}_{{\mathrm{Poly}}_1\left(K\right)}\left(\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_M},\left(Y\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)\right){\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(\left(\left(Y\left(W\right)-C\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right){\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(C\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right)\right)\right)=0_{{\mathrm{Poly}}_1\left(K\right)}$$
172	118 171	eqtrd	$$⊢\phi \to G\left(Y\right){-}_{{\mathrm{Poly}}_1\left(K\right)}\left(\left(\left(\left(Y\left(W\right)-C\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right){+}_M\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_M},\left(Y\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)\right)\right){\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(C\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right)\right)=0_{{\mathrm{Poly}}_1\left(K\right)}$$
173	172	fveq2d	$$⊢\phi \to {\mathrm{deg}}_1\left(K\right)\left(G\left(Y\right){-}_{{\mathrm{Poly}}_1\left(K\right)}\left(\left(\left(\left(Y\left(W\right)-C\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right){+}_M\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_M},\left(Y\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)\right)\right){\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(C\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right)\right)\right)={\mathrm{deg}}_1\left(K\right)\left(0_{{\mathrm{Poly}}_1\left(K\right)}\right)$$
174		eqid	$$⊢{\mathrm{deg}}_1\left(K\right)={\mathrm{deg}}_1\left(K\right)$$
175	174 17 167	deg1z	$$⊢K\in \mathrm{Ring}\to {\mathrm{deg}}_1\left(K\right)\left(0_{{\mathrm{Poly}}_1\left(K\right)}\right)=\mathrm{-\infty }$$
176	48 175	syl	$$⊢\phi \to {\mathrm{deg}}_1\left(K\right)\left(0_{{\mathrm{Poly}}_1\left(K\right)}\right)=\mathrm{-\infty }$$
177	1	flddrngd	$$⊢\phi \to K\in \mathrm{DivRing}$$
178		drngdomn	$$⊢K\in \mathrm{DivRing}\to K\in \mathrm{Domn}$$
179	177 178	syl	$$⊢\phi \to K\in \mathrm{Domn}$$
180	17	ply1domn	$$⊢K\in \mathrm{Domn}\to {\mathrm{Poly}}_1\left(K\right)\in \mathrm{Domn}$$
181	179 180	syl	$$⊢\phi \to {\mathrm{Poly}}_1\left(K\right)\in \mathrm{Domn}$$
182	19 181	jca	$$⊢\phi \to \left({\mathrm{Poly}}_1\left(K\right)\in \mathrm{CRing}\wedge {\mathrm{Poly}}_1\left(K\right)\in \mathrm{Domn}\right)$$
183		isidom	$$⊢{\mathrm{Poly}}_1\left(K\right)\in \mathrm{IDomn}\leftrightarrow \left({\mathrm{Poly}}_1\left(K\right)\in \mathrm{CRing}\wedge {\mathrm{Poly}}_1\left(K\right)\in \mathrm{Domn}\right)$$
184	182 183	sylibr	$$⊢\phi \to {\mathrm{Poly}}_1\left(K\right)\in \mathrm{IDomn}$$
185	174 17 49	deg1xrcl	$$⊢S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}\to {\mathrm{deg}}_1\left(K\right)\left(S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\in {ℝ}^{*}$$
186	62 185	syl	$$⊢\phi \to {\mathrm{deg}}_1\left(K\right)\left(S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\in {ℝ}^{*}$$
187		0xr	$$⊢0\in {ℝ}^{*}$$
188	187	a1i	$$⊢\phi \to 0\in {ℝ}^{*}$$
189	174 17 49	deg1xrcl	$$⊢X\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}\to {\mathrm{deg}}_1\left(K\right)\left(X\right)\in {ℝ}^{*}$$
190	51 189	syl	$$⊢\phi \to {\mathrm{deg}}_1\left(K\right)\left(X\right)\in {ℝ}^{*}$$
191	174 17 56 14	deg1sclle	$$⊢\left(K\in \mathrm{Ring}\wedge \mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\in {\mathrm{Base}}_K\right)\to {\mathrm{deg}}_1\left(K\right)\left(S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\le 0$$
192	48 60 191	syl2anc	$$⊢\phi \to {\mathrm{deg}}_1\left(K\right)\left(S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\le 0$$
193		0lt1	$$⊢0<1$$
194	193	a1i	$$⊢\phi \to 0<1$$
195	51 66	eleqtrdi	$$⊢\phi \to X\in {\mathrm{Base}}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}$$
196	127 7	mulg1	$$⊢X\in {\mathrm{Base}}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\to 1\underset{\dot{}}{\times }X=X$$
197	195 196	syl	$$⊢\phi \to 1\underset{\dot{}}{\times }X=X$$
198	197	fveq2d	$$⊢\phi \to {\mathrm{deg}}_1\left(K\right)\left(1\underset{\dot{}}{\times }X\right)={\mathrm{deg}}_1\left(K\right)\left(X\right)$$
199		isfld	$$⊢K\in \mathrm{Field}\leftrightarrow \left(K\in \mathrm{DivRing}\wedge K\in \mathrm{CRing}\right)$$
200	199	biimpi	$$⊢K\in \mathrm{Field}\to \left(K\in \mathrm{DivRing}\wedge K\in \mathrm{CRing}\right)$$
201	1 200	syl	$$⊢\phi \to \left(K\in \mathrm{DivRing}\wedge K\in \mathrm{CRing}\right)$$
202	201	simpld	$$⊢\phi \to K\in \mathrm{DivRing}$$
203		drngnzr	$$⊢K\in \mathrm{DivRing}\to K\in \mathrm{NzRing}$$
204	202 203	syl	$$⊢\phi \to K\in \mathrm{NzRing}$$
205		1nn0	$$⊢1\in {\mathbb{N}}_0$$
206	205	a1i	$$⊢\phi \to 1\in {\mathbb{N}}_0$$
207	174 17 6 22 7	deg1pw	$$⊢\left(K\in \mathrm{NzRing}\wedge 1\in {\mathbb{N}}_0\right)\to {\mathrm{deg}}_1\left(K\right)\left(1\underset{\dot{}}{\times }X\right)=1$$
208	204 206 207	syl2anc	$$⊢\phi \to {\mathrm{deg}}_1\left(K\right)\left(1\underset{\dot{}}{\times }X\right)=1$$
209	198 208	eqtr3d	$$⊢\phi \to {\mathrm{deg}}_1\left(K\right)\left(X\right)=1$$
210	209	eqcomd	$$⊢\phi \to 1={\mathrm{deg}}_1\left(K\right)\left(X\right)$$
211	194 210	breqtrd	$$⊢\phi \to 0<{\mathrm{deg}}_1\left(K\right)\left(X\right)$$
212	186 188 190 192 211	xrlelttrd	$$⊢\phi \to {\mathrm{deg}}_1\left(K\right)\left(S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)<{\mathrm{deg}}_1\left(K\right)\left(X\right)$$
213	17 174 48 49 63 51 62 212	deg1add	$$⊢\phi \to {\mathrm{deg}}_1\left(K\right)\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)={\mathrm{deg}}_1\left(K\right)\left(X\right)$$
214	209 206	eqeltrd	$$⊢\phi \to {\mathrm{deg}}_1\left(K\right)\left(X\right)\in {\mathbb{N}}_0$$
215	213 214	eqeltrd	$$⊢\phi \to {\mathrm{deg}}_1\left(K\right)\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\in {\mathbb{N}}_0$$
216	174 17 167 49	deg1nn0clb	$$⊢\left(K\in \mathrm{Ring}\wedge X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}\right)\to \left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\ne 0_{{\mathrm{Poly}}_1\left(K\right)}\leftrightarrow {\mathrm{deg}}_1\left(K\right)\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\in {\mathbb{N}}_0\right)$$
217	48 65 216	syl2anc	$$⊢\phi \to \left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\ne 0_{{\mathrm{Poly}}_1\left(K\right)}\leftrightarrow {\mathrm{deg}}_1\left(K\right)\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\in {\mathbb{N}}_0\right)$$
218	215 217	mpbird	$$⊢\phi \to X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\ne 0_{{\mathrm{Poly}}_1\left(K\right)}$$
219	184 65 218 11 7	idomnnzpownz	$$⊢\phi \to C\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\ne 0_{{\mathrm{Poly}}_1\left(K\right)}$$
220	174 17 167 49	deg1nn0clb	$$⊢\left(K\in \mathrm{Ring}\wedge C\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}\right)\to \left(C\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\ne 0_{{\mathrm{Poly}}_1\left(K\right)}\leftrightarrow {\mathrm{deg}}_1\left(K\right)\left(C\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right)\in {\mathbb{N}}_0\right)$$
221	48 114 220	syl2anc	$$⊢\phi \to \left(C\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\ne 0_{{\mathrm{Poly}}_1\left(K\right)}\leftrightarrow {\mathrm{deg}}_1\left(K\right)\left(C\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right)\in {\mathbb{N}}_0\right)$$
222	219 221	mpbid	$$⊢\phi \to {\mathrm{deg}}_1\left(K\right)\left(C\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right)\in {\mathbb{N}}_0$$
223	222	nn0red	$$⊢\phi \to {\mathrm{deg}}_1\left(K\right)\left(C\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right)\in ℝ$$
224	223	mnfltd	$$⊢\phi \to \mathrm{-\infty }<{\mathrm{deg}}_1\left(K\right)\left(C\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right)$$
225	176 224	eqbrtrd	$$⊢\phi \to {\mathrm{deg}}_1\left(K\right)\left(0_{{\mathrm{Poly}}_1\left(K\right)}\right)<{\mathrm{deg}}_1\left(K\right)\left(C\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right)$$
226	173 225	eqbrtrd	$$⊢\phi \to {\mathrm{deg}}_1\left(K\right)\left(G\left(Y\right){-}_{{\mathrm{Poly}}_1\left(K\right)}\left(\left(\left(\left(Y\left(W\right)-C\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right){+}_M\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_M},\left(Y\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)\right)\right){\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(C\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right)\right)\right)<{\mathrm{deg}}_1\left(K\right)\left(C\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right)$$
227	102 226	jca	$$⊢\phi \to \left(\left(\left(Y\left(W\right)-C\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right){+}_M\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_M},\left(Y\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}\wedge {\mathrm{deg}}_1\left(K\right)\left(G\left(Y\right){-}_{{\mathrm{Poly}}_1\left(K\right)}\left(\left(\left(\left(Y\left(W\right)-C\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right){+}_M\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_M},\left(Y\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)\right)\right){\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(C\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right)\right)\right)<{\mathrm{deg}}_1\left(K\right)\left(C\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right)\right)$$
228		eqid	$$⊢{Unic}_{\mathrm{1p}}\left(K\right)={Unic}_{\mathrm{1p}}\left(K\right)$$
229	17 49 167 228	drnguc1p	$$⊢\left(K\in \mathrm{DivRing}\wedge C\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}\wedge C\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\ne 0_{{\mathrm{Poly}}_1\left(K\right)}\right)\to C\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\in {Unic}_{\mathrm{1p}}\left(K\right)$$
230	177 114 219 229	syl3anc	$$⊢\phi \to C\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\in {Unic}_{\mathrm{1p}}\left(K\right)$$
231	13 17 49 174 168 106 228	q1peqb	$$⊢\left(K\in \mathrm{Ring}\wedge G\left(Y\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}\wedge C\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\in {Unic}_{\mathrm{1p}}\left(K\right)\right)\to \left(\left(\left(\left(Y\left(W\right)-C\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right){+}_M\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_M},\left(Y\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}\wedge {\mathrm{deg}}_1\left(K\right)\left(G\left(Y\right){-}_{{\mathrm{Poly}}_1\left(K\right)}\left(\left(\left(\left(Y\left(W\right)-C\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right){+}_M\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_M},\left(Y\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)\right)\right){\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(C\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right)\right)\right)<{\mathrm{deg}}_1\left(K\right)\left(C\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right)\right)\leftrightarrow G\left(Y\right)Q\left(C\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right)=\left(\left(Y\left(W\right)-C\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right){+}_M\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_M},\left(Y\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)\right)\right)$$
232	48 166 230 231	syl3anc	$$⊢\phi \to \left(\left(\left(\left(Y\left(W\right)-C\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right){+}_M\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_M},\left(Y\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}\wedge {\mathrm{deg}}_1\left(K\right)\left(G\left(Y\right){-}_{{\mathrm{Poly}}_1\left(K\right)}\left(\left(\left(\left(Y\left(W\right)-C\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right){+}_M\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_M},\left(Y\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)\right)\right){\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(C\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right)\right)\right)<{\mathrm{deg}}_1\left(K\right)\left(C\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right)\right)\leftrightarrow G\left(Y\right)Q\left(C\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right)=\left(\left(Y\left(W\right)-C\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right){+}_M\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_M},\left(Y\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)\right)\right)$$
233	227 232	mpbid	$$⊢\phi \to G\left(Y\right)Q\left(C\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right)=\left(\left(Y\left(W\right)-C\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\right){+}_M\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_M},\left(Y\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}S\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)\right)$$