Theorem aks6d1c6lem1

Description: Lemma for claim 6, deduce exact degree of the polynomial. (Contributed by metakunt, 7-May-2025)

	Ref	Expression
Hypotheses	aks6d1c6.1	$$⊢\underset{\dot{}}{\sim }=\left\{⟨e,f⟩|\left(e\in \mathbb{N}\wedge f\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}\wedge \forall y\in \left({\mathrm{mulGrp}}_K\mathrm{PrimRoots}R\right)e{\cdot }_{{\mathrm{mulGrp}}_K}{\mathrm{eval}}_1\left(K\right)\left(f\right)\left(y\right)={\mathrm{eval}}_1\left(K\right)\left(f\right)\left(e{\cdot }_{{\mathrm{mulGrp}}_K}y\right)\right)\right\}$$
	aks6d1c6.2	$$⊢P=\mathrm{chr}\left(K\right)$$
	aks6d1c6.3	$$⊢\phi \to K\in \mathrm{Field}$$
	aks6d1c6.4	$$⊢\phi \to P\in \mathbb{P}$$
	aks6d1c6.5	$$⊢\phi \to R\in \mathbb{N}$$
	aks6d1c6.6	$$⊢\phi \to N\in \mathbb{N}$$
	aks6d1c6.7	$$⊢\phi \to P\parallel N$$
	aks6d1c6.8	$$⊢\phi \to N\gcd R=1$$
	aks6d1c6.9	$$⊢\phi \to A<P$$
	aks6d1c6.10	$$⊢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){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\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)$$
	aks6d1c6.11	$$⊢\phi \to A\in {\mathbb{N}}_0$$
	aks6d1c6.12	$$⊢E=\left(k\in {\mathbb{N}}_0,l\in {\mathbb{N}}_0⟼P^k{\left(\frac{N}{P}\right)}^l\right)$$
	aks6d1c6.13	$$⊢L=\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/R\mathbb{Z}\right)$$
	aks6d1c6.14	$$⊢\phi \to \forall a\in \left(1\dots A\right)N\underset{\dot{}}{\sim }\left({\mathrm{var}}_1\left(K\right){+}_{{\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(a\right)\right)\right)$$
	aks6d1c6.15	$$⊢\phi \to \left(x\in {\mathrm{Base}}_K⟼P{\cdot }_{{\mathrm{mulGrp}}_K}x\right)\in \left(K\mathrm{RingIso}K\right)$$
	aks6d1c6.16	$$⊢\phi \to M\in \left({\mathrm{mulGrp}}_K\mathrm{PrimRoots}R\right)$$
	aks6d1c6.17	$$⊢H=\left(h\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)⟼{\mathrm{eval}}_1\left(K\right)\left(G\left(h\right)\right)\left(M\right)\right)$$
	aks6d1c6.18	$$⊢D=\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|$$
	aks6d1c6.19	$$⊢S=\left\{s\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)|\sum _{t=0}^{A}s\left(t\right)\le D-1\right\}$$
	aks6d1c6lem1.1	$$⊢\phi \to U\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)$$
Assertion	aks6d1c6lem1	$$⊢\phi \to {\mathrm{deg}}_1\left(K\right)\left(G\left(U\right)\right)=\sum _{t=0}^{A}U\left(t\right)$$

Proof

