Theorem aks6d1c5lem2

Description: Lemma for Claim 5, contradiction of different evaluations that map to the same. (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)$$
	aks6d1c5p2.1	$$⊢\phi \to Y\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)$$
	aks6d1c5p2.2	$$⊢\phi \to Z\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)$$
	aks6d1c5p2.3	$$⊢\phi \to G\left(Y\right)=G\left(Z\right)$$
	aks6d1c5p2.4	$$⊢\phi \to W\in \left(0\dots A\right)$$
	aks6d1c5p2.5	$$⊢\phi \to Y\left(W\right)<Z\left(W\right)$$
Assertion	aks6d1c5lem2	$$⊢\phi \to 0_K\ne 0_K$$

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		aks6d1c5p2.1	$$⊢\phi \to Y\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)$$
10		aks6d1c5p2.2	$$⊢\phi \to Z\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)$$
11		aks6d1c5p2.3	$$⊢\phi \to G\left(Y\right)=G\left(Z\right)$$
12		aks6d1c5p2.4	$$⊢\phi \to W\in \left(0\dots A\right)$$
13		aks6d1c5p2.5	$$⊢\phi \to Y\left(W\right)<Z\left(W\right)$$
14		eqid	$$⊢{\mathrm{eval}}_1\left(K\right)={\mathrm{eval}}_1\left(K\right)$$
15		eqid	$$⊢{\mathrm{Poly}}_1\left(K\right)={\mathrm{Poly}}_1\left(K\right)$$
16		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
17		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
18		isfld	$$⊢K\in \mathrm{Field}\leftrightarrow \left(K\in \mathrm{DivRing}\wedge K\in \mathrm{CRing}\right)$$
19	18	simprbi	$$⊢K\in \mathrm{Field}\to K\in \mathrm{CRing}$$
20	1 19	syl	$$⊢\phi \to K\in \mathrm{CRing}$$
21	20	crngringd	$$⊢\phi \to K\in \mathrm{Ring}$$
22		eqid	$$⊢\mathrm{\mathbb{Z}RHom}\left(K\right)=\mathrm{\mathbb{Z}RHom}\left(K\right)$$
23	22	zrhrhm	$$⊢K\in \mathrm{Ring}\to \mathrm{\mathbb{Z}RHom}\left(K\right)\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}K\right)$$
24	21 23	syl	$$⊢\phi \to \mathrm{\mathbb{Z}RHom}\left(K\right)\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}K\right)$$
25		zringbas	$$⊢\mathbb{Z}={\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
26	25 16	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$$
27	24 26	syl	$$⊢\phi \to \mathrm{\mathbb{Z}RHom}\left(K\right):\mathbb{Z}⟶{\mathrm{Base}}_K$$
28		0zd	$$⊢\phi \to 0\in \mathbb{Z}$$
29	12	elfzelzd	$$⊢\phi \to W\in \mathbb{Z}$$
30	28 29	zsubcld	$$⊢\phi \to 0-W\in \mathbb{Z}$$
31	27 30	ffvelcdmd	$$⊢\phi \to \mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\in {\mathrm{Base}}_K$$
32		eqid	$$⊢{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}={\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}$$
33	32 17	mgpbas	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}$$
34	15	ply1crng	$$⊢K\in \mathrm{CRing}\to {\mathrm{Poly}}_1\left(K\right)\in \mathrm{CRing}$$
35	20 34	syl	$$⊢\phi \to {\mathrm{Poly}}_1\left(K\right)\in \mathrm{CRing}$$
36	32	crngmgp	$$⊢{\mathrm{Poly}}_1\left(K\right)\in \mathrm{CRing}\to {\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}\in \mathrm{CMnd}$$
37	35 36	syl	$$⊢\phi \to {\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}\in \mathrm{CMnd}$$
38	37	cmnmndd	$$⊢\phi \to {\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}\in \mathrm{Mnd}$$
39		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
40	39	a1i	$$⊢\phi \to {\mathbb{N}}_0\in \mathrm{V}$$
41		ovexd	$$⊢\phi \to \left(0\dots A\right)\in \mathrm{V}$$
42		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)$$
43	40 41 42	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)$$
44	9 43	mpbid	$$⊢\phi \to Y:\left(0\dots A\right)⟶{\mathbb{N}}_0$$
45	44 12	ffvelcdmd	$$⊢\phi \to Y\left(W\right)\in {\mathbb{N}}_0$$
46	45	nn0zd	$$⊢\phi \to Y\left(W\right)\in \mathbb{Z}$$
47	46 46	zsubcld	$$⊢\phi \to Y\left(W\right)-Y\left(W\right)\in \mathbb{Z}$$
48		0red	$$⊢\phi \to 0\in ℝ$$
49	48	leidd	$$⊢\phi \to 0\le 0$$
50	45	nn0red	$$⊢\phi \to Y\left(W\right)\in ℝ$$
51	50	recnd	$$⊢\phi \to Y\left(W\right)\in ℂ$$
52	51	subidd	$$⊢\phi \to Y\left(W\right)-Y\left(W\right)=0$$
53	52	eqcomd	$$⊢\phi \to 0=Y\left(W\right)-Y\left(W\right)$$
54	49 53	breqtrd	$$⊢\phi \to 0\le Y\left(W\right)-Y\left(W\right)$$
55	47 54	jca	$$⊢\phi \to \left(Y\left(W\right)-Y\left(W\right)\in \mathbb{Z}\wedge 0\le Y\left(W\right)-Y\left(W\right)\right)$$
56		elnn0z	$$⊢Y\left(W\right)-Y\left(W\right)\in {\mathbb{N}}_0\leftrightarrow \left(Y\left(W\right)-Y\left(W\right)\in \mathbb{Z}\wedge 0\le Y\left(W\right)-Y\left(W\right)\right)$$
57	55 56	sylibr	$$⊢\phi \to Y\left(W\right)-Y\left(W\right)\in {\mathbb{N}}_0$$
58	14 6 16 15 17 20 31	evl1vard	$$⊢\phi \to \left(X\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}\wedge {\mathrm{eval}}_1\left(K\right)\left(X\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)=\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)$$
59		eqid	$$⊢\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)=\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)$$
60	27 29	ffvelcdmd	$$⊢\phi \to \mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\in {\mathrm{Base}}_K$$
61	14 15 16 59 17 20 60 31	evl1scad	$$⊢\phi \to \left(\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}\wedge {\mathrm{eval}}_1\left(K\right)\left(\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)=\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)$$
62		eqid	$$⊢{+}_{{\mathrm{Poly}}_1\left(K\right)}={+}_{{\mathrm{Poly}}_1\left(K\right)}$$
63		eqid	$$⊢{+}_K={+}_K$$
64	14 15 16 17 20 31 58 61 62 63	evl1addd	$$⊢\phi \to \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(W\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}\wedge {\mathrm{eval}}_1\left(K\right)\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(W\right)\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)=\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right){+}_K\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)$$
65	64	simpld	$$⊢\phi \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(W\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
66	33 7 38 57 65	mulgnn0cld	$$⊢\phi \to \left(Y\left(W\right)-Y\left(W\right)\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(W\right)\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
67	52	oveq1d	$$⊢\phi \to \left(Y\left(W\right)-Y\left(W\right)\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(W\right)\right)\right)=0\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(W\right)\right)\right)$$
68		eqid	$$⊢0_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}=0_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}$$
69	33 68 7	mulg0	$$⊢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(W\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}\to 0\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(W\right)\right)\right)=0_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}$$
70	65 69	syl	$$⊢\phi \to 0\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(W\right)\right)\right)=0_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}$$
71	67 70	eqtrd	$$⊢\phi \to \left(Y\left(W\right)-Y\left(W\right)\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(W\right)\right)\right)=0_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}$$
72	71	fveq2d	$$⊢\phi \to {\mathrm{eval}}_1\left(K\right)\left(\left(Y\left(W\right)-Y\left(W\right)\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(W\right)\right)\right)\right)={\mathrm{eval}}_1\left(K\right)\left(0_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\right)$$
73	72	fveq1d	$$⊢\phi \to {\mathrm{eval}}_1\left(K\right)\left(\left(Y\left(W\right)-Y\left(W\right)\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(W\right)\right)\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)={\mathrm{eval}}_1\left(K\right)\left(0_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)$$
74		eqid	$$⊢1_{{\mathrm{Poly}}_1\left(K\right)}=1_{{\mathrm{Poly}}_1\left(K\right)}$$
75	32 74	ringidval	$$⊢1_{{\mathrm{Poly}}_1\left(K\right)}=0_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}$$
76	75	eqcomi	$$⊢0_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}=1_{{\mathrm{Poly}}_1\left(K\right)}$$
77	76	a1i	$$⊢\phi \to 0_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}=1_{{\mathrm{Poly}}_1\left(K\right)}$$
78	77	fveq2d	$$⊢\phi \to {\mathrm{eval}}_1\left(K\right)\left(0_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\right)={\mathrm{eval}}_1\left(K\right)\left(1_{{\mathrm{Poly}}_1\left(K\right)}\right)$$
79	78	fveq1d	$$⊢\phi \to {\mathrm{eval}}_1\left(K\right)\left(0_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)={\mathrm{eval}}_1\left(K\right)\left(1_{{\mathrm{Poly}}_1\left(K\right)}\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)$$
80	15 6 32 7	ply1idvr1	$$⊢K\in \mathrm{Ring}\to 0\underset{\dot{}}{\times }X=1_{{\mathrm{Poly}}_1\left(K\right)}$$
81	80	eqcomd	$$⊢K\in \mathrm{Ring}\to 1_{{\mathrm{Poly}}_1\left(K\right)}=0\underset{\dot{}}{\times }X$$
82	21 81	syl	$$⊢\phi \to 1_{{\mathrm{Poly}}_1\left(K\right)}=0\underset{\dot{}}{\times }X$$
83	82	fveq2d	$$⊢\phi \to {\mathrm{eval}}_1\left(K\right)\left(1_{{\mathrm{Poly}}_1\left(K\right)}\right)={\mathrm{eval}}_1\left(K\right)\left(0\underset{\dot{}}{\times }X\right)$$
84	83	fveq1d	$$⊢\phi \to {\mathrm{eval}}_1\left(K\right)\left(1_{{\mathrm{Poly}}_1\left(K\right)}\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)={\mathrm{eval}}_1\left(K\right)\left(0\underset{\dot{}}{\times }X\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)$$
85		eqid	$$⊢{\cdot }_{{\mathrm{mulGrp}}_K}={\cdot }_{{\mathrm{mulGrp}}_K}$$
86	53 57	eqeltrd	$$⊢\phi \to 0\in {\mathbb{N}}_0$$
87	14 15 16 17 20 31 58 7 85 86	evl1expd	$$⊢\phi \to \left(0\underset{\dot{}}{\times }X\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}\wedge {\mathrm{eval}}_1\left(K\right)\left(0\underset{\dot{}}{\times }X\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)=0{\cdot }_{{\mathrm{mulGrp}}_K}\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)$$
88	87	simprd	$$⊢\phi \to {\mathrm{eval}}_1\left(K\right)\left(0\underset{\dot{}}{\times }X\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)=0{\cdot }_{{\mathrm{mulGrp}}_K}\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)$$
89		eqid	$$⊢{\mathrm{mulGrp}}_K={\mathrm{mulGrp}}_K$$
90	89 16	mgpbas	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_{{\mathrm{mulGrp}}_K}$$
91	90	a1i	$$⊢\phi \to {\mathrm{Base}}_K={\mathrm{Base}}_{{\mathrm{mulGrp}}_K}$$
92	31 91	eleqtrd	$$⊢\phi \to \mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\in {\mathrm{Base}}_{{\mathrm{mulGrp}}_K}$$
93		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{mulGrp}}_K}={\mathrm{Base}}_{{\mathrm{mulGrp}}_K}$$
94		eqid	$$⊢0_{{\mathrm{mulGrp}}_K}=0_{{\mathrm{mulGrp}}_K}$$
95	93 94 85	mulg0	$$⊢\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\in {\mathrm{Base}}_{{\mathrm{mulGrp}}_K}\to 0{\cdot }_{{\mathrm{mulGrp}}_K}\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)=0_{{\mathrm{mulGrp}}_K}$$
96	92 95	syl	$$⊢\phi \to 0{\cdot }_{{\mathrm{mulGrp}}_K}\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)=0_{{\mathrm{mulGrp}}_K}$$
97		eqid	$$⊢1_K=1_K$$
98	89 97	ringidval	$$⊢1_K=0_{{\mathrm{mulGrp}}_K}$$
99	98	eqcomi	$$⊢0_{{\mathrm{mulGrp}}_K}=1_K$$
100	99	a1i	$$⊢\phi \to 0_{{\mathrm{mulGrp}}_K}=1_K$$
101	96 100	eqtrd	$$⊢\phi \to 0{\cdot }_{{\mathrm{mulGrp}}_K}\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)=1_K$$
102	88 101	eqtrd	$$⊢\phi \to {\mathrm{eval}}_1\left(K\right)\left(0\underset{\dot{}}{\times }X\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)=1_K$$
103	84 102	eqtrd	$$⊢\phi \to {\mathrm{eval}}_1\left(K\right)\left(1_{{\mathrm{Poly}}_1\left(K\right)}\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)=1_K$$
104	79 103	eqtrd	$$⊢\phi \to {\mathrm{eval}}_1\left(K\right)\left(0_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)=1_K$$
105	73 104	eqtrd	$$⊢\phi \to {\mathrm{eval}}_1\left(K\right)\left(\left(Y\left(W\right)-Y\left(W\right)\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(W\right)\right)\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)=1_K$$
106	66 105	jca	$$⊢\phi \to \left(\left(Y\left(W\right)-Y\left(W\right)\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(W\right)\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}\wedge {\mathrm{eval}}_1\left(K\right)\left(\left(Y\left(W\right)-Y\left(W\right)\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(W\right)\right)\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)=1_K\right)$$
107		fzfid	$$⊢\phi \to \left(0\dots A\right)\in \mathrm{Fin}$$
108		diffi	$$⊢\left(0\dots A\right)\in \mathrm{Fin}\to \left(0\dots A\right)\setminus \left\{W\right\}\in \mathrm{Fin}$$
109	107 108	syl	$$⊢\phi \to \left(0\dots A\right)\setminus \left\{W\right\}\in \mathrm{Fin}$$
110	38	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}$$
111	44	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$$
112		eldifi	$$⊢i\in \left(\left(0\dots A\right)\setminus \left\{W\right\}\right)\to i\in \left(0\dots A\right)$$
113	112	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)$$
114	111 113	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$$
115	35	crngringd	$$⊢\phi \to {\mathrm{Poly}}_1\left(K\right)\in \mathrm{Ring}$$
116		ringcmn	$$⊢{\mathrm{Poly}}_1\left(K\right)\in \mathrm{Ring}\to {\mathrm{Poly}}_1\left(K\right)\in \mathrm{CMnd}$$
117	115 116	syl	$$⊢\phi \to {\mathrm{Poly}}_1\left(K\right)\in \mathrm{CMnd}$$
118		cmnmnd	$$⊢{\mathrm{Poly}}_1\left(K\right)\in \mathrm{CMnd}\to {\mathrm{Poly}}_1\left(K\right)\in \mathrm{Mnd}$$
119	117 118	syl	$$⊢\phi \to {\mathrm{Poly}}_1\left(K\right)\in \mathrm{Mnd}$$
120	119	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}$$
121	58	simpld	$$⊢\phi \to X\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
122	121	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)}$$
123	21	adantr	$$⊢\left(\phi \wedge i\in \left(\left(0\dots A\right)\setminus \left\{W\right\}\right)\right)\to K\in \mathrm{Ring}$$
124	123 23 26	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$$
125	113	elfzelzd	$$⊢\left(\phi \wedge i\in \left(\left(0\dots A\right)\setminus \left\{W\right\}\right)\right)\to i\in \mathbb{Z}$$
126	124 125	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$$
127	15 59 16 17	ply1sclcl	$$⊢\left(K\in \mathrm{Ring}\wedge \mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\in {\mathrm{Base}}_K\right)\to \mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
128	123 126 127	syl2anc	$$⊢\left(\phi \wedge i\in \left(\left(0\dots A\right)\setminus \left\{W\right\}\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)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
129	17 62	mndcl	$$⊢\left({\mathrm{Poly}}_1\left(K\right)\in \mathrm{Mnd}\wedge X\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}\wedge \mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\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)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
130	120 122 128 129	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)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
131	33 7 110 114 130	mulgnn0cld	$$⊢\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)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
132	131	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)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
133	33 37 109 132	gsummptcl	$$⊢\phi \to \underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}}\left(Y\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)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
134	132	r19.21bi	$$⊢\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)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
135	134	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)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
136	14 15 32 16 17 89 20 31 135 109	evl1gprodd	$$⊢\phi \to {\mathrm{eval}}_1\left(K\right)\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}}\left(Y\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)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)=\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_{{\mathrm{mulGrp}}_K}}{\mathrm{eval}}_1\left(K\right)\left(Y\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(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)$$
137	133 136	jca	$$⊢\phi \to \left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}}\left(Y\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)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}\wedge {\mathrm{eval}}_1\left(K\right)\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}}\left(Y\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)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)=\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_{{\mathrm{mulGrp}}_K}}{\mathrm{eval}}_1\left(K\right)\left(Y\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(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)\right)$$
138		eqid	$$⊢{\cdot }_{{\mathrm{Poly}}_1\left(K\right)}={\cdot }_{{\mathrm{Poly}}_1\left(K\right)}$$
139	32 138	mgpplusg	$$⊢{\cdot }_{{\mathrm{Poly}}_1\left(K\right)}={+}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}$$
140	139	eqcomi	$$⊢{+}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}={\cdot }_{{\mathrm{Poly}}_1\left(K\right)}$$
141		eqid	$$⊢{\cdot }_K={\cdot }_K$$
142	14 15 16 17 20 31 106 137 140 141	evl1muld	$$⊢\phi \to \left(\left(\left(Y\left(W\right)-Y\left(W\right)\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(W\right)\right)\right)\right){+}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}},\left(Y\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)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}\wedge {\mathrm{eval}}_1\left(K\right)\left(\left(\left(Y\left(W\right)-Y\left(W\right)\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(W\right)\right)\right)\right){+}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}},\left(Y\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)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)=1_K{\cdot }_K\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_{{\mathrm{mulGrp}}_K}},{\mathrm{eval}}_1\left(K\right)\left(Y\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(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)\right)\right)$$
143	142	simprd	$$⊢\phi \to {\mathrm{eval}}_1\left(K\right)\left(\left(\left(Y\left(W\right)-Y\left(W\right)\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(W\right)\right)\right)\right){+}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}},\left(Y\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)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)=1_K{\cdot }_K\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_{{\mathrm{mulGrp}}_K}},{\mathrm{eval}}_1\left(K\right)\left(Y\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(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)\right)$$
144		fldidom	$$⊢K\in \mathrm{Field}\to K\in \mathrm{IDomn}$$
145	1 144	syl	$$⊢\phi \to K\in \mathrm{IDomn}$$
146		isidom	$$⊢K\in \mathrm{IDomn}\leftrightarrow \left(K\in \mathrm{CRing}\wedge K\in \mathrm{Domn}\right)$$
147	145 146	sylib	$$⊢\phi \to \left(K\in \mathrm{CRing}\wedge K\in \mathrm{Domn}\right)$$
148	147	simprd	$$⊢\phi \to K\in \mathrm{Domn}$$
149	98	a1i	$$⊢\phi \to 1_K=0_{{\mathrm{mulGrp}}_K}$$
150	89	ringmgp	$$⊢K\in \mathrm{Ring}\to {\mathrm{mulGrp}}_K\in \mathrm{Mnd}$$
151	21 150	syl	$$⊢\phi \to {\mathrm{mulGrp}}_K\in \mathrm{Mnd}$$
152	90 94	mndidcl	$$⊢{\mathrm{mulGrp}}_K\in \mathrm{Mnd}\to 0_{{\mathrm{mulGrp}}_K}\in {\mathrm{Base}}_K$$
153	151 152	syl	$$⊢\phi \to 0_{{\mathrm{mulGrp}}_K}\in {\mathrm{Base}}_K$$
154	149 153	eqeltrd	$$⊢\phi \to 1_K\in {\mathrm{Base}}_K$$
155	1	flddrngd	$$⊢\phi \to K\in \mathrm{DivRing}$$
156		eqid	$$⊢0_K=0_K$$
157	156 97	drngunz	$$⊢K\in \mathrm{DivRing}\to 1_K\ne 0_K$$
158	155 157	syl	$$⊢\phi \to 1_K\ne 0_K$$
159	154 158	jca	$$⊢\phi \to \left(1_K\in {\mathrm{Base}}_K\wedge 1_K\ne 0_K\right)$$
160	89	crngmgp	$$⊢K\in \mathrm{CRing}\to {\mathrm{mulGrp}}_K\in \mathrm{CMnd}$$
161	20 160	syl	$$⊢\phi \to {\mathrm{mulGrp}}_K\in \mathrm{CMnd}$$
162	20	adantr	$$⊢\left(\phi \wedge i\in \left(\left(0\dots A\right)\setminus \left\{W\right\}\right)\right)\to K\in \mathrm{CRing}$$
163	31	adantr	$$⊢\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(0-W\right)\in {\mathrm{Base}}_K$$
164	14 15 16 17 162 163 131	fveval1fvcl	$$⊢\left(\phi \wedge i\in \left(\left(0\dots A\right)\setminus \left\{W\right\}\right)\right)\to {\mathrm{eval}}_1\left(K\right)\left(Y\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(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)\in {\mathrm{Base}}_K$$
165	164	ralrimiva	$$⊢\phi \to \forall i\in \left(\left(0\dots A\right)\setminus \left\{W\right\}\right){\mathrm{eval}}_1\left(K\right)\left(Y\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(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)\in {\mathrm{Base}}_K$$
166	90 161 109 165	gsummptcl	$$⊢\phi \to \underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_{{\mathrm{mulGrp}}_K}}{\mathrm{eval}}_1\left(K\right)\left(Y\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(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)\in {\mathrm{Base}}_K$$
167	33	a1i	$$⊢\left(\phi \wedge i\in \left(\left(0\dots A\right)\setminus \left\{W\right\}\right)\right)\to {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}$$
168	130 167	eleqtrd	$$⊢\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)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\in {\mathrm{Base}}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}$$
169	33	eqcomi	$$⊢{\mathrm{Base}}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
170	169	a1i	$$⊢\left(\phi \wedge i\in \left(\left(0\dots A\right)\setminus \left\{W\right\}\right)\right)\to {\mathrm{Base}}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
171	168 170	eleqtrd	$$⊢\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)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
172		eqidd	$$⊢\left(\phi \wedge i\in \left(\left(0\dots A\right)\setminus \left\{W\right\}\right)\right)\to {\mathrm{eval}}_1\left(K\right)\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)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)={\mathrm{eval}}_1\left(K\right)\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)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)$$
173	171 172	jca	$$⊢\left(\phi \wedge i\in \left(\left(0\dots A\right)\setminus \left\{W\right\}\right)\right)\to \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)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}\wedge {\mathrm{eval}}_1\left(K\right)\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)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)={\mathrm{eval}}_1\left(K\right)\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)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)\right)$$
174	14 15 16 17 162 163 173 7 85 114	evl1expd	$$⊢\left(\phi \wedge i\in \left(\left(0\dots A\right)\setminus \left\{W\right\}\right)\right)\to \left(Y\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)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}\wedge {\mathrm{eval}}_1\left(K\right)\left(Y\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(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)=Y\left(i\right){\cdot }_{{\mathrm{mulGrp}}_K}{\mathrm{eval}}_1\left(K\right)\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)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)\right)$$
175	174	simprd	$$⊢\left(\phi \wedge i\in \left(\left(0\dots A\right)\setminus \left\{W\right\}\right)\right)\to {\mathrm{eval}}_1\left(K\right)\left(Y\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(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)=Y\left(i\right){\cdot }_{{\mathrm{mulGrp}}_K}{\mathrm{eval}}_1\left(K\right)\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)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)$$
176	145	adantr	$$⊢\left(\phi \wedge i\in \left(\left(0\dots A\right)\setminus \left\{W\right\}\right)\right)\to K\in \mathrm{IDomn}$$
177	14 15 16 17 162 163 171	fveval1fvcl	$$⊢\left(\phi \wedge i\in \left(\left(0\dots A\right)\setminus \left\{W\right\}\right)\right)\to {\mathrm{eval}}_1\left(K\right)\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)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)\in {\mathrm{Base}}_K$$
178		eldifsni	$$⊢i\in \left(\left(0\dots A\right)\setminus \left\{W\right\}\right)\to i\ne W$$
179	178	adantl	$$⊢\left(\phi \wedge i\in \left(\left(0\dots A\right)\setminus \left\{W\right\}\right)\right)\to i\ne W$$
180	1	adantr	$$⊢\left(\phi \wedge i\in \left(\left(0\dots A\right)\setminus \left\{W\right\}\right)\right)\to K\in \mathrm{Field}$$
181	2	adantr	$$⊢\left(\phi \wedge i\in \left(\left(0\dots A\right)\setminus \left\{W\right\}\right)\right)\to P\in \mathbb{P}$$
182	4	adantr	$$⊢\left(\phi \wedge i\in \left(\left(0\dots A\right)\setminus \left\{W\right\}\right)\right)\to A\in {\mathbb{N}}_0$$
183	5	adantr	$$⊢\left(\phi \wedge i\in \left(\left(0\dots A\right)\setminus \left\{W\right\}\right)\right)\to A<P$$
184	12	adantr	$$⊢\left(\phi \wedge i\in \left(\left(0\dots A\right)\setminus \left\{W\right\}\right)\right)\to W\in \left(0\dots A\right)$$
185	180 181 3 182 183 6 7 8 113 184	aks6d1c5lem1	$$⊢\left(\phi \wedge i\in \left(\left(0\dots A\right)\setminus \left\{W\right\}\right)\right)\to \left(i=W\leftrightarrow {\mathrm{eval}}_1\left(K\right)\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)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)=0_K\right)$$
186	185	necon3bid	$$⊢\left(\phi \wedge i\in \left(\left(0\dots A\right)\setminus \left\{W\right\}\right)\right)\to \left(i\ne W\leftrightarrow {\mathrm{eval}}_1\left(K\right)\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)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)\ne 0_K\right)$$
187	179 186	mpbid	$$⊢\left(\phi \wedge i\in \left(\left(0\dots A\right)\setminus \left\{W\right\}\right)\right)\to {\mathrm{eval}}_1\left(K\right)\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)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)\ne 0_K$$
188	176 177 187 114 85	idomnnzpownz	$$⊢\left(\phi \wedge i\in \left(\left(0\dots A\right)\setminus \left\{W\right\}\right)\right)\to Y\left(i\right){\cdot }_{{\mathrm{mulGrp}}_K}{\mathrm{eval}}_1\left(K\right)\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)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)\ne 0_K$$
189	175 188	eqnetrd	$$⊢\left(\phi \wedge i\in \left(\left(0\dots A\right)\setminus \left\{W\right\}\right)\right)\to {\mathrm{eval}}_1\left(K\right)\left(Y\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(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)\ne 0_K$$
190	89 145 109 164 189	idomnnzgmulnz	$$⊢\phi \to \underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_{{\mathrm{mulGrp}}_K}}{\mathrm{eval}}_1\left(K\right)\left(Y\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(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)\ne 0_K$$
191	166 190	jca	$$⊢\phi \to \left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_{{\mathrm{mulGrp}}_K}}{\mathrm{eval}}_1\left(K\right)\left(Y\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(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)\in {\mathrm{Base}}_K\wedge \underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_{{\mathrm{mulGrp}}_K}}{\mathrm{eval}}_1\left(K\right)\left(Y\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(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)\ne 0_K\right)$$
192	16 141 156	domnmuln0	$$⊢\left(K\in \mathrm{Domn}\wedge \left(1_K\in {\mathrm{Base}}_K\wedge 1_K\ne 0_K\right)\wedge \left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_{{\mathrm{mulGrp}}_K}}{\mathrm{eval}}_1\left(K\right)\left(Y\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(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)\in {\mathrm{Base}}_K\wedge \underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_{{\mathrm{mulGrp}}_K}}{\mathrm{eval}}_1\left(K\right)\left(Y\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(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)\ne 0_K\right)\right)\to 1_K{\cdot }_K\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_{{\mathrm{mulGrp}}_K}},{\mathrm{eval}}_1\left(K\right)\left(Y\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(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)\right)\ne 0_K$$
193	148 159 191 192	syl3anc	$$⊢\phi \to 1_K{\cdot }_K\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_{{\mathrm{mulGrp}}_K}},{\mathrm{eval}}_1\left(K\right)\left(Y\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(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)\right)\ne 0_K$$
194	143 193	eqnetrd	$$⊢\phi \to {\mathrm{eval}}_1\left(K\right)\left(\left(\left(Y\left(W\right)-Y\left(W\right)\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(W\right)\right)\right)\right){+}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}},\left(Y\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)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)\ne 0_K$$
195	194	necomd	$$⊢\phi \to 0_K\ne {\mathrm{eval}}_1\left(K\right)\left(\left(\left(Y\left(W\right)-Y\left(W\right)\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(W\right)\right)\right)\right){+}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}},\left(Y\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)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)$$
196	50	leidd	$$⊢\phi \to Y\left(W\right)\le Y\left(W\right)$$
197		eqid	$$⊢{quot}_{\mathrm{1p}}\left(K\right)={quot}_{\mathrm{1p}}\left(K\right)$$
198	1 2 3 4 5 6 7 8 9 12 45 196 197 59 32	aks6d1c5lem3	$$⊢\phi \to G\left(Y\right){quot}_{\mathrm{1p}}\left(K\right)\left(Y\left(W\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(W\right)\right)\right)\right)=\left(\left(Y\left(W\right)-Y\left(W\right)\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(W\right)\right)\right)\right){+}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}},\left(Y\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)$$
199	198	eqcomd	$$⊢\phi \to \left(\left(Y\left(W\right)-Y\left(W\right)\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(W\right)\right)\right)\right){+}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}},\left(Y\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)=G\left(Y\right){quot}_{\mathrm{1p}}\left(K\right)\left(Y\left(W\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(W\right)\right)\right)\right)$$
200	11	oveq1d	$$⊢\phi \to G\left(Y\right){quot}_{\mathrm{1p}}\left(K\right)\left(Y\left(W\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(W\right)\right)\right)\right)=G\left(Z\right){quot}_{\mathrm{1p}}\left(K\right)\left(Y\left(W\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(W\right)\right)\right)\right)$$
201		elmapg	$$⊢\left({\mathbb{N}}_0\in \mathrm{V}\wedge \left(0\dots A\right)\in \mathrm{V}\right)\to \left(Z\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)\leftrightarrow Z:\left(0\dots A\right)⟶{\mathbb{N}}_0\right)$$
202	40 41 201	syl2anc	$$⊢\phi \to \left(Z\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)\leftrightarrow Z:\left(0\dots A\right)⟶{\mathbb{N}}_0\right)$$
203	10 202	mpbid	$$⊢\phi \to Z:\left(0\dots A\right)⟶{\mathbb{N}}_0$$
204	203 12	ffvelcdmd	$$⊢\phi \to Z\left(W\right)\in {\mathbb{N}}_0$$
205	204	nn0red	$$⊢\phi \to Z\left(W\right)\in ℝ$$
206	50 205 13	ltled	$$⊢\phi \to Y\left(W\right)\le Z\left(W\right)$$
207	1 2 3 4 5 6 7 8 10 12 45 206 197 59 32	aks6d1c5lem3	$$⊢\phi \to G\left(Z\right){quot}_{\mathrm{1p}}\left(K\right)\left(Y\left(W\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(W\right)\right)\right)\right)=\left(\left(Z\left(W\right)-Y\left(W\right)\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(W\right)\right)\right)\right){+}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}},\left(Z\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)$$
208	199 200 207	3eqtrd	$$⊢\phi \to \left(\left(Y\left(W\right)-Y\left(W\right)\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(W\right)\right)\right)\right){+}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}},\left(Y\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)=\left(\left(Z\left(W\right)-Y\left(W\right)\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(W\right)\right)\right)\right){+}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}},\left(Z\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)$$
209	208	fveq2d	$$⊢\phi \to {\mathrm{eval}}_1\left(K\right)\left(\left(\left(Y\left(W\right)-Y\left(W\right)\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(W\right)\right)\right)\right){+}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}},\left(Y\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)\right)={\mathrm{eval}}_1\left(K\right)\left(\left(\left(Z\left(W\right)-Y\left(W\right)\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(W\right)\right)\right)\right){+}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}},\left(Z\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)\right)$$
210	209	fveq1d	$$⊢\phi \to {\mathrm{eval}}_1\left(K\right)\left(\left(\left(Y\left(W\right)-Y\left(W\right)\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(W\right)\right)\right)\right){+}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}},\left(Y\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)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)={\mathrm{eval}}_1\left(K\right)\left(\left(\left(Z\left(W\right)-Y\left(W\right)\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(W\right)\right)\right)\right){+}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}},\left(Z\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)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)$$
211	204	nn0zd	$$⊢\phi \to Z\left(W\right)\in \mathbb{Z}$$
212	211 46	zsubcld	$$⊢\phi \to Z\left(W\right)-Y\left(W\right)\in \mathbb{Z}$$
213	205 50	resubcld	$$⊢\phi \to Z\left(W\right)-Y\left(W\right)\in ℝ$$
214	50 205	posdifd	$$⊢\phi \to \left(Y\left(W\right)<Z\left(W\right)\leftrightarrow 0<Z\left(W\right)-Y\left(W\right)\right)$$
215	13 214	mpbid	$$⊢\phi \to 0<Z\left(W\right)-Y\left(W\right)$$
216	48 213 215	ltled	$$⊢\phi \to 0\le Z\left(W\right)-Y\left(W\right)$$
217	212 216	jca	$$⊢\phi \to \left(Z\left(W\right)-Y\left(W\right)\in \mathbb{Z}\wedge 0\le Z\left(W\right)-Y\left(W\right)\right)$$
218		elnn0z	$$⊢Z\left(W\right)-Y\left(W\right)\in {\mathbb{N}}_0\leftrightarrow \left(Z\left(W\right)-Y\left(W\right)\in \mathbb{Z}\wedge 0\le Z\left(W\right)-Y\left(W\right)\right)$$
219	217 218	sylibr	$$⊢\phi \to Z\left(W\right)-Y\left(W\right)\in {\mathbb{N}}_0$$
220	14 15 16 17 20 31 64 7 85 219	evl1expd	$$⊢\phi \to \left(\left(Z\left(W\right)-Y\left(W\right)\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(W\right)\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}\wedge {\mathrm{eval}}_1\left(K\right)\left(\left(Z\left(W\right)-Y\left(W\right)\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(W\right)\right)\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)=\left(Z\left(W\right)-Y\left(W\right)\right){\cdot }_{{\mathrm{mulGrp}}_K}\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right){+}_K\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)\right)$$
221	220	simpld	$$⊢\phi \to \left(Z\left(W\right)-Y\left(W\right)\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(W\right)\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
222	220	simprd	$$⊢\phi \to {\mathrm{eval}}_1\left(K\right)\left(\left(Z\left(W\right)-Y\left(W\right)\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(W\right)\right)\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)=\left(Z\left(W\right)-Y\left(W\right)\right){\cdot }_{{\mathrm{mulGrp}}_K}\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right){+}_K\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)$$
223		rhmghm	$$⊢\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)\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{GrpHom}K\right)$$
224	24 223	syl	$$⊢\phi \to \mathrm{\mathbb{Z}RHom}\left(K\right)\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{GrpHom}K\right)$$
225	30 25	eleqtrdi	$$⊢\phi \to 0-W\in {\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
226	29 25	eleqtrdi	$$⊢\phi \to W\in {\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
227		eqid	$$⊢{\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}={\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
228		eqid	$$⊢{+}_{{\mathbb{Z}}_{\mathrm{ring}}}={+}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
229	227 228 63	ghmlin	$$⊢\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{GrpHom}K\right)\wedge 0-W\in {\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}\wedge W\in {\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}\right)\to \mathrm{\mathbb{Z}RHom}\left(K\right)\left(\left(0-W\right){+}_{{\mathbb{Z}}_{\mathrm{ring}}}W\right)=\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right){+}_K\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)$$
230	224 225 226 229	syl3anc	$$⊢\phi \to \mathrm{\mathbb{Z}RHom}\left(K\right)\left(\left(0-W\right){+}_{{\mathbb{Z}}_{\mathrm{ring}}}W\right)=\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right){+}_K\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)$$
231		zringplusg	$$⊢+={+}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
232	231	eqcomi	$$⊢{+}_{{\mathbb{Z}}_{\mathrm{ring}}}=+$$
233	232	a1i	$$⊢\phi \to {+}_{{\mathbb{Z}}_{\mathrm{ring}}}=+$$
234	233	oveqd	$$⊢\phi \to \left(0-W\right){+}_{{\mathbb{Z}}_{\mathrm{ring}}}W=0-W+W$$
235	234	fveq2d	$$⊢\phi \to \mathrm{\mathbb{Z}RHom}\left(K\right)\left(\left(0-W\right){+}_{{\mathbb{Z}}_{\mathrm{ring}}}W\right)=\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W+W\right)$$
236		0cnd	$$⊢\phi \to 0\in ℂ$$
237	29	zcnd	$$⊢\phi \to W\in ℂ$$
238	236 237	npcand	$$⊢\phi \to 0-W+W=0$$
239	238	fveq2d	$$⊢\phi \to \mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W+W\right)=\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0\right)$$
240	235 239	eqtrd	$$⊢\phi \to \mathrm{\mathbb{Z}RHom}\left(K\right)\left(\left(0-W\right){+}_{{\mathbb{Z}}_{\mathrm{ring}}}W\right)=\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0\right)$$
241	22 156	zrh0	$$⊢K\in \mathrm{Ring}\to \mathrm{\mathbb{Z}RHom}\left(K\right)\left(0\right)=0_K$$
242	21 241	syl	$$⊢\phi \to \mathrm{\mathbb{Z}RHom}\left(K\right)\left(0\right)=0_K$$
243	240 242	eqtrd	$$⊢\phi \to \mathrm{\mathbb{Z}RHom}\left(K\right)\left(\left(0-W\right){+}_{{\mathbb{Z}}_{\mathrm{ring}}}W\right)=0_K$$
244	230 243	eqtr3d	$$⊢\phi \to \mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right){+}_K\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)=0_K$$
245	244	oveq2d	$$⊢\phi \to \left(Z\left(W\right)-Y\left(W\right)\right){\cdot }_{{\mathrm{mulGrp}}_K}\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right){+}_K\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)=\left(Z\left(W\right)-Y\left(W\right)\right){\cdot }_{{\mathrm{mulGrp}}_K}{0}_K$$
246	219	nn0zd	$$⊢\phi \to Z\left(W\right)-Y\left(W\right)\in \mathbb{Z}$$
247	246 215	jca	$$⊢\phi \to \left(Z\left(W\right)-Y\left(W\right)\in \mathbb{Z}\wedge 0<Z\left(W\right)-Y\left(W\right)\right)$$
248		elnnz	$$⊢Z\left(W\right)-Y\left(W\right)\in \mathbb{N}\leftrightarrow \left(Z\left(W\right)-Y\left(W\right)\in \mathbb{Z}\wedge 0<Z\left(W\right)-Y\left(W\right)\right)$$
249	247 248	sylibr	$$⊢\phi \to Z\left(W\right)-Y\left(W\right)\in \mathbb{N}$$
250	21 249 85	ringexp0nn	$$⊢\phi \to \left(Z\left(W\right)-Y\left(W\right)\right){\cdot }_{{\mathrm{mulGrp}}_K}{0}_K=0_K$$
251	245 250	eqtrd	$$⊢\phi \to \left(Z\left(W\right)-Y\left(W\right)\right){\cdot }_{{\mathrm{mulGrp}}_K}\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right){+}_K\mathrm{\mathbb{Z}RHom}\left(K\right)\left(W\right)\right)=0_K$$
252	222 251	eqtrd	$$⊢\phi \to {\mathrm{eval}}_1\left(K\right)\left(\left(Z\left(W\right)-Y\left(W\right)\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(W\right)\right)\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)=0_K$$
253	221 252	jca	$$⊢\phi \to \left(\left(Z\left(W\right)-Y\left(W\right)\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(W\right)\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}\wedge {\mathrm{eval}}_1\left(K\right)\left(\left(Z\left(W\right)-Y\left(W\right)\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(W\right)\right)\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)=0_K\right)$$
254		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}$$
255	203	adantr	$$⊢\left(\phi \wedge i\in \left(\left(0\dots A\right)\setminus \left\{W\right\}\right)\right)\to Z:\left(0\dots A\right)⟶{\mathbb{N}}_0$$
256	255 113	ffvelcdmd	$$⊢\left(\phi \wedge i\in \left(\left(0\dots A\right)\setminus \left\{W\right\}\right)\right)\to Z\left(i\right)\in {\mathbb{N}}_0$$
257	254 7 110 256 168	mulgnn0cld	$$⊢\left(\phi \wedge i\in \left(\left(0\dots A\right)\setminus \left\{W\right\}\right)\right)\to Z\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)\in {\mathrm{Base}}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}$$
258	257 170	eleqtrd	$$⊢\left(\phi \wedge i\in \left(\left(0\dots A\right)\setminus \left\{W\right\}\right)\right)\to Z\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)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
259	258	ralrimiva	$$⊢\phi \to \forall i\in \left(\left(0\dots A\right)\setminus \left\{W\right\}\right)Z\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)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
260	33 37 109 259	gsummptcl	$$⊢\phi \to \underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}}\left(Z\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)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
261		eqidd	$$⊢\phi \to {\mathrm{eval}}_1\left(K\right)\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}}\left(Z\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)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)={\mathrm{eval}}_1\left(K\right)\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}}\left(Z\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)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)$$
262	260 261	jca	$$⊢\phi \to \left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}}\left(Z\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)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}\wedge {\mathrm{eval}}_1\left(K\right)\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}}\left(Z\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)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)={\mathrm{eval}}_1\left(K\right)\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}}\left(Z\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)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)\right)$$
263	14 15 16 17 20 31 253 262 140 141	evl1muld	$$⊢\phi \to \left(\left(\left(Z\left(W\right)-Y\left(W\right)\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(W\right)\right)\right)\right){+}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}},\left(Z\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)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}\wedge {\mathrm{eval}}_1\left(K\right)\left(\left(\left(Z\left(W\right)-Y\left(W\right)\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(W\right)\right)\right)\right){+}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}},\left(Z\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)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)=0_K{\cdot }_K{\mathrm{eval}}_1\left(K\right)\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}}\left(Z\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)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)\right)$$
264	263	simprd	$$⊢\phi \to {\mathrm{eval}}_1\left(K\right)\left(\left(\left(Z\left(W\right)-Y\left(W\right)\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(W\right)\right)\right)\right){+}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}},\left(Z\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)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)=0_K{\cdot }_K{\mathrm{eval}}_1\left(K\right)\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}}\left(Z\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)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)$$
265	14 15 16 17 20 31 260	fveval1fvcl	$$⊢\phi \to {\mathrm{eval}}_1\left(K\right)\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}}\left(Z\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)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)\in {\mathrm{Base}}_K$$
266	16 141 156 21 265	ringlzd	$$⊢\phi \to 0_K{\cdot }_K{\mathrm{eval}}_1\left(K\right)\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}}\left(Z\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)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)=0_K$$
267	264 266	eqtrd	$$⊢\phi \to {\mathrm{eval}}_1\left(K\right)\left(\left(\left(Z\left(W\right)-Y\left(W\right)\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(W\right)\right)\right)\right){+}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}},\left(Z\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)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)=0_K$$
268	210 267	eqtrd	$$⊢\phi \to {\mathrm{eval}}_1\left(K\right)\left(\left(\left(Y\left(W\right)-Y\left(W\right)\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(W\right)\right)\right)\right){+}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left(\underset{i\in \left(0\dots A\right)\setminus \left\{W\right\}}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}},\left(Y\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)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(0-W\right)\right)=0_K$$
269	195 268	neeqtrd	$$⊢\phi \to 0_K\ne 0_K$$