Theorem vietadeg1

Description: The degree of a product of H of linear polynomials of the form X - Z is H . (Contributed by Thierry Arnoux, 15-Feb-2026)

	Ref	Expression
Hypotheses	vieta.w	$$⊢W={\mathrm{Poly}}_1\left(R\right)$$
	vieta.b	$$⊢B={\mathrm{Base}}_R$$
	vieta.3	$$⊢\underset{\dot{}}{-}={-}_W$$
	vieta.m	$$⊢M={\mathrm{mulGrp}}_W$$
	vieta.q	$$⊢Q=I\mathrm{eval}R$$
	vieta.e	No typesetting found for |- E = ( I eSymPoly R ) with typecode |-
	vieta.n	$$⊢N={inv}_g\left(R\right)$$
	vieta.1	$$⊢\underset{\dot{}}{1}=1_R$$
	vieta.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	vieta.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
	vieta.a	$$⊢A=\mathrm{algSc}\left(W\right)$$
	vieta.p	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_R}$$
	vieta.h	$$⊢H=\left|I\right|$$
	vieta.i	$$⊢\phi \to I\in \mathrm{Fin}$$
	vieta.r	$$⊢\phi \to R\in \mathrm{IDomn}$$
	vieta.z	$$⊢\phi \to Z:I⟶B$$
	vieta.f	$$⊢F=\underset{n\in I}{{\sum }_M}\left(X\underset{\dot{}}{-}A\left(Z\left(n\right)\right)\right)$$
	vietadeg1.1	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
Assertion	vietadeg1	$$⊢\phi \to D\left(F\right)=H$$

Proof