Step	Hyp	Ref	Expression
1		aks6d1c6.1	$$⊢\underset{\dot{}}{\sim }=\left\{⟨e,f⟩|\left(e\in \mathbb{N}\wedge f\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}\wedge \forall y\in \left({\mathrm{mulGrp}}_K\mathrm{PrimRoots}R\right)e{\cdot }_{{\mathrm{mulGrp}}_K}{\mathrm{eval}}_1\left(K\right)\left(f\right)\left(y\right)={\mathrm{eval}}_1\left(K\right)\left(f\right)\left(e{\cdot }_{{\mathrm{mulGrp}}_K}y\right)\right)\right\}$$
2		aks6d1c6.2	$$⊢P=\mathrm{chr}\left(K\right)$$
3		aks6d1c6.3	$$⊢\phi \to K\in \mathrm{Field}$$
4		aks6d1c6.4	$$⊢\phi \to P\in \mathbb{P}$$
5		aks6d1c6.5	$$⊢\phi \to R\in \mathbb{N}$$
6		aks6d1c6.6	$$⊢\phi \to N\in \mathbb{N}$$
7		aks6d1c6.7	$$⊢\phi \to P\parallel N$$
8		aks6d1c6.8	$$⊢\phi \to N\gcd R=1$$
9		aks6d1c6.9	$$⊢\phi \to A<P$$
10		aks6d1c6.10	$$⊢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){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\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)$$
11		aks6d1c6.11	$$⊢\phi \to A\in {\mathbb{N}}_0$$
12		aks6d1c6.12	$$⊢E=\left(k\in {\mathbb{N}}_0,l\in {\mathbb{N}}_0⟼P^k{\left(\frac{N}{P}\right)}^l\right)$$
13		aks6d1c6.13	$$⊢L=\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/R\mathbb{Z}\right)$$
14		aks6d1c6.14	$$⊢\phi \to \forall a\in \left(1\dots A\right)N\underset{\dot{}}{\sim }\left({\mathrm{var}}_1\left(K\right){+}_{{\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(a\right)\right)\right)$$
15		aks6d1c6.15	$$⊢\phi \to \left(x\in {\mathrm{Base}}_K⟼P{\cdot }_{{\mathrm{mulGrp}}_K}x\right)\in \left(K\mathrm{RingIso}K\right)$$
16		aks6d1c6.16	$$⊢\phi \to M\in \left({\mathrm{mulGrp}}_K\mathrm{PrimRoots}R\right)$$
17		aks6d1c6.17	$$⊢H=\left(h\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)⟼{\mathrm{eval}}_1\left(K\right)\left(G\left(h\right)\right)\left(M\right)\right)$$
18		aks6d1c6.18	$$⊢D=\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|$$
19		aks6d1c6.19	$$⊢S=\left\{s\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)|\sum _{t=0}^{A}s\left(t\right)\le D-1\right\}$$
20		aks6d1c6lem1.1	$$⊢\phi \to U\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)$$
21	10	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){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\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)$$
22	21	fveq1d	$$⊢\phi \to G\left(U\right)=\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){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\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(U\right)$$
23	22	fveq2d	$$⊢\phi \to {\mathrm{deg}}_1\left(K\right)\left(G\left(U\right)\right)={\mathrm{deg}}_1\left(K\right)\left(\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){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\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(U\right)\right)$$
24		eqidd	$$⊢\phi \to \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){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\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(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){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\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)$$
25		simplr	$$⊢\left(\left(\phi \wedge g=U\right)\wedge i\in \left(0\dots A\right)\right)\to g=U$$
26	25	fveq1d	$$⊢\left(\left(\phi \wedge g=U\right)\wedge i\in \left(0\dots A\right)\right)\to g\left(i\right)=U\left(i\right)$$
27	26	oveq1d	$$⊢\left(\left(\phi \wedge g=U\right)\wedge i\in \left(0\dots A\right)\right)\to g\left(i\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\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)=U\left(i\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\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)$$
28	27	mpteq2dva	$$⊢\left(\phi \wedge g=U\right)\to \left(i\in \left(0\dots A\right)⟼g\left(i\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\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)⟼U\left(i\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\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)$$
29	28	oveq2d	$$⊢\left(\phi \wedge g=U\right)\to \underset{i=0}{\overset{A}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}}}\left(g\left(i\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\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 }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}}}\left(U\left(i\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\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)$$
30		ovexd	$$⊢\phi \to \underset{i=0}{\overset{A}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}}}\left(U\left(i\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\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{V}$$
31	24 29 20 30	fvmptd	$$⊢\phi \to \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){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\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(U\right)=\underset{i=0}{\overset{A}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}}}\left(U\left(i\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\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)$$
32	31	fveq2d	$$⊢\phi \to {\mathrm{deg}}_1\left(K\right)\left(\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){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\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(U\right)\right)={\mathrm{deg}}_1\left(K\right)\left(\underset{i=0}{\overset{A}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}}}\left(U\left(i\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\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)$$
33		fldidom	$$⊢K\in \mathrm{Field}\to K\in \mathrm{IDomn}$$
34	3 33	syl	$$⊢\phi \to K\in \mathrm{IDomn}$$
35		fzfid	$$⊢\phi \to \left(0\dots A\right)\in \mathrm{Fin}$$
36		eqid	$$⊢{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}={\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}$$
37		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
38	36 37	mgpbas	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}$$
39		eqid	$$⊢{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}={\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}$$
40	3	fldcrngd	$$⊢\phi \to K\in \mathrm{CRing}$$
41		crngring	$$⊢K\in \mathrm{CRing}\to K\in \mathrm{Ring}$$
42	40 41	syl	$$⊢\phi \to K\in \mathrm{Ring}$$
43		eqid	$$⊢{\mathrm{Poly}}_1\left(K\right)={\mathrm{Poly}}_1\left(K\right)$$
44	43	ply1ring	$$⊢K\in \mathrm{Ring}\to {\mathrm{Poly}}_1\left(K\right)\in \mathrm{Ring}$$
45	42 44	syl	$$⊢\phi \to {\mathrm{Poly}}_1\left(K\right)\in \mathrm{Ring}$$
46	36	ringmgp	$$⊢{\mathrm{Poly}}_1\left(K\right)\in \mathrm{Ring}\to {\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}\in \mathrm{Mnd}$$
47	45 46	syl	$$⊢\phi \to {\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}\in \mathrm{Mnd}$$
48	47	adantr	$$⊢\left(\phi \wedge i\in \left(0\dots A\right)\right)\to {\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}\in \mathrm{Mnd}$$
49		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
50	49	a1i	$$⊢\phi \to {\mathbb{N}}_0\in \mathrm{V}$$
51		ovexd	$$⊢\phi \to \left(0\dots A\right)\in \mathrm{V}$$
52	50 51	elmapd	$$⊢\phi \to \left(U\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)\leftrightarrow U:\left(0\dots A\right)⟶{\mathbb{N}}_0\right)$$
53	20 52	mpbid	$$⊢\phi \to U:\left(0\dots A\right)⟶{\mathbb{N}}_0$$
54	53	adantr	$$⊢\left(\phi \wedge i\in \left(0\dots A\right)\right)\to U:\left(0\dots A\right)⟶{\mathbb{N}}_0$$
55		simpr	$$⊢\left(\phi \wedge i\in \left(0\dots A\right)\right)\to i\in \left(0\dots A\right)$$
56	54 55	ffvelcdmd	$$⊢\left(\phi \wedge i\in \left(0\dots A\right)\right)\to U\left(i\right)\in {\mathbb{N}}_0$$
57		2fveq3	$$⊢t=i\to \mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(t\right)\right)=\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)$$
58	57	oveq2d	$$⊢t=i\to {\mathrm{var}}_1\left(K\right){+}_{{\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(t\right)\right)={\mathrm{var}}_1\left(K\right){+}_{{\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)$$
59	58	eleq1d	$$⊢t=i\to \left({\mathrm{var}}_1\left(K\right){+}_{{\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(t\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}\leftrightarrow {\mathrm{var}}_1\left(K\right){+}_{{\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)}\right)$$
60		ringmnd	$$⊢{\mathrm{Poly}}_1\left(K\right)\in \mathrm{Ring}\to {\mathrm{Poly}}_1\left(K\right)\in \mathrm{Mnd}$$
61	45 60	syl	$$⊢\phi \to {\mathrm{Poly}}_1\left(K\right)\in \mathrm{Mnd}$$
62	61	adantr	$$⊢\left(\phi \wedge t\in \left(0\dots A\right)\right)\to {\mathrm{Poly}}_1\left(K\right)\in \mathrm{Mnd}$$
63	42	adantr	$$⊢\left(\phi \wedge t\in \left(0\dots A\right)\right)\to K\in \mathrm{Ring}$$
64		eqid	$$⊢{\mathrm{var}}_1\left(K\right)={\mathrm{var}}_1\left(K\right)$$
65	64 43 37	vr1cl	$$⊢K\in \mathrm{Ring}\to {\mathrm{var}}_1\left(K\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
66	63 65	syl	$$⊢\left(\phi \wedge t\in \left(0\dots A\right)\right)\to {\mathrm{var}}_1\left(K\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
67		eqid	$$⊢\mathrm{\mathbb{Z}RHom}\left(K\right)=\mathrm{\mathbb{Z}RHom}\left(K\right)$$
68	67	zrhrhm	$$⊢K\in \mathrm{Ring}\to \mathrm{\mathbb{Z}RHom}\left(K\right)\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}K\right)$$
69	42 68	syl	$$⊢\phi \to \mathrm{\mathbb{Z}RHom}\left(K\right)\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}K\right)$$
70		zringbas	$$⊢\mathbb{Z}={\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
71		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
72	70 71	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$$
73	69 72	syl	$$⊢\phi \to \mathrm{\mathbb{Z}RHom}\left(K\right):\mathbb{Z}⟶{\mathrm{Base}}_K$$
74	73	adantr	$$⊢\left(\phi \wedge t\in \left(0\dots A\right)\right)\to \mathrm{\mathbb{Z}RHom}\left(K\right):\mathbb{Z}⟶{\mathrm{Base}}_K$$
75		elfzelz	$$⊢t\in \left(0\dots A\right)\to t\in \mathbb{Z}$$
76	75	adantl	$$⊢\left(\phi \wedge t\in \left(0\dots A\right)\right)\to t\in \mathbb{Z}$$
77	74 76	ffvelcdmd	$$⊢\left(\phi \wedge t\in \left(0\dots A\right)\right)\to \mathrm{\mathbb{Z}RHom}\left(K\right)\left(t\right)\in {\mathrm{Base}}_K$$
78		eqid	$$⊢\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)=\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)$$
79	43 78 71 37	ply1sclcl	$$⊢\left(K\in \mathrm{Ring}\wedge \mathrm{\mathbb{Z}RHom}\left(K\right)\left(t\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(t\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
80	63 77 79	syl2anc	$$⊢\left(\phi \wedge t\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(t\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
81		eqid	$$⊢{+}_{{\mathrm{Poly}}_1\left(K\right)}={+}_{{\mathrm{Poly}}_1\left(K\right)}$$
82	37 81	mndcl	$$⊢\left({\mathrm{Poly}}_1\left(K\right)\in \mathrm{Mnd}\wedge {\mathrm{var}}_1\left(K\right)\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(t\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}\right)\to {\mathrm{var}}_1\left(K\right){+}_{{\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(t\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
83	62 66 80 82	syl3anc	$$⊢\left(\phi \wedge t\in \left(0\dots A\right)\right)\to {\mathrm{var}}_1\left(K\right){+}_{{\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(t\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
84	83	ralrimiva	$$⊢\phi \to \forall t\in \left(0\dots A\right){\mathrm{var}}_1\left(K\right){+}_{{\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(t\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
85	84	adantr	$$⊢\left(\phi \wedge i\in \left(0\dots A\right)\right)\to \forall t\in \left(0\dots A\right){\mathrm{var}}_1\left(K\right){+}_{{\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(t\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
86	59 85 55	rspcdva	$$⊢\left(\phi \wedge i\in \left(0\dots A\right)\right)\to {\mathrm{var}}_1\left(K\right){+}_{{\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)}$$
87	38 39 48 56 86	mulgnn0cld	$$⊢\left(\phi \wedge i\in \left(0\dots A\right)\right)\to U\left(i\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\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)}$$
88	43	ply1idom	$$⊢K\in \mathrm{IDomn}\to {\mathrm{Poly}}_1\left(K\right)\in \mathrm{IDomn}$$
89	34 88	syl	$$⊢\phi \to {\mathrm{Poly}}_1\left(K\right)\in \mathrm{IDomn}$$
90	89	adantr	$$⊢\left(\phi \wedge i\in \left(0\dots A\right)\right)\to {\mathrm{Poly}}_1\left(K\right)\in \mathrm{IDomn}$$
91	58	neeq1d	$$⊢t=i\to \left({\mathrm{var}}_1\left(K\right){+}_{{\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(t\right)\right)\ne 0_{{\mathrm{Poly}}_1\left(K\right)}\leftrightarrow {\mathrm{var}}_1\left(K\right){+}_{{\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)\ne 0_{{\mathrm{Poly}}_1\left(K\right)}\right)$$
92		eqid	$$⊢{\mathrm{deg}}_1\left(K\right)={\mathrm{deg}}_1\left(K\right)$$
93	92 43 37	deg1xrcl	$$⊢\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(t\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}\to {\mathrm{deg}}_1\left(K\right)\left(\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(t\right)\right)\right)\in {ℝ}^{*}$$
94	80 93	syl	$$⊢\left(\phi \wedge t\in \left(0\dots A\right)\right)\to {\mathrm{deg}}_1\left(K\right)\left(\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(t\right)\right)\right)\in {ℝ}^{*}$$
95		0xr	$$⊢0\in {ℝ}^{*}$$
96	95	a1i	$$⊢\left(\phi \wedge t\in \left(0\dots A\right)\right)\to 0\in {ℝ}^{*}$$
97		1xr	$$⊢1\in {ℝ}^{*}$$
98	97	a1i	$$⊢\left(\phi \wedge t\in \left(0\dots A\right)\right)\to 1\in {ℝ}^{*}$$
99	92 43 71 78	deg1sclle	$$⊢\left(K\in \mathrm{Ring}\wedge \mathrm{\mathbb{Z}RHom}\left(K\right)\left(t\right)\in {\mathrm{Base}}_K\right)\to {\mathrm{deg}}_1\left(K\right)\left(\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(t\right)\right)\right)\le 0$$
100	63 77 99	syl2anc	$$⊢\left(\phi \wedge t\in \left(0\dots A\right)\right)\to {\mathrm{deg}}_1\left(K\right)\left(\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(t\right)\right)\right)\le 0$$
101		0lt1	$$⊢0<1$$
102	101	a1i	$$⊢\left(\phi \wedge t\in \left(0\dots A\right)\right)\to 0<1$$
103	94 96 98 100 102	xrlelttrd	$$⊢\left(\phi \wedge t\in \left(0\dots A\right)\right)\to {\mathrm{deg}}_1\left(K\right)\left(\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(t\right)\right)\right)<1$$
104	38 39	mulg1	$$⊢{\mathrm{var}}_1\left(K\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}\to 1{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}{\mathrm{var}}_1\left(K\right)={\mathrm{var}}_1\left(K\right)$$
105	66 104	syl	$$⊢\left(\phi \wedge t\in \left(0\dots A\right)\right)\to 1{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}{\mathrm{var}}_1\left(K\right)={\mathrm{var}}_1\left(K\right)$$
106	105	eqcomd	$$⊢\left(\phi \wedge t\in \left(0\dots A\right)\right)\to {\mathrm{var}}_1\left(K\right)=1{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}{\mathrm{var}}_1\left(K\right)$$
107	106	fveq2d	$$⊢\left(\phi \wedge t\in \left(0\dots A\right)\right)\to {\mathrm{deg}}_1\left(K\right)\left({\mathrm{var}}_1\left(K\right)\right)={\mathrm{deg}}_1\left(K\right)\left(1{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}{\mathrm{var}}_1\left(K\right)\right)$$
108		isfld	$$⊢K\in \mathrm{Field}\leftrightarrow \left(K\in \mathrm{DivRing}\wedge K\in \mathrm{CRing}\right)$$
109		drngnzr	$$⊢K\in \mathrm{DivRing}\to K\in \mathrm{NzRing}$$
110	109	adantr	$$⊢\left(K\in \mathrm{DivRing}\wedge K\in \mathrm{CRing}\right)\to K\in \mathrm{NzRing}$$
111	108 110	sylbi	$$⊢K\in \mathrm{Field}\to K\in \mathrm{NzRing}$$
112	3 111	syl	$$⊢\phi \to K\in \mathrm{NzRing}$$
113	112	adantr	$$⊢\left(\phi \wedge t\in \left(0\dots A\right)\right)\to K\in \mathrm{NzRing}$$
114		1nn0	$$⊢1\in {\mathbb{N}}_0$$
115	114	a1i	$$⊢\left(\phi \wedge t\in \left(0\dots A\right)\right)\to 1\in {\mathbb{N}}_0$$
116	92 43 64 36 39	deg1pw	$$⊢\left(K\in \mathrm{NzRing}\wedge 1\in {\mathbb{N}}_0\right)\to {\mathrm{deg}}_1\left(K\right)\left(1{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}{\mathrm{var}}_1\left(K\right)\right)=1$$
117	113 115 116	syl2anc	$$⊢\left(\phi \wedge t\in \left(0\dots A\right)\right)\to {\mathrm{deg}}_1\left(K\right)\left(1{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}{\mathrm{var}}_1\left(K\right)\right)=1$$
118	107 117	eqtr2d	$$⊢\left(\phi \wedge t\in \left(0\dots A\right)\right)\to 1={\mathrm{deg}}_1\left(K\right)\left({\mathrm{var}}_1\left(K\right)\right)$$
119	103 118	breqtrd	$$⊢\left(\phi \wedge t\in \left(0\dots A\right)\right)\to {\mathrm{deg}}_1\left(K\right)\left(\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(t\right)\right)\right)<{\mathrm{deg}}_1\left(K\right)\left({\mathrm{var}}_1\left(K\right)\right)$$
120	43 92 63 37 81 66 80 119	deg1add	$$⊢\left(\phi \wedge t\in \left(0\dots A\right)\right)\to {\mathrm{deg}}_1\left(K\right)\left({\mathrm{var}}_1\left(K\right){+}_{{\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(t\right)\right)\right)={\mathrm{deg}}_1\left(K\right)\left({\mathrm{var}}_1\left(K\right)\right)$$
121	107 117	eqtrd	$$⊢\left(\phi \wedge t\in \left(0\dots A\right)\right)\to {\mathrm{deg}}_1\left(K\right)\left({\mathrm{var}}_1\left(K\right)\right)=1$$
122	120 121	eqtrd	$$⊢\left(\phi \wedge t\in \left(0\dots A\right)\right)\to {\mathrm{deg}}_1\left(K\right)\left({\mathrm{var}}_1\left(K\right){+}_{{\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(t\right)\right)\right)=1$$
123	122 115	eqeltrd	$$⊢\left(\phi \wedge t\in \left(0\dots A\right)\right)\to {\mathrm{deg}}_1\left(K\right)\left({\mathrm{var}}_1\left(K\right){+}_{{\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(t\right)\right)\right)\in {\mathbb{N}}_0$$
124		eqid	$$⊢0_{{\mathrm{Poly}}_1\left(K\right)}=0_{{\mathrm{Poly}}_1\left(K\right)}$$
125	92 43 124 37	deg1nn0clb	$$⊢\left(K\in \mathrm{Ring}\wedge {\mathrm{var}}_1\left(K\right){+}_{{\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(t\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}\right)\to \left({\mathrm{var}}_1\left(K\right){+}_{{\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(t\right)\right)\ne 0_{{\mathrm{Poly}}_1\left(K\right)}\leftrightarrow {\mathrm{deg}}_1\left(K\right)\left({\mathrm{var}}_1\left(K\right){+}_{{\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(t\right)\right)\right)\in {\mathbb{N}}_0\right)$$
126	63 83 125	syl2anc	$$⊢\left(\phi \wedge t\in \left(0\dots A\right)\right)\to \left({\mathrm{var}}_1\left(K\right){+}_{{\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(t\right)\right)\ne 0_{{\mathrm{Poly}}_1\left(K\right)}\leftrightarrow {\mathrm{deg}}_1\left(K\right)\left({\mathrm{var}}_1\left(K\right){+}_{{\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(t\right)\right)\right)\in {\mathbb{N}}_0\right)$$
127	123 126	mpbird	$$⊢\left(\phi \wedge t\in \left(0\dots A\right)\right)\to {\mathrm{var}}_1\left(K\right){+}_{{\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(t\right)\right)\ne 0_{{\mathrm{Poly}}_1\left(K\right)}$$
128	127	ralrimiva	$$⊢\phi \to \forall t\in \left(0\dots A\right){\mathrm{var}}_1\left(K\right){+}_{{\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(t\right)\right)\ne 0_{{\mathrm{Poly}}_1\left(K\right)}$$
129	128	adantr	$$⊢\left(\phi \wedge i\in \left(0\dots A\right)\right)\to \forall t\in \left(0\dots A\right){\mathrm{var}}_1\left(K\right){+}_{{\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(t\right)\right)\ne 0_{{\mathrm{Poly}}_1\left(K\right)}$$
130	91 129 55	rspcdva	$$⊢\left(\phi \wedge i\in \left(0\dots A\right)\right)\to {\mathrm{var}}_1\left(K\right){+}_{{\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)\ne 0_{{\mathrm{Poly}}_1\left(K\right)}$$
131	90 86 130 56 39	idomnnzpownz	$$⊢\left(\phi \wedge i\in \left(0\dots A\right)\right)\to U\left(i\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\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)\ne 0_{{\mathrm{Poly}}_1\left(K\right)}$$
132	87 131	jca	$$⊢\left(\phi \wedge i\in \left(0\dots A\right)\right)\to \left(U\left(i\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\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 U\left(i\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\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)\ne 0_{{\mathrm{Poly}}_1\left(K\right)}\right)$$
133	132	ralrimiva	$$⊢\phi \to \forall i\in \left(0\dots A\right)\left(U\left(i\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\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 U\left(i\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\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)\ne 0_{{\mathrm{Poly}}_1\left(K\right)}\right)$$
134	34 35 133	deg1gprod	$$⊢\phi \to \left({\mathrm{deg}}_1\left(K\right)\left(\underset{i=0}{\overset{A}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}}}\left(U\left(i\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\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)=\sum _{t=0}^A{\mathrm{deg}}_1\left(K\right)\left(\left(i\in \left(0\dots A\right)⟼U\left(i\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\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(t\right)\right)\wedge 0\le {\mathrm{deg}}_1\left(K\right)\left(\underset{i=0}{\overset{A}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}}}\left(U\left(i\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\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)$$
135	134	simpld	$$⊢\phi \to {\mathrm{deg}}_1\left(K\right)\left(\underset{i=0}{\overset{A}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}}}\left(U\left(i\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\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)=\sum _{t=0}^A{\mathrm{deg}}_1\left(K\right)\left(\left(i\in \left(0\dots A\right)⟼U\left(i\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\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(t\right)\right)$$
136		eqidd	$$⊢\left(\phi \wedge t\in \left(0\dots A\right)\right)\to \left(i\in \left(0\dots A\right)⟼U\left(i\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\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)⟼U\left(i\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\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)$$
137		simpr	$$⊢\left(\left(\phi \wedge t\in \left(0\dots A\right)\right)\wedge i=t\right)\to i=t$$
138	137	fveq2d	$$⊢\left(\left(\phi \wedge t\in \left(0\dots A\right)\right)\wedge i=t\right)\to U\left(i\right)=U\left(t\right)$$
139	137	fveq2d	$$⊢\left(\left(\phi \wedge t\in \left(0\dots A\right)\right)\wedge i=t\right)\to \mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)=\mathrm{\mathbb{Z}RHom}\left(K\right)\left(t\right)$$
140	139	fveq2d	$$⊢\left(\left(\phi \wedge t\in \left(0\dots A\right)\right)\wedge i=t\right)\to \mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)=\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(t\right)\right)$$
141	140	oveq2d	$$⊢\left(\left(\phi \wedge t\in \left(0\dots A\right)\right)\wedge i=t\right)\to {\mathrm{var}}_1\left(K\right){+}_{{\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)={\mathrm{var}}_1\left(K\right){+}_{{\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(t\right)\right)$$
142	138 141	oveq12d	$$⊢\left(\left(\phi \wedge t\in \left(0\dots A\right)\right)\wedge i=t\right)\to U\left(i\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\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)=U\left(t\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\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(t\right)\right)\right)$$
143		simpr	$$⊢\left(\phi \wedge t\in \left(0\dots A\right)\right)\to t\in \left(0\dots A\right)$$
144		ovexd	$$⊢\left(\phi \wedge t\in \left(0\dots A\right)\right)\to U\left(t\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\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(t\right)\right)\right)\in \mathrm{V}$$
145	136 142 143 144	fvmptd	$$⊢\left(\phi \wedge t\in \left(0\dots A\right)\right)\to \left(i\in \left(0\dots A\right)⟼U\left(i\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\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(t\right)=U\left(t\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\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(t\right)\right)\right)$$
146	145	fveq2d	$$⊢\left(\phi \wedge t\in \left(0\dots A\right)\right)\to {\mathrm{deg}}_1\left(K\right)\left(\left(i\in \left(0\dots A\right)⟼U\left(i\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\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(t\right)\right)={\mathrm{deg}}_1\left(K\right)\left(U\left(t\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\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(t\right)\right)\right)\right)$$
147	34	adantr	$$⊢\left(\phi \wedge t\in \left(0\dots A\right)\right)\to K\in \mathrm{IDomn}$$
148	53	ffvelcdmda	$$⊢\left(\phi \wedge t\in \left(0\dots A\right)\right)\to U\left(t\right)\in {\mathbb{N}}_0$$
149	147 83 127 148 39 92	deg1pow	$$⊢\left(\phi \wedge t\in \left(0\dots A\right)\right)\to {\mathrm{deg}}_1\left(K\right)\left(U\left(t\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\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(t\right)\right)\right)\right)=U\left(t\right){\mathrm{deg}}_1\left(K\right)\left({\mathrm{var}}_1\left(K\right){+}_{{\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(t\right)\right)\right)$$
150	122	oveq2d	$$⊢\left(\phi \wedge t\in \left(0\dots A\right)\right)\to U\left(t\right){\mathrm{deg}}_1\left(K\right)\left({\mathrm{var}}_1\left(K\right){+}_{{\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(t\right)\right)\right)=U\left(t\right)\cdot 1$$
151	148	nn0cnd	$$⊢\left(\phi \wedge t\in \left(0\dots A\right)\right)\to U\left(t\right)\in ℂ$$
152	151	mulridd	$$⊢\left(\phi \wedge t\in \left(0\dots A\right)\right)\to U\left(t\right)\cdot 1=U\left(t\right)$$
153	150 152	eqtrd	$$⊢\left(\phi \wedge t\in \left(0\dots A\right)\right)\to U\left(t\right){\mathrm{deg}}_1\left(K\right)\left({\mathrm{var}}_1\left(K\right){+}_{{\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(t\right)\right)\right)=U\left(t\right)$$
154	149 153	eqtrd	$$⊢\left(\phi \wedge t\in \left(0\dots A\right)\right)\to {\mathrm{deg}}_1\left(K\right)\left(U\left(t\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\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(t\right)\right)\right)\right)=U\left(t\right)$$
155	146 154	eqtrd	$$⊢\left(\phi \wedge t\in \left(0\dots A\right)\right)\to {\mathrm{deg}}_1\left(K\right)\left(\left(i\in \left(0\dots A\right)⟼U\left(i\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\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(t\right)\right)=U\left(t\right)$$
156	155	sumeq2dv	$$⊢\phi \to \sum _{t=0}^A{\mathrm{deg}}_1\left(K\right)\left(\left(i\in \left(0\dots A\right)⟼U\left(i\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\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(t\right)\right)=\sum _{t=0}^{A}U\left(t\right)$$
157	135 156	eqtrd	$$⊢\phi \to {\mathrm{deg}}_1\left(K\right)\left(\underset{i=0}{\overset{A}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}}}\left(U\left(i\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\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)=\sum _{t=0}^{A}U\left(t\right)$$
158	32 157	eqtrd	$$⊢\phi \to {\mathrm{deg}}_1\left(K\right)\left(\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){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\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(U\right)\right)=\sum _{t=0}^{A}U\left(t\right)$$
159	23 158	eqtrd	$$⊢\phi \to {\mathrm{deg}}_1\left(K\right)\left(G\left(U\right)\right)=\sum _{t=0}^{A}U\left(t\right)$$