dgrcolem1

Description: The degree of a composition of a monomial with a polynomial. (Contributed by Mario Carneiro, 15-Sep-2014)

	Ref	Expression
Hypotheses	dgrcolem1.1	$⊢ N = \deg (G)$
	dgrcolem1.2	$⊢ φ \to M \in ℕ$
	dgrcolem1.3	$⊢ φ \to N \in ℕ$
	dgrcolem1.4	$⊢ φ \to G \in Poly (S)$
Assertion	dgrcolem1	$⊢ φ \to \deg ((x \in ℂ ⟼ {G (x)}^{M})) = M \cdot N$

Proof

Step	Hyp	Ref	Expression
1		dgrcolem1.1	$⊢ N = \deg (G)$
2		dgrcolem1.2	$⊢ φ \to M \in ℕ$
3		dgrcolem1.3	$⊢ φ \to N \in ℕ$
4		dgrcolem1.4	$⊢ φ \to G \in Poly (S)$
5		oveq2	$⊢ y = 1 \to {G (x)}^{y} = {G (x)}^{1}$
6	5	mpteq2dv	$⊢ y = 1 \to (x \in ℂ ⟼ {G (x)}^{y}) = (x \in ℂ ⟼ {G (x)}^{1})$
7	6	fveq2d	$⊢ y = 1 \to \deg ((x \in ℂ ⟼ {G (x)}^{y})) = \deg ((x \in ℂ ⟼ {G (x)}^{1}))$
8		oveq1	$⊢ y = 1 \to y \cdot N = 1 \cdot N$
9	7 8	eqeq12d	$⊢ y = 1 \to (\deg ((x \in ℂ ⟼ {G (x)}^{y})) = y \cdot N \leftrightarrow \deg ((x \in ℂ ⟼ {G (x)}^{1})) = 1 \cdot N)$
10	9	imbi2d	$⊢ y = 1 \to ((φ \to \deg ((x \in ℂ ⟼ {G (x)}^{y})) = y \cdot N) \leftrightarrow (φ \to \deg ((x \in ℂ ⟼ {G (x)}^{1})) = 1 \cdot N))$
11		oveq2	$⊢ y = d \to {G (x)}^{y} = {G (x)}^{d}$
12	11	mpteq2dv	$⊢ y = d \to (x \in ℂ ⟼ {G (x)}^{y}) = (x \in ℂ ⟼ {G (x)}^{d})$
13	12	fveq2d	$⊢ y = d \to \deg ((x \in ℂ ⟼ {G (x)}^{y})) = \deg ((x \in ℂ ⟼ {G (x)}^{d}))$
14		oveq1	$⊢ y = d \to y \cdot N = d \cdot N$
15	13 14	eqeq12d	$⊢ y = d \to (\deg ((x \in ℂ ⟼ {G (x)}^{y})) = y \cdot N \leftrightarrow \deg ((x \in ℂ ⟼ {G (x)}^{d})) = d \cdot N)$
16	15	imbi2d	$⊢ y = d \to ((φ \to \deg ((x \in ℂ ⟼ {G (x)}^{y})) = y \cdot N) \leftrightarrow (φ \to \deg ((x \in ℂ ⟼ {G (x)}^{d})) = d \cdot N))$
17		oveq2	$⊢ y = d + 1 \to {G (x)}^{y} = {G (x)}^{d + 1}$
18	17	mpteq2dv	$⊢ y = d + 1 \to (x \in ℂ ⟼ {G (x)}^{y}) = (x \in ℂ ⟼ {G (x)}^{d + 1})$
19	18	fveq2d	$⊢ y = d + 1 \to \deg ((x \in ℂ ⟼ {G (x)}^{y})) = \deg ((x \in ℂ ⟼ {G (x)}^{d + 1}))$
20		oveq1	$⊢ y = d + 1 \to y \cdot N = (d + 1) \cdot N$
21	19 20	eqeq12d	$⊢ y = d + 1 \to (\deg ((x \in ℂ ⟼ {G (x)}^{y})) = y \cdot N \leftrightarrow \deg ((x \in ℂ ⟼ {G (x)}^{d + 1})) = (d + 1) \cdot N)$
22	21	imbi2d	$⊢ y = d + 1 \to ((φ \to \deg ((x \in ℂ ⟼ {G (x)}^{y})) = y \cdot N) \leftrightarrow (φ \to \deg ((x \in ℂ ⟼ {G (x)}^{d + 1})) = (d + 1) \cdot N))$
23		oveq2	$⊢ y = M \to {G (x)}^{y} = {G (x)}^{M}$
24	23	mpteq2dv	$⊢ y = M \to (x \in ℂ ⟼ {G (x)}^{y}) = (x \in ℂ ⟼ {G (x)}^{M})$
25	24	fveq2d	$⊢ y = M \to \deg ((x \in ℂ ⟼ {G (x)}^{y})) = \deg ((x \in ℂ ⟼ {G (x)}^{M}))$
26		oveq1	$⊢ y = M \to y \cdot N = M \cdot N$
27	25 26	eqeq12d	$⊢ y = M \to (\deg ((x \in ℂ ⟼ {G (x)}^{y})) = y \cdot N \leftrightarrow \deg ((x \in ℂ ⟼ {G (x)}^{M})) = M \cdot N)$
28	27	imbi2d	$⊢ y = M \to ((φ \to \deg ((x \in ℂ ⟼ {G (x)}^{y})) = y \cdot N) \leftrightarrow (φ \to \deg ((x \in ℂ ⟼ {G (x)}^{M})) = M \cdot N))$
29		plyf	$⊢ G \in Poly (S) \to G : ℂ ⟶ ℂ$
30	4 29	syl	$⊢ φ \to G : ℂ ⟶ ℂ$
31	30	ffvelrnda	$⊢ (φ \land x \in ℂ) \to G (x) \in ℂ$
32	31	exp1d	$⊢ (φ \land x \in ℂ) \to {G (x)}^{1} = G (x)$
33	32	mpteq2dva	$⊢ φ \to (x \in ℂ ⟼ {G (x)}^{1}) = (x \in ℂ ⟼ G (x))$
34	30	feqmptd	$⊢ φ \to G = (x \in ℂ ⟼ G (x))$
35	33 34	eqtr4d	$⊢ φ \to (x \in ℂ ⟼ {G (x)}^{1}) = G$
36	35	fveq2d	$⊢ φ \to \deg ((x \in ℂ ⟼ {G (x)}^{1})) = \deg (G)$
37	36 1	eqtr4di	$⊢ φ \to \deg ((x \in ℂ ⟼ {G (x)}^{1})) = N$
38	3	nncnd	$⊢ φ \to N \in ℂ$
39	38	mulid2d	$⊢ φ \to 1 \cdot N = N$
40	37 39	eqtr4d	$⊢ φ \to \deg ((x \in ℂ ⟼ {G (x)}^{1})) = 1 \cdot N$
41	31	adantlr	$⊢ ((φ \land d \in ℕ) \land x \in ℂ) \to G (x) \in ℂ$
42		nnnn0	$⊢ d \in ℕ \to d \in ℕ_{0}$
43	42	adantl	$⊢ (φ \land d \in ℕ) \to d \in ℕ_{0}$
44	43	adantr	$⊢ ((φ \land d \in ℕ) \land x \in ℂ) \to d \in ℕ_{0}$
45	41 44	expp1d	$⊢ ((φ \land d \in ℕ) \land x \in ℂ) \to {G (x)}^{d + 1} = {G (x)}^{d} G (x)$
46	45	mpteq2dva	$⊢ (φ \land d \in ℕ) \to (x \in ℂ ⟼ {G (x)}^{d + 1}) = (x \in ℂ ⟼ {G (x)}^{d} G (x))$
47		cnex	$⊢ ℂ \in V$
48	47	a1i	$⊢ (φ \land d \in ℕ) \to ℂ \in V$
49		ovexd	$⊢ ((φ \land d \in ℕ) \land x \in ℂ) \to {G (x)}^{d} \in V$
50		eqidd	$⊢ (φ \land d \in ℕ) \to (x \in ℂ ⟼ {G (x)}^{d}) = (x \in ℂ ⟼ {G (x)}^{d})$
51	34	adantr	$⊢ (φ \land d \in ℕ) \to G = (x \in ℂ ⟼ G (x))$
52	48 49 41 50 51	offval2	$⊢ (φ \land d \in ℕ) \to (x \in ℂ ⟼ {G (x)}^{d}) \times_{f} G = (x \in ℂ ⟼ {G (x)}^{d} G (x))$
53	46 52	eqtr4d	$⊢ (φ \land d \in ℕ) \to (x \in ℂ ⟼ {G (x)}^{d + 1}) = (x \in ℂ ⟼ {G (x)}^{d}) \times_{f} G$
54	53	fveq2d	$⊢ (φ \land d \in ℕ) \to \deg ((x \in ℂ ⟼ {G (x)}^{d + 1})) = \deg ((x \in ℂ ⟼ {G (x)}^{d}) \times_{f} G)$
55	54	adantr	$⊢ ((φ \land d \in ℕ) \land \deg ((x \in ℂ ⟼ {G (x)}^{d})) = d \cdot N) \to \deg ((x \in ℂ ⟼ {G (x)}^{d + 1})) = \deg ((x \in ℂ ⟼ {G (x)}^{d}) \times_{f} G)$
56		oveq1	$⊢ \deg ((x \in ℂ ⟼ {G (x)}^{d})) = d \cdot N \to \deg ((x \in ℂ ⟼ {G (x)}^{d})) + N = d \cdot N + N$
57	56	adantl	$⊢ ((φ \land d \in ℕ) \land \deg ((x \in ℂ ⟼ {G (x)}^{d})) = d \cdot N) \to \deg ((x \in ℂ ⟼ {G (x)}^{d})) + N = d \cdot N + N$
58		eqidd	$⊢ (φ \land d \in ℕ) \to (y \in ℂ ⟼ y^{d}) = (y \in ℂ ⟼ y^{d})$
59		oveq1	$⊢ y = G (x) \to y^{d} = {G (x)}^{d}$
60	41 51 58 59	fmptco	$⊢ (φ \land d \in ℕ) \to (y \in ℂ ⟼ y^{d}) \circ G = (x \in ℂ ⟼ {G (x)}^{d})$
61		ssidd	$⊢ (φ \land d \in ℕ) \to ℂ \subseteq ℂ$
62		1cnd	$⊢ (φ \land d \in ℕ) \to 1 \in ℂ$
63		plypow	$⊢ (ℂ \subseteq ℂ \land 1 \in ℂ \land d \in ℕ_{0}) \to (y \in ℂ ⟼ y^{d}) \in Poly (ℂ)$
64	61 62 43 63	syl3anc	$⊢ (φ \land d \in ℕ) \to (y \in ℂ ⟼ y^{d}) \in Poly (ℂ)$
65		plyssc	$⊢ Poly (S) \subseteq Poly (ℂ)$
66	4	adantr	$⊢ (φ \land d \in ℕ) \to G \in Poly (S)$
67	65 66	sselid	$⊢ (φ \land d \in ℕ) \to G \in Poly (ℂ)$
68		addcl	$⊢ (z \in ℂ \land w \in ℂ) \to z + w \in ℂ$
69	68	adantl	$⊢ ((φ \land d \in ℕ) \land (z \in ℂ \land w \in ℂ)) \to z + w \in ℂ$
70		mulcl	$⊢ (z \in ℂ \land w \in ℂ) \to z w \in ℂ$
71	70	adantl	$⊢ ((φ \land d \in ℕ) \land (z \in ℂ \land w \in ℂ)) \to z w \in ℂ$
72	64 67 69 71	plyco	$⊢ (φ \land d \in ℕ) \to (y \in ℂ ⟼ y^{d}) \circ G \in Poly (ℂ)$
73	60 72	eqeltrrd	$⊢ (φ \land d \in ℕ) \to (x \in ℂ ⟼ {G (x)}^{d}) \in Poly (ℂ)$
74	73	adantr	$⊢ ((φ \land d \in ℕ) \land \deg ((x \in ℂ ⟼ {G (x)}^{d})) = d \cdot N) \to (x \in ℂ ⟼ {G (x)}^{d}) \in Poly (ℂ)$
75		simpr	$⊢ ((φ \land d \in ℕ) \land \deg ((x \in ℂ ⟼ {G (x)}^{d})) = d \cdot N) \to \deg ((x \in ℂ ⟼ {G (x)}^{d})) = d \cdot N$
76		simpr	$⊢ (φ \land d \in ℕ) \to d \in ℕ$
77	3	adantr	$⊢ (φ \land d \in ℕ) \to N \in ℕ$
78	76 77	nnmulcld	$⊢ (φ \land d \in ℕ) \to d \cdot N \in ℕ$
79	78	nnne0d	$⊢ (φ \land d \in ℕ) \to d \cdot N \neq 0$
80	79	adantr	$⊢ ((φ \land d \in ℕ) \land \deg ((x \in ℂ ⟼ {G (x)}^{d})) = d \cdot N) \to d \cdot N \neq 0$
81	75 80	eqnetrd	$⊢ ((φ \land d \in ℕ) \land \deg ((x \in ℂ ⟼ {G (x)}^{d})) = d \cdot N) \to \deg ((x \in ℂ ⟼ {G (x)}^{d})) \neq 0$
82		fveq2	$⊢ (x \in ℂ ⟼ {G (x)}^{d}) = 0_{𝑝} \to \deg ((x \in ℂ ⟼ {G (x)}^{d})) = \deg (0_{𝑝})$
83		dgr0	$⊢ \deg (0_{𝑝}) = 0$
84	82 83	eqtrdi	$⊢ (x \in ℂ ⟼ {G (x)}^{d}) = 0_{𝑝} \to \deg ((x \in ℂ ⟼ {G (x)}^{d})) = 0$
85	84	necon3i	$⊢ \deg ((x \in ℂ ⟼ {G (x)}^{d})) \neq 0 \to (x \in ℂ ⟼ {G (x)}^{d}) \neq 0_{𝑝}$
86	81 85	syl	$⊢ ((φ \land d \in ℕ) \land \deg ((x \in ℂ ⟼ {G (x)}^{d})) = d \cdot N) \to (x \in ℂ ⟼ {G (x)}^{d}) \neq 0_{𝑝}$
87	67	adantr	$⊢ ((φ \land d \in ℕ) \land \deg ((x \in ℂ ⟼ {G (x)}^{d})) = d \cdot N) \to G \in Poly (ℂ)$
88	3	nnne0d	$⊢ φ \to N \neq 0$
89		fveq2	$⊢ G = 0_{𝑝} \to \deg (G) = \deg (0_{𝑝})$
90	89 83	eqtrdi	$⊢ G = 0_{𝑝} \to \deg (G) = 0$
91	1 90	eqtrid	$⊢ G = 0_{𝑝} \to N = 0$
92	91	necon3i	$⊢ N \neq 0 \to G \neq 0_{𝑝}$
93	88 92	syl	$⊢ φ \to G \neq 0_{𝑝}$
94	93	adantr	$⊢ (φ \land d \in ℕ) \to G \neq 0_{𝑝}$
95	94	adantr	$⊢ ((φ \land d \in ℕ) \land \deg ((x \in ℂ ⟼ {G (x)}^{d})) = d \cdot N) \to G \neq 0_{𝑝}$
96		eqid	$⊢ \deg ((x \in ℂ ⟼ {G (x)}^{d})) = \deg ((x \in ℂ ⟼ {G (x)}^{d}))$
97	96 1	dgrmul	$⊢ (((x \in ℂ ⟼ {G (x)}^{d}) \in Poly (ℂ) \land (x \in ℂ ⟼ {G (x)}^{d}) \neq 0_{𝑝}) \land (G \in Poly (ℂ) \land G \neq 0_{𝑝})) \to \deg ((x \in ℂ ⟼ {G (x)}^{d}) \times_{f} G) = \deg ((x \in ℂ ⟼ {G (x)}^{d})) + N$
98	74 86 87 95 97	syl22anc	$⊢ ((φ \land d \in ℕ) \land \deg ((x \in ℂ ⟼ {G (x)}^{d})) = d \cdot N) \to \deg ((x \in ℂ ⟼ {G (x)}^{d}) \times_{f} G) = \deg ((x \in ℂ ⟼ {G (x)}^{d})) + N$
99		nncn	$⊢ d \in ℕ \to d \in ℂ$
100	99	adantl	$⊢ (φ \land d \in ℕ) \to d \in ℂ$
101	38	adantr	$⊢ (φ \land d \in ℕ) \to N \in ℂ$
102	100 101	adddirp1d	$⊢ (φ \land d \in ℕ) \to (d + 1) \cdot N = d \cdot N + N$
103	102	adantr	$⊢ ((φ \land d \in ℕ) \land \deg ((x \in ℂ ⟼ {G (x)}^{d})) = d \cdot N) \to (d + 1) \cdot N = d \cdot N + N$
104	57 98 103	3eqtr4rd	$⊢ ((φ \land d \in ℕ) \land \deg ((x \in ℂ ⟼ {G (x)}^{d})) = d \cdot N) \to (d + 1) \cdot N = \deg ((x \in ℂ ⟼ {G (x)}^{d}) \times_{f} G)$
105	55 104	eqtr4d	$⊢ ((φ \land d \in ℕ) \land \deg ((x \in ℂ ⟼ {G (x)}^{d})) = d \cdot N) \to \deg ((x \in ℂ ⟼ {G (x)}^{d + 1})) = (d + 1) \cdot N$
106	105	ex	$⊢ (φ \land d \in ℕ) \to (\deg ((x \in ℂ ⟼ {G (x)}^{d})) = d \cdot N \to \deg ((x \in ℂ ⟼ {G (x)}^{d + 1})) = (d + 1) \cdot N)$
107	106	expcom	$⊢ d \in ℕ \to (φ \to (\deg ((x \in ℂ ⟼ {G (x)}^{d})) = d \cdot N \to \deg ((x \in ℂ ⟼ {G (x)}^{d + 1})) = (d + 1) \cdot N))$
108	107	a2d	$⊢ d \in ℕ \to ((φ \to \deg ((x \in ℂ ⟼ {G (x)}^{d})) = d \cdot N) \to (φ \to \deg ((x \in ℂ ⟼ {G (x)}^{d + 1})) = (d + 1) \cdot N))$
109	10 16 22 28 40 108	nnind	$⊢ M \in ℕ \to (φ \to \deg ((x \in ℂ ⟼ {G (x)}^{M})) = M \cdot N)$
110	2 109	mpcom	$⊢ φ \to \deg ((x \in ℂ ⟼ {G (x)}^{M})) = M \cdot N$

Metamath Proof Explorer

Theorem dgrcolem1

Proof