Theorem deg1pow

Description: Exact degree of a power of a polynomial in an integral domain. (Contributed by metakunt, 6-May-2025)

	Ref	Expression
Hypotheses	deg1pow.1	$$⊢\phi \to R\in \mathrm{IDomn}$$
	deg1pow.2	$$⊢\phi \to F\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
	deg1pow.3	$$⊢\phi \to F\ne 0_{{\mathrm{Poly}}_1\left(R\right)}$$
	deg1pow.4	$$⊢\phi \to A\in {\mathbb{N}}_0$$
	deg1pow.5	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}$$
	deg1pow.6	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
Assertion	deg1pow	$$⊢\phi \to D\left(A\underset{\dot{}}{\times }F\right)=AD\left(F\right)$$

Proof

Step	Hyp	Ref	Expression
1		deg1pow.1	$$⊢\phi \to R\in \mathrm{IDomn}$$
2		deg1pow.2	$$⊢\phi \to F\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
3		deg1pow.3	$$⊢\phi \to F\ne 0_{{\mathrm{Poly}}_1\left(R\right)}$$
4		deg1pow.4	$$⊢\phi \to A\in {\mathbb{N}}_0$$
5		deg1pow.5	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}$$
6		deg1pow.6	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
7		fvoveq1	$$⊢x=0\to D\left(x\underset{\dot{}}{\times }F\right)=D\left(0\underset{\dot{}}{\times }F\right)$$
8		oveq1	$$⊢x=0\to xD\left(F\right)=0\cdot D\left(F\right)$$
9	7 8	eqeq12d	$$⊢x=0\to \left(D\left(x\underset{\dot{}}{\times }F\right)=xD\left(F\right)\leftrightarrow D\left(0\underset{\dot{}}{\times }F\right)=0\cdot D\left(F\right)\right)$$
10		fvoveq1	$$⊢x=y\to D\left(x\underset{\dot{}}{\times }F\right)=D\left(y\underset{\dot{}}{\times }F\right)$$
11		oveq1	$$⊢x=y\to xD\left(F\right)=yD\left(F\right)$$
12	10 11	eqeq12d	$$⊢x=y\to \left(D\left(x\underset{\dot{}}{\times }F\right)=xD\left(F\right)\leftrightarrow D\left(y\underset{\dot{}}{\times }F\right)=yD\left(F\right)\right)$$
13		fvoveq1	$$⊢x=y+1\to D\left(x\underset{\dot{}}{\times }F\right)=D\left(\left(y+1\right)\underset{\dot{}}{\times }F\right)$$
14		oveq1	$$⊢x=y+1\to xD\left(F\right)=\left(y+1\right)D\left(F\right)$$
15	13 14	eqeq12d	$$⊢x=y+1\to \left(D\left(x\underset{\dot{}}{\times }F\right)=xD\left(F\right)\leftrightarrow D\left(\left(y+1\right)\underset{\dot{}}{\times }F\right)=\left(y+1\right)D\left(F\right)\right)$$
16		fvoveq1	$$⊢x=A\to D\left(x\underset{\dot{}}{\times }F\right)=D\left(A\underset{\dot{}}{\times }F\right)$$
17		oveq1	$$⊢x=A\to xD\left(F\right)=AD\left(F\right)$$
18	16 17	eqeq12d	$$⊢x=A\to \left(D\left(x\underset{\dot{}}{\times }F\right)=xD\left(F\right)\leftrightarrow D\left(A\underset{\dot{}}{\times }F\right)=AD\left(F\right)\right)$$
19		eqid	$$⊢{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}={\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}$$
20		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
21	19 20	mgpbas	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}$$
22		eqid	$$⊢1_{{\mathrm{Poly}}_1\left(R\right)}=1_{{\mathrm{Poly}}_1\left(R\right)}$$
23	19 22	ringidval	$$⊢1_{{\mathrm{Poly}}_1\left(R\right)}=0_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}$$
24	21 23 5	mulg0	$$⊢F\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}\to 0\underset{\dot{}}{\times }F=1_{{\mathrm{Poly}}_1\left(R\right)}$$
25	2 24	syl	$$⊢\phi \to 0\underset{\dot{}}{\times }F=1_{{\mathrm{Poly}}_1\left(R\right)}$$
26	25	fveq2d	$$⊢\phi \to D\left(0\underset{\dot{}}{\times }F\right)=D\left(1_{{\mathrm{Poly}}_1\left(R\right)}\right)$$
27		isidom	$$⊢R\in \mathrm{IDomn}\leftrightarrow \left(R\in \mathrm{CRing}\wedge R\in \mathrm{Domn}\right)$$
28	27	simprbi	$$⊢R\in \mathrm{IDomn}\to R\in \mathrm{Domn}$$
29		domnring	$$⊢R\in \mathrm{Domn}\to R\in \mathrm{Ring}$$
30	28 29	syl	$$⊢R\in \mathrm{IDomn}\to R\in \mathrm{Ring}$$
31	1 30	syl	$$⊢\phi \to R\in \mathrm{Ring}$$
32		eqid	$$⊢{\mathrm{Poly}}_1\left(R\right)={\mathrm{Poly}}_1\left(R\right)$$
33		eqid	$$⊢\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)=\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)$$
34		eqid	$$⊢1_R=1_R$$
35	32 33 34 22	ply1scl1	$$⊢R\in \mathrm{Ring}\to \mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(1_R\right)=1_{{\mathrm{Poly}}_1\left(R\right)}$$
36	31 35	syl	$$⊢\phi \to \mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(1_R\right)=1_{{\mathrm{Poly}}_1\left(R\right)}$$
37	36	eqcomd	$$⊢\phi \to 1_{{\mathrm{Poly}}_1\left(R\right)}=\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(1_R\right)$$
38	37	fveq2d	$$⊢\phi \to D\left(1_{{\mathrm{Poly}}_1\left(R\right)}\right)=D\left(\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(1_R\right)\right)$$
39		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
40	39 34	ringidcl	$$⊢R\in \mathrm{Ring}\to 1_R\in {\mathrm{Base}}_R$$
41	31 40	syl	$$⊢\phi \to 1_R\in {\mathrm{Base}}_R$$
42	1 28	syl	$$⊢\phi \to R\in \mathrm{Domn}$$
43		domnnzr	$$⊢R\in \mathrm{Domn}\to R\in \mathrm{NzRing}$$
44	42 43	syl	$$⊢\phi \to R\in \mathrm{NzRing}$$
45		eqid	$$⊢0_R=0_R$$
46	34 45	nzrnz	$$⊢R\in \mathrm{NzRing}\to 1_R\ne 0_R$$
47	44 46	syl	$$⊢\phi \to 1_R\ne 0_R$$
48	6 32 39 33 45	deg1scl	$$⊢\left(R\in \mathrm{Ring}\wedge 1_R\in {\mathrm{Base}}_R\wedge 1_R\ne 0_R\right)\to D\left(\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(1_R\right)\right)=0$$
49	31 41 47 48	syl3anc	$$⊢\phi \to D\left(\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(1_R\right)\right)=0$$
50	38 49	eqtrd	$$⊢\phi \to D\left(1_{{\mathrm{Poly}}_1\left(R\right)}\right)=0$$
51	26 50	eqtrd	$$⊢\phi \to D\left(0\underset{\dot{}}{\times }F\right)=0$$
52		eqid	$$⊢0_{{\mathrm{Poly}}_1\left(R\right)}=0_{{\mathrm{Poly}}_1\left(R\right)}$$
53	6 32 52 20	deg1nn0cl	$$⊢\left(R\in \mathrm{Ring}\wedge F\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}\wedge F\ne 0_{{\mathrm{Poly}}_1\left(R\right)}\right)\to D\left(F\right)\in {\mathbb{N}}_0$$
54	31 2 3 53	syl3anc	$$⊢\phi \to D\left(F\right)\in {\mathbb{N}}_0$$
55	54	nn0cnd	$$⊢\phi \to D\left(F\right)\in ℂ$$
56	55	mul02d	$$⊢\phi \to 0\cdot D\left(F\right)=0$$
57	56	eqcomd	$$⊢\phi \to 0=0\cdot D\left(F\right)$$
58	51 57	eqtrd	$$⊢\phi \to D\left(0\underset{\dot{}}{\times }F\right)=0\cdot D\left(F\right)$$
59	32	ply1idom	$$⊢R\in \mathrm{IDomn}\to {\mathrm{Poly}}_1\left(R\right)\in \mathrm{IDomn}$$
60	1 59	syl	$$⊢\phi \to {\mathrm{Poly}}_1\left(R\right)\in \mathrm{IDomn}$$
61	60	idomringd	$$⊢\phi \to {\mathrm{Poly}}_1\left(R\right)\in \mathrm{Ring}$$
62	61	adantr	$$⊢\left(\phi \wedge y\in {\mathbb{N}}_0\right)\to {\mathrm{Poly}}_1\left(R\right)\in \mathrm{Ring}$$
63	62	adantr	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge D\left(y\underset{\dot{}}{\times }F\right)=yD\left(F\right)\right)\to {\mathrm{Poly}}_1\left(R\right)\in \mathrm{Ring}$$
64	19	ringmgp	$$⊢{\mathrm{Poly}}_1\left(R\right)\in \mathrm{Ring}\to {\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}\in \mathrm{Mnd}$$
65	63 64	syl	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge D\left(y\underset{\dot{}}{\times }F\right)=yD\left(F\right)\right)\to {\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}\in \mathrm{Mnd}$$
66		simplr	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge D\left(y\underset{\dot{}}{\times }F\right)=yD\left(F\right)\right)\to y\in {\mathbb{N}}_0$$
67	2	ad2antrr	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge D\left(y\underset{\dot{}}{\times }F\right)=yD\left(F\right)\right)\to F\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
68		eqid	$$⊢{+}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}={+}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}$$
69	21 5 68	mulgnn0p1	$$⊢\left({\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}\in \mathrm{Mnd}\wedge y\in {\mathbb{N}}_0\wedge F\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}\right)\to \left(y+1\right)\underset{\dot{}}{\times }F=\left(y\underset{\dot{}}{\times }F\right){+}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}F$$
70	65 66 67 69	syl3anc	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge D\left(y\underset{\dot{}}{\times }F\right)=yD\left(F\right)\right)\to \left(y+1\right)\underset{\dot{}}{\times }F=\left(y\underset{\dot{}}{\times }F\right){+}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}F$$
71	70	fveq2d	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge D\left(y\underset{\dot{}}{\times }F\right)=yD\left(F\right)\right)\to D\left(\left(y+1\right)\underset{\dot{}}{\times }F\right)=D\left(\left(y\underset{\dot{}}{\times }F\right){+}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}F\right)$$
72		eqid	$$⊢{\cdot }_{{\mathrm{Poly}}_1\left(R\right)}={\cdot }_{{\mathrm{Poly}}_1\left(R\right)}$$
73	19 72	mgpplusg	$$⊢{\cdot }_{{\mathrm{Poly}}_1\left(R\right)}={+}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}$$
74	73	eqcomi	$$⊢{+}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}={\cdot }_{{\mathrm{Poly}}_1\left(R\right)}$$
75	1	idomdomd	$$⊢\phi \to R\in \mathrm{Domn}$$
76	75	adantr	$$⊢\left(\phi \wedge y\in {\mathbb{N}}_0\right)\to R\in \mathrm{Domn}$$
77	76	adantr	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge D\left(y\underset{\dot{}}{\times }F\right)=yD\left(F\right)\right)\to R\in \mathrm{Domn}$$
78	21 5 65 66 67	mulgnn0cld	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge D\left(y\underset{\dot{}}{\times }F\right)=yD\left(F\right)\right)\to y\underset{\dot{}}{\times }F\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
79	60	adantr	$$⊢\left(\phi \wedge y\in {\mathbb{N}}_0\right)\to {\mathrm{Poly}}_1\left(R\right)\in \mathrm{IDomn}$$
80	79	adantr	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge D\left(y\underset{\dot{}}{\times }F\right)=yD\left(F\right)\right)\to {\mathrm{Poly}}_1\left(R\right)\in \mathrm{IDomn}$$
81	3	ad2antrr	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge D\left(y\underset{\dot{}}{\times }F\right)=yD\left(F\right)\right)\to F\ne 0_{{\mathrm{Poly}}_1\left(R\right)}$$
82	80 67 81 66 5	idomnnzpownz	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge D\left(y\underset{\dot{}}{\times }F\right)=yD\left(F\right)\right)\to y\underset{\dot{}}{\times }F\ne 0_{{\mathrm{Poly}}_1\left(R\right)}$$
83	6 32 20 74 52 77 78 82 67 81	deg1mul	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge D\left(y\underset{\dot{}}{\times }F\right)=yD\left(F\right)\right)\to D\left(\left(y\underset{\dot{}}{\times }F\right){+}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}F\right)=D\left(y\underset{\dot{}}{\times }F\right)+D\left(F\right)$$
84		simpr	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge D\left(y\underset{\dot{}}{\times }F\right)=yD\left(F\right)\right)\to D\left(y\underset{\dot{}}{\times }F\right)=yD\left(F\right)$$
85	84	oveq1d	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge D\left(y\underset{\dot{}}{\times }F\right)=yD\left(F\right)\right)\to D\left(y\underset{\dot{}}{\times }F\right)+D\left(F\right)=yD\left(F\right)+D\left(F\right)$$
86	66	nn0cnd	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge D\left(y\underset{\dot{}}{\times }F\right)=yD\left(F\right)\right)\to y\in ℂ$$
87	55	ad2antrr	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge D\left(y\underset{\dot{}}{\times }F\right)=yD\left(F\right)\right)\to D\left(F\right)\in ℂ$$
88	86 87	adddirp1d	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge D\left(y\underset{\dot{}}{\times }F\right)=yD\left(F\right)\right)\to \left(y+1\right)D\left(F\right)=yD\left(F\right)+D\left(F\right)$$
89	88	eqcomd	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge D\left(y\underset{\dot{}}{\times }F\right)=yD\left(F\right)\right)\to yD\left(F\right)+D\left(F\right)=\left(y+1\right)D\left(F\right)$$
90	85 89	eqtrd	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge D\left(y\underset{\dot{}}{\times }F\right)=yD\left(F\right)\right)\to D\left(y\underset{\dot{}}{\times }F\right)+D\left(F\right)=\left(y+1\right)D\left(F\right)$$
91	83 90	eqtrd	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge D\left(y\underset{\dot{}}{\times }F\right)=yD\left(F\right)\right)\to D\left(\left(y\underset{\dot{}}{\times }F\right){+}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}F\right)=\left(y+1\right)D\left(F\right)$$
92	71 91	eqtrd	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge D\left(y\underset{\dot{}}{\times }F\right)=yD\left(F\right)\right)\to D\left(\left(y+1\right)\underset{\dot{}}{\times }F\right)=\left(y+1\right)D\left(F\right)$$
93	9 12 15 18 58 92	nn0indd	$$⊢\left(\phi \wedge A\in {\mathbb{N}}_0\right)\to D\left(A\underset{\dot{}}{\times }F\right)=AD\left(F\right)$$
94	93	ex	$$⊢\phi \to \left(A\in {\mathbb{N}}_0\to D\left(A\underset{\dot{}}{\times }F\right)=AD\left(F\right)\right)$$
95	4 94	mpd	$$⊢\phi \to D\left(A\underset{\dot{}}{\times }F\right)=AD\left(F\right)$$