Step	Hyp	Ref	Expression
1		vieta.w	$$⊢W={\mathrm{Poly}}_1\left(R\right)$$
2		vieta.b	$$⊢B={\mathrm{Base}}_R$$
3		vieta.3	$$⊢\underset{\dot{}}{-}={-}_W$$
4		vieta.m	$$⊢M={\mathrm{mulGrp}}_W$$
5		vieta.q	$$⊢Q=I\mathrm{eval}R$$
6		vieta.e	Could not format E = ( I eSymPoly R ) : No typesetting found for |- E = ( I eSymPoly R ) with typecode |-
7		vieta.n	$$⊢N={inv}_g\left(R\right)$$
8		vieta.1	$$⊢\underset{\dot{}}{1}=1_R$$
9		vieta.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
10		vieta.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
11		vieta.a	$$⊢A=\mathrm{algSc}\left(W\right)$$
12		vieta.p	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_R}$$
13		vieta.h	$$⊢H=\left|I\right|$$
14		vieta.i	$$⊢\phi \to I\in \mathrm{Fin}$$
15		vieta.r	$$⊢\phi \to R\in \mathrm{IDomn}$$
16		vieta.z	$$⊢\phi \to Z:I⟶B$$
17		vieta.f	$$⊢F=\underset{n\in I}{{\sum }_M}\left(X\underset{\dot{}}{-}A\left(Z\left(n\right)\right)\right)$$
18		vietadeg1.1	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
19	17	fveq2i	$$⊢D\left(F\right)=D\left(\underset{n\in I}{{\sum }_M}\left(X\underset{\dot{}}{-}A\left(Z\left(n\right)\right)\right)\right)$$
20		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
21		eqid	$$⊢0_W=0_W$$
22	15	idomringd	$$⊢\phi \to R\in \mathrm{Ring}$$
23	1	ply1ring	$$⊢R\in \mathrm{Ring}\to W\in \mathrm{Ring}$$
24		ringgrp	$$⊢W\in \mathrm{Ring}\to W\in \mathrm{Grp}$$
25	22 23 24	3syl	$$⊢\phi \to W\in \mathrm{Grp}$$
26	25	adantr	$$⊢\left(\phi \wedge n\in I\right)\to W\in \mathrm{Grp}$$
27	10 1 20	vr1cl	$$⊢R\in \mathrm{Ring}\to X\in {\mathrm{Base}}_W$$
28	22 27	syl	$$⊢\phi \to X\in {\mathrm{Base}}_W$$
29	28	adantr	$$⊢\left(\phi \wedge n\in I\right)\to X\in {\mathrm{Base}}_W$$
30		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
31		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
32	15	idomcringd	$$⊢\phi \to R\in \mathrm{CRing}$$
33	1	ply1assa	$$⊢R\in \mathrm{CRing}\to W\in \mathrm{AssAlg}$$
34	32 33	syl	$$⊢\phi \to W\in \mathrm{AssAlg}$$
35	34	adantr	$$⊢\left(\phi \wedge n\in I\right)\to W\in \mathrm{AssAlg}$$
36	16	ffvelcdmda	$$⊢\left(\phi \wedge n\in I\right)\to Z\left(n\right)\in B$$
37	1	ply1sca	$$⊢R\in \mathrm{IDomn}\to R=\mathrm{Scalar}\left(W\right)$$
38	15 37	syl	$$⊢\phi \to R=\mathrm{Scalar}\left(W\right)$$
39	38	fveq2d	$$⊢\phi \to {\mathrm{Base}}_R={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
40	2 39	eqtrid	$$⊢\phi \to B={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
41	40	adantr	$$⊢\left(\phi \wedge n\in I\right)\to B={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
42	36 41	eleqtrd	$$⊢\left(\phi \wedge n\in I\right)\to Z\left(n\right)\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
43	11 30 31 35 42	asclelbas	$$⊢\left(\phi \wedge n\in I\right)\to A\left(Z\left(n\right)\right)\in {\mathrm{Base}}_W$$
44	20 3 26 29 43	grpsubcld	$$⊢\left(\phi \wedge n\in I\right)\to X\underset{\dot{}}{-}A\left(Z\left(n\right)\right)\in {\mathrm{Base}}_W$$
45	15	idomdomd	$$⊢\phi \to R\in \mathrm{Domn}$$
46		domnnzr	$$⊢R\in \mathrm{Domn}\to R\in \mathrm{NzRing}$$
47	45 46	syl	$$⊢\phi \to R\in \mathrm{NzRing}$$
48	18 1 10 47	deg1vr	$$⊢\phi \to D\left(X\right)=1$$
49	48	ad2antrr	$$⊢\left(\left(\phi \wedge n\in I\right)\wedge X\underset{\dot{}}{-}A\left(Z\left(n\right)\right)=0_W\right)\to D\left(X\right)=1$$
50	18 1 20	deg1cl	$$⊢X\in {\mathrm{Base}}_W\to D\left(X\right)\in \left({\mathbb{N}}_0\cup \left\{\mathrm{-\infty }\right\}\right)$$
51	28 50	syl	$$⊢\phi \to D\left(X\right)\in \left({\mathbb{N}}_0\cup \left\{\mathrm{-\infty }\right\}\right)$$
52	51	nn0mnfxrd	$$⊢\phi \to D\left(X\right)\in {ℝ}^{*}$$
53	52	ad2antrr	$$⊢\left(\left(\phi \wedge n\in I\right)\wedge X\underset{\dot{}}{-}A\left(Z\left(n\right)\right)=0_W\right)\to D\left(X\right)\in {ℝ}^{*}$$
54	49 53	eqeltrrd	$$⊢\left(\left(\phi \wedge n\in I\right)\wedge X\underset{\dot{}}{-}A\left(Z\left(n\right)\right)=0_W\right)\to 1\in {ℝ}^{*}$$
55	51	ad2antrr	$$⊢\left(\left(\phi \wedge n\in I\right)\wedge X\underset{\dot{}}{-}A\left(Z\left(n\right)\right)=0_W\right)\to D\left(X\right)\in \left({\mathbb{N}}_0\cup \left\{\mathrm{-\infty }\right\}\right)$$
56		0zd	$$⊢\left(\left(\phi \wedge n\in I\right)\wedge X\underset{\dot{}}{-}A\left(Z\left(n\right)\right)=0_W\right)\to 0\in \mathbb{Z}$$
57	26	adantr	$$⊢\left(\left(\phi \wedge n\in I\right)\wedge X\underset{\dot{}}{-}A\left(Z\left(n\right)\right)=0_W\right)\to W\in \mathrm{Grp}$$
58	29	adantr	$$⊢\left(\left(\phi \wedge n\in I\right)\wedge X\underset{\dot{}}{-}A\left(Z\left(n\right)\right)=0_W\right)\to X\in {\mathrm{Base}}_W$$
59	43	adantr	$$⊢\left(\left(\phi \wedge n\in I\right)\wedge X\underset{\dot{}}{-}A\left(Z\left(n\right)\right)=0_W\right)\to A\left(Z\left(n\right)\right)\in {\mathrm{Base}}_W$$
60		simpr	$$⊢\left(\left(\phi \wedge n\in I\right)\wedge X\underset{\dot{}}{-}A\left(Z\left(n\right)\right)=0_W\right)\to X\underset{\dot{}}{-}A\left(Z\left(n\right)\right)=0_W$$
61	20 21 3	grpsubeq0	$$⊢\left(W\in \mathrm{Grp}\wedge X\in {\mathrm{Base}}_W\wedge A\left(Z\left(n\right)\right)\in {\mathrm{Base}}_W\right)\to \left(X\underset{\dot{}}{-}A\left(Z\left(n\right)\right)=0_W\leftrightarrow X=A\left(Z\left(n\right)\right)\right)$$
62	61	biimpa	$$⊢\left(\left(W\in \mathrm{Grp}\wedge X\in {\mathrm{Base}}_W\wedge A\left(Z\left(n\right)\right)\in {\mathrm{Base}}_W\right)\wedge X\underset{\dot{}}{-}A\left(Z\left(n\right)\right)=0_W\right)\to X=A\left(Z\left(n\right)\right)$$
63	57 58 59 60 62	syl31anc	$$⊢\left(\left(\phi \wedge n\in I\right)\wedge X\underset{\dot{}}{-}A\left(Z\left(n\right)\right)=0_W\right)\to X=A\left(Z\left(n\right)\right)$$
64	63	fveq2d	$$⊢\left(\left(\phi \wedge n\in I\right)\wedge X\underset{\dot{}}{-}A\left(Z\left(n\right)\right)=0_W\right)\to D\left(X\right)=D\left(A\left(Z\left(n\right)\right)\right)$$
65	22	adantr	$$⊢\left(\phi \wedge n\in I\right)\to R\in \mathrm{Ring}$$
66	18 1 2 11	deg1sclle	$$⊢\left(R\in \mathrm{Ring}\wedge Z\left(n\right)\in B\right)\to D\left(A\left(Z\left(n\right)\right)\right)\le 0$$
67	65 36 66	syl2anc	$$⊢\left(\phi \wedge n\in I\right)\to D\left(A\left(Z\left(n\right)\right)\right)\le 0$$
68	67	adantr	$$⊢\left(\left(\phi \wedge n\in I\right)\wedge X\underset{\dot{}}{-}A\left(Z\left(n\right)\right)=0_W\right)\to D\left(A\left(Z\left(n\right)\right)\right)\le 0$$
69	64 68	eqbrtrd	$$⊢\left(\left(\phi \wedge n\in I\right)\wedge X\underset{\dot{}}{-}A\left(Z\left(n\right)\right)=0_W\right)\to D\left(X\right)\le 0$$
70		degltp1le	$$⊢\left(D\left(X\right)\in \left({\mathbb{N}}_0\cup \left\{\mathrm{-\infty }\right\}\right)\wedge 0\in \mathbb{Z}\right)\to \left(D\left(X\right)<0+1\leftrightarrow D\left(X\right)\le 0\right)$$
71	70	biimpar	$$⊢\left(\left(D\left(X\right)\in \left({\mathbb{N}}_0\cup \left\{\mathrm{-\infty }\right\}\right)\wedge 0\in \mathbb{Z}\right)\wedge D\left(X\right)\le 0\right)\to D\left(X\right)<0+1$$
72	55 56 69 71	syl21anc	$$⊢\left(\left(\phi \wedge n\in I\right)\wedge X\underset{\dot{}}{-}A\left(Z\left(n\right)\right)=0_W\right)\to D\left(X\right)<0+1$$
73		0p1e1	$$⊢0+1=1$$
74	72 73	breqtrdi	$$⊢\left(\left(\phi \wedge n\in I\right)\wedge X\underset{\dot{}}{-}A\left(Z\left(n\right)\right)=0_W\right)\to D\left(X\right)<1$$
75	53 54 74	xrgtned	$$⊢\left(\left(\phi \wedge n\in I\right)\wedge X\underset{\dot{}}{-}A\left(Z\left(n\right)\right)=0_W\right)\to 1\ne D\left(X\right)$$
76	75	necomd	$$⊢\left(\left(\phi \wedge n\in I\right)\wedge X\underset{\dot{}}{-}A\left(Z\left(n\right)\right)=0_W\right)\to D\left(X\right)\ne 1$$
77	76	neneqd	$$⊢\left(\left(\phi \wedge n\in I\right)\wedge X\underset{\dot{}}{-}A\left(Z\left(n\right)\right)=0_W\right)\to \neg D\left(X\right)=1$$
78	49 77	pm2.65da	$$⊢\left(\phi \wedge n\in I\right)\to \neg X\underset{\dot{}}{-}A\left(Z\left(n\right)\right)=0_W$$
79	78	neqned	$$⊢\left(\phi \wedge n\in I\right)\to X\underset{\dot{}}{-}A\left(Z\left(n\right)\right)\ne 0_W$$
80	44 79	eldifsnd	$$⊢\left(\phi \wedge n\in I\right)\to X\underset{\dot{}}{-}A\left(Z\left(n\right)\right)\in \left({\mathrm{Base}}_W\setminus \left\{0_W\right\}\right)$$
81	80	fmpttd	$$⊢\phi \to \left(n\in I⟼X\underset{\dot{}}{-}A\left(Z\left(n\right)\right)\right):I⟶{\mathrm{Base}}_W\setminus \left\{0_W\right\}$$
82	18 1 20 4 21 14 15 81	deg1prod	$$⊢\phi \to D\left(\underset{n\in I}{{\sum }_M}\left(X\underset{\dot{}}{-}A\left(Z\left(n\right)\right)\right)\right)=\sum _{k\in I}D\left(\left(n\in I⟼X\underset{\dot{}}{-}A\left(Z\left(n\right)\right)\right)\left(k\right)\right)$$
83		eqid	$$⊢\left(n\in I⟼X\underset{\dot{}}{-}A\left(Z\left(n\right)\right)\right)=\left(n\in I⟼X\underset{\dot{}}{-}A\left(Z\left(n\right)\right)\right)$$
84		2fveq3	$$⊢n=k\to A\left(Z\left(n\right)\right)=A\left(Z\left(k\right)\right)$$
85	84	oveq2d	$$⊢n=k\to X\underset{\dot{}}{-}A\left(Z\left(n\right)\right)=X\underset{\dot{}}{-}A\left(Z\left(k\right)\right)$$
86		simpr	$$⊢\left(\phi \wedge k\in I\right)\to k\in I$$
87		ovexd	$$⊢\left(\phi \wedge k\in I\right)\to X\underset{\dot{}}{-}A\left(Z\left(k\right)\right)\in \mathrm{V}$$
88	83 85 86 87	fvmptd3	$$⊢\left(\phi \wedge k\in I\right)\to \left(n\in I⟼X\underset{\dot{}}{-}A\left(Z\left(n\right)\right)\right)\left(k\right)=X\underset{\dot{}}{-}A\left(Z\left(k\right)\right)$$
89	88	fveq2d	$$⊢\left(\phi \wedge k\in I\right)\to D\left(\left(n\in I⟼X\underset{\dot{}}{-}A\left(Z\left(n\right)\right)\right)\left(k\right)\right)=D\left(X\underset{\dot{}}{-}A\left(Z\left(k\right)\right)\right)$$
90	18 1 20	deg1xrcl	$$⊢A\left(Z\left(n\right)\right)\in {\mathrm{Base}}_W\to D\left(A\left(Z\left(n\right)\right)\right)\in {ℝ}^{*}$$
91	43 90	syl	$$⊢\left(\phi \wedge n\in I\right)\to D\left(A\left(Z\left(n\right)\right)\right)\in {ℝ}^{*}$$
92		0xr	$$⊢0\in {ℝ}^{*}$$
93	92	a1i	$$⊢\left(\phi \wedge n\in I\right)\to 0\in {ℝ}^{*}$$
94		1xr	$$⊢1\in {ℝ}^{*}$$
95	94	a1i	$$⊢\left(\phi \wedge n\in I\right)\to 1\in {ℝ}^{*}$$
96		0lt1	$$⊢0<1$$
97	96	a1i	$$⊢\left(\phi \wedge n\in I\right)\to 0<1$$
98	91 93 95 67 97	xrlelttrd	$$⊢\left(\phi \wedge n\in I\right)\to D\left(A\left(Z\left(n\right)\right)\right)<1$$
99	48	adantr	$$⊢\left(\phi \wedge n\in I\right)\to D\left(X\right)=1$$
100	98 99	breqtrrd	$$⊢\left(\phi \wedge n\in I\right)\to D\left(A\left(Z\left(n\right)\right)\right)<D\left(X\right)$$
101	1 18 65 20 3 29 43 100	deg1sub	$$⊢\left(\phi \wedge n\in I\right)\to D\left(X\underset{\dot{}}{-}A\left(Z\left(n\right)\right)\right)=D\left(X\right)$$
102	101 99	eqtrd	$$⊢\left(\phi \wedge n\in I\right)\to D\left(X\underset{\dot{}}{-}A\left(Z\left(n\right)\right)\right)=1$$
103	102	ralrimiva	$$⊢\phi \to \forall n\in ID\left(X\underset{\dot{}}{-}A\left(Z\left(n\right)\right)\right)=1$$
104	85	fveqeq2d	$$⊢n=k\to \left(D\left(X\underset{\dot{}}{-}A\left(Z\left(n\right)\right)\right)=1\leftrightarrow D\left(X\underset{\dot{}}{-}A\left(Z\left(k\right)\right)\right)=1\right)$$
105	104	cbvralvw	$$⊢\forall n\in ID\left(X\underset{\dot{}}{-}A\left(Z\left(n\right)\right)\right)=1\leftrightarrow \forall k\in ID\left(X\underset{\dot{}}{-}A\left(Z\left(k\right)\right)\right)=1$$
106	103 105	sylib	$$⊢\phi \to \forall k\in ID\left(X\underset{\dot{}}{-}A\left(Z\left(k\right)\right)\right)=1$$
107	106	r19.21bi	$$⊢\left(\phi \wedge k\in I\right)\to D\left(X\underset{\dot{}}{-}A\left(Z\left(k\right)\right)\right)=1$$
108	89 107	eqtrd	$$⊢\left(\phi \wedge k\in I\right)\to D\left(\left(n\in I⟼X\underset{\dot{}}{-}A\left(Z\left(n\right)\right)\right)\left(k\right)\right)=1$$
109	108	sumeq2dv	$$⊢\phi \to \sum _{k\in I}D\left(\left(n\in I⟼X\underset{\dot{}}{-}A\left(Z\left(n\right)\right)\right)\left(k\right)\right)=\sum _{k\in I}1$$
110		1cnd	$$⊢\phi \to 1\in ℂ$$
111		fsumconst	$$⊢\left(I\in \mathrm{Fin}\wedge 1\in ℂ\right)\to \sum _{k\in I}1=\left|I\right|\cdot 1$$
112	14 110 111	syl2anc	$$⊢\phi \to \sum _{k\in I}1=\left|I\right|\cdot 1$$
113		hashcl	$$⊢I\in \mathrm{Fin}\to \left|I\right|\in {\mathbb{N}}_0$$
114	14 113	syl	$$⊢\phi \to \left|I\right|\in {\mathbb{N}}_0$$
115	114	nn0cnd	$$⊢\phi \to \left|I\right|\in ℂ$$
116	115	mulridd	$$⊢\phi \to \left|I\right|\cdot 1=\left|I\right|$$
117	116 13	eqtr4di	$$⊢\phi \to \left|I\right|\cdot 1=H$$
118	109 112 117	3eqtrd	$$⊢\phi \to \sum _{k\in I}D\left(\left(n\in I⟼X\underset{\dot{}}{-}A\left(Z\left(n\right)\right)\right)\left(k\right)\right)=H$$
119	82 118	eqtrd	$$⊢\phi \to D\left(\underset{n\in I}{{\sum }_M}\left(X\underset{\dot{}}{-}A\left(Z\left(n\right)\right)\right)\right)=H$$
120	19 119	eqtrid	$$⊢\phi \to D\left(F\right)=H$$