dgrco

Description: The degree of a composition of two polynomials is the product of the degrees. (Contributed by Mario Carneiro, 15-Sep-2014)

	Ref	Expression
Hypotheses	dgrco.1	$⊢ M = \deg (F)$
	dgrco.2	$⊢ N = \deg (G)$
	dgrco.3	$⊢ φ \to F \in Poly (S)$
	dgrco.4	$⊢ φ \to G \in Poly (S)$
Assertion	dgrco	$⊢ φ \to \deg (F \circ G) = M \cdot N$

Proof

Step	Hyp	Ref	Expression
1		dgrco.1	$⊢ M = \deg (F)$
2		dgrco.2	$⊢ N = \deg (G)$
3		dgrco.3	$⊢ φ \to F \in Poly (S)$
4		dgrco.4	$⊢ φ \to G \in Poly (S)$
5		plyssc	$⊢ Poly (S) \subseteq Poly (ℂ)$
6	5 3	sseldi	$⊢ φ \to F \in Poly (ℂ)$
7		dgrcl	$⊢ F \in Poly (S) \to \deg (F) \in ℕ_{0}$
8	3 7	syl	$⊢ φ \to \deg (F) \in ℕ_{0}$
9	1 8	eqeltrid	$⊢ φ \to M \in ℕ_{0}$
10		breq2	$⊢ x = 0 \to (\deg (f) \leq x \leftrightarrow \deg (f) \leq 0)$
11	10	imbi1d	$⊢ x = 0 \to ((\deg (f) \leq x \to \deg (f \circ G) = \deg (f) \cdot N) \leftrightarrow (\deg (f) \leq 0 \to \deg (f \circ G) = \deg (f) \cdot N))$
12	11	ralbidv	$⊢ x = 0 \to (\forall f \in Poly (ℂ) (\deg (f) \leq x \to \deg (f \circ G) = \deg (f) \cdot N) \leftrightarrow \forall f \in Poly (ℂ) (\deg (f) \leq 0 \to \deg (f \circ G) = \deg (f) \cdot N))$
13	12	imbi2d	$⊢ x = 0 \to ((φ \to \forall f \in Poly (ℂ) (\deg (f) \leq x \to \deg (f \circ G) = \deg (f) \cdot N)) \leftrightarrow (φ \to \forall f \in Poly (ℂ) (\deg (f) \leq 0 \to \deg (f \circ G) = \deg (f) \cdot N)))$
14		breq2	$⊢ x = d \to (\deg (f) \leq x \leftrightarrow \deg (f) \leq d)$
15	14	imbi1d	$⊢ x = d \to ((\deg (f) \leq x \to \deg (f \circ G) = \deg (f) \cdot N) \leftrightarrow (\deg (f) \leq d \to \deg (f \circ G) = \deg (f) \cdot N))$
16	15	ralbidv	$⊢ x = d \to (\forall f \in Poly (ℂ) (\deg (f) \leq x \to \deg (f \circ G) = \deg (f) \cdot N) \leftrightarrow \forall f \in Poly (ℂ) (\deg (f) \leq d \to \deg (f \circ G) = \deg (f) \cdot N))$
17	16	imbi2d	$⊢ x = d \to ((φ \to \forall f \in Poly (ℂ) (\deg (f) \leq x \to \deg (f \circ G) = \deg (f) \cdot N)) \leftrightarrow (φ \to \forall f \in Poly (ℂ) (\deg (f) \leq d \to \deg (f \circ G) = \deg (f) \cdot N)))$
18		breq2	$⊢ x = d + 1 \to (\deg (f) \leq x \leftrightarrow \deg (f) \leq d + 1)$
19	18	imbi1d	$⊢ x = d + 1 \to ((\deg (f) \leq x \to \deg (f \circ G) = \deg (f) \cdot N) \leftrightarrow (\deg (f) \leq d + 1 \to \deg (f \circ G) = \deg (f) \cdot N))$
20	19	ralbidv	$⊢ x = d + 1 \to (\forall f \in Poly (ℂ) (\deg (f) \leq x \to \deg (f \circ G) = \deg (f) \cdot N) \leftrightarrow \forall f \in Poly (ℂ) (\deg (f) \leq d + 1 \to \deg (f \circ G) = \deg (f) \cdot N))$
21	20	imbi2d	$⊢ x = d + 1 \to ((φ \to \forall f \in Poly (ℂ) (\deg (f) \leq x \to \deg (f \circ G) = \deg (f) \cdot N)) \leftrightarrow (φ \to \forall f \in Poly (ℂ) (\deg (f) \leq d + 1 \to \deg (f \circ G) = \deg (f) \cdot N)))$
22		breq2	$⊢ x = M \to (\deg (f) \leq x \leftrightarrow \deg (f) \leq M)$
23	22	imbi1d	$⊢ x = M \to ((\deg (f) \leq x \to \deg (f \circ G) = \deg (f) \cdot N) \leftrightarrow (\deg (f) \leq M \to \deg (f \circ G) = \deg (f) \cdot N))$
24	23	ralbidv	$⊢ x = M \to (\forall f \in Poly (ℂ) (\deg (f) \leq x \to \deg (f \circ G) = \deg (f) \cdot N) \leftrightarrow \forall f \in Poly (ℂ) (\deg (f) \leq M \to \deg (f \circ G) = \deg (f) \cdot N))$
25	24	imbi2d	$⊢ x = M \to ((φ \to \forall f \in Poly (ℂ) (\deg (f) \leq x \to \deg (f \circ G) = \deg (f) \cdot N)) \leftrightarrow (φ \to \forall f \in Poly (ℂ) (\deg (f) \leq M \to \deg (f \circ G) = \deg (f) \cdot N)))$
26		dgrcl	$⊢ G \in Poly (S) \to \deg (G) \in ℕ_{0}$
27	4 26	syl	$⊢ φ \to \deg (G) \in ℕ_{0}$
28	2 27	eqeltrid	$⊢ φ \to N \in ℕ_{0}$
29	28	nn0cnd	$⊢ φ \to N \in ℂ$
30	29	adantr	$⊢ (φ \land (f \in Poly (ℂ) \land \deg (f) \leq 0)) \to N \in ℂ$
31	30	mul02d	$⊢ (φ \land (f \in Poly (ℂ) \land \deg (f) \leq 0)) \to 0 \cdot N = 0$
32		simprr	$⊢ (φ \land (f \in Poly (ℂ) \land \deg (f) \leq 0)) \to \deg (f) \leq 0$
33		dgrcl	$⊢ f \in Poly (ℂ) \to \deg (f) \in ℕ_{0}$
34	33	ad2antrl	$⊢ (φ \land (f \in Poly (ℂ) \land \deg (f) \leq 0)) \to \deg (f) \in ℕ_{0}$
35	34	nn0ge0d	$⊢ (φ \land (f \in Poly (ℂ) \land \deg (f) \leq 0)) \to 0 \leq \deg (f)$
36	34	nn0red	$⊢ (φ \land (f \in Poly (ℂ) \land \deg (f) \leq 0)) \to \deg (f) \in ℝ$
37		0re	$⊢ 0 \in ℝ$
38		letri3	$⊢ (\deg (f) \in ℝ \land 0 \in ℝ) \to (\deg (f) = 0 \leftrightarrow (\deg (f) \leq 0 \land 0 \leq \deg (f)))$
39	36 37 38	sylancl	$⊢ (φ \land (f \in Poly (ℂ) \land \deg (f) \leq 0)) \to (\deg (f) = 0 \leftrightarrow (\deg (f) \leq 0 \land 0 \leq \deg (f)))$
40	32 35 39	mpbir2and	$⊢ (φ \land (f \in Poly (ℂ) \land \deg (f) \leq 0)) \to \deg (f) = 0$
41	40	oveq1d	$⊢ (φ \land (f \in Poly (ℂ) \land \deg (f) \leq 0)) \to \deg (f) \cdot N = 0 \cdot N$
42	31 41 40	3eqtr4d	$⊢ (φ \land (f \in Poly (ℂ) \land \deg (f) \leq 0)) \to \deg (f) \cdot N = \deg (f)$
43		fconstmpt	$⊢ ℂ \times \{f (0)\} = (y \in ℂ ⟼ f (0))$
44		0dgrb	$⊢ f \in Poly (ℂ) \to (\deg (f) = 0 \leftrightarrow f = ℂ \times \{f (0)\})$
45	44	ad2antrl	$⊢ (φ \land (f \in Poly (ℂ) \land \deg (f) \leq 0)) \to (\deg (f) = 0 \leftrightarrow f = ℂ \times \{f (0)\})$
46	40 45	mpbid	$⊢ (φ \land (f \in Poly (ℂ) \land \deg (f) \leq 0)) \to f = ℂ \times \{f (0)\}$
47	4	adantr	$⊢ (φ \land (f \in Poly (ℂ) \land \deg (f) \leq 0)) \to G \in Poly (S)$
48		plyf	$⊢ G \in Poly (S) \to G : ℂ ⟶ ℂ$
49	47 48	syl	$⊢ (φ \land (f \in Poly (ℂ) \land \deg (f) \leq 0)) \to G : ℂ ⟶ ℂ$
50	49	ffvelrnda	$⊢ ((φ \land (f \in Poly (ℂ) \land \deg (f) \leq 0)) \land y \in ℂ) \to G (y) \in ℂ$
51	49	feqmptd	$⊢ (φ \land (f \in Poly (ℂ) \land \deg (f) \leq 0)) \to G = (y \in ℂ ⟼ G (y))$
52		fconstmpt	$⊢ ℂ \times \{f (0)\} = (x \in ℂ ⟼ f (0))$
53	46 52	eqtrdi	$⊢ (φ \land (f \in Poly (ℂ) \land \deg (f) \leq 0)) \to f = (x \in ℂ ⟼ f (0))$
54		eqidd	$⊢ x = G (y) \to f (0) = f (0)$
55	50 51 53 54	fmptco	$⊢ (φ \land (f \in Poly (ℂ) \land \deg (f) \leq 0)) \to f \circ G = (y \in ℂ ⟼ f (0))$
56	43 46 55	3eqtr4a	$⊢ (φ \land (f \in Poly (ℂ) \land \deg (f) \leq 0)) \to f = f \circ G$
57	56	fveq2d	$⊢ (φ \land (f \in Poly (ℂ) \land \deg (f) \leq 0)) \to \deg (f) = \deg (f \circ G)$
58	42 57	eqtr2d	$⊢ (φ \land (f \in Poly (ℂ) \land \deg (f) \leq 0)) \to \deg (f \circ G) = \deg (f) \cdot N$
59	58	expr	$⊢ (φ \land f \in Poly (ℂ)) \to (\deg (f) \leq 0 \to \deg (f \circ G) = \deg (f) \cdot N)$
60	59	ralrimiva	$⊢ φ \to \forall f \in Poly (ℂ) (\deg (f) \leq 0 \to \deg (f \circ G) = \deg (f) \cdot N)$
61		fveq2	$⊢ f = g \to \deg (f) = \deg (g)$
62	61	breq1d	$⊢ f = g \to (\deg (f) \leq d \leftrightarrow \deg (g) \leq d)$
63		coeq1	$⊢ f = g \to f \circ G = g \circ G$
64	63	fveq2d	$⊢ f = g \to \deg (f \circ G) = \deg (g \circ G)$
65	61	oveq1d	$⊢ f = g \to \deg (f) \cdot N = \deg (g) \cdot N$
66	64 65	eqeq12d	$⊢ f = g \to (\deg (f \circ G) = \deg (f) \cdot N \leftrightarrow \deg (g \circ G) = \deg (g) \cdot N)$
67	62 66	imbi12d	$⊢ f = g \to ((\deg (f) \leq d \to \deg (f \circ G) = \deg (f) \cdot N) \leftrightarrow (\deg (g) \leq d \to \deg (g \circ G) = \deg (g) \cdot N))$
68	67	cbvralvw	$⊢ \forall f \in Poly (ℂ) (\deg (f) \leq d \to \deg (f \circ G) = \deg (f) \cdot N) \leftrightarrow \forall g \in Poly (ℂ) (\deg (g) \leq d \to \deg (g \circ G) = \deg (g) \cdot N)$
69	33	ad2antrl	$⊢ ((φ \land d \in ℕ_{0}) \land (f \in Poly (ℂ) \land \forall g \in Poly (ℂ) (\deg (g) \leq d \to \deg (g \circ G) = \deg (g) \cdot N))) \to \deg (f) \in ℕ_{0}$
70	69	nn0red	$⊢ ((φ \land d \in ℕ_{0}) \land (f \in Poly (ℂ) \land \forall g \in Poly (ℂ) (\deg (g) \leq d \to \deg (g \circ G) = \deg (g) \cdot N))) \to \deg (f) \in ℝ$
71		nn0p1nn	$⊢ d \in ℕ_{0} \to d + 1 \in ℕ$
72	71	ad2antlr	$⊢ ((φ \land d \in ℕ_{0}) \land (f \in Poly (ℂ) \land \forall g \in Poly (ℂ) (\deg (g) \leq d \to \deg (g \circ G) = \deg (g) \cdot N))) \to d + 1 \in ℕ$
73	72	nnred	$⊢ ((φ \land d \in ℕ_{0}) \land (f \in Poly (ℂ) \land \forall g \in Poly (ℂ) (\deg (g) \leq d \to \deg (g \circ G) = \deg (g) \cdot N))) \to d + 1 \in ℝ$
74	70 73	leloed	$⊢ ((φ \land d \in ℕ_{0}) \land (f \in Poly (ℂ) \land \forall g \in Poly (ℂ) (\deg (g) \leq d \to \deg (g \circ G) = \deg (g) \cdot N))) \to (\deg (f) \leq d + 1 \leftrightarrow (\deg (f) < d + 1 \lor \deg (f) = d + 1))$
75		simplr	$⊢ ((φ \land d \in ℕ_{0}) \land (f \in Poly (ℂ) \land \forall g \in Poly (ℂ) (\deg (g) \leq d \to \deg (g \circ G) = \deg (g) \cdot N))) \to d \in ℕ_{0}$
76		nn0leltp1	$⊢ (\deg (f) \in ℕ_{0} \land d \in ℕ_{0}) \to (\deg (f) \leq d \leftrightarrow \deg (f) < d + 1)$
77	69 75 76	syl2anc	$⊢ ((φ \land d \in ℕ_{0}) \land (f \in Poly (ℂ) \land \forall g \in Poly (ℂ) (\deg (g) \leq d \to \deg (g \circ G) = \deg (g) \cdot N))) \to (\deg (f) \leq d \leftrightarrow \deg (f) < d + 1)$
78		fveq2	$⊢ g = f \to \deg (g) = \deg (f)$
79	78	breq1d	$⊢ g = f \to (\deg (g) \leq d \leftrightarrow \deg (f) \leq d)$
80		coeq1	$⊢ g = f \to g \circ G = f \circ G$
81	80	fveq2d	$⊢ g = f \to \deg (g \circ G) = \deg (f \circ G)$
82	78	oveq1d	$⊢ g = f \to \deg (g) \cdot N = \deg (f) \cdot N$
83	81 82	eqeq12d	$⊢ g = f \to (\deg (g \circ G) = \deg (g) \cdot N \leftrightarrow \deg (f \circ G) = \deg (f) \cdot N)$
84	79 83	imbi12d	$⊢ g = f \to ((\deg (g) \leq d \to \deg (g \circ G) = \deg (g) \cdot N) \leftrightarrow (\deg (f) \leq d \to \deg (f \circ G) = \deg (f) \cdot N))$
85	84	rspcva	$⊢ (f \in Poly (ℂ) \land \forall g \in Poly (ℂ) (\deg (g) \leq d \to \deg (g \circ G) = \deg (g) \cdot N)) \to (\deg (f) \leq d \to \deg (f \circ G) = \deg (f) \cdot N)$
86	85	adantl	$⊢ ((φ \land d \in ℕ_{0}) \land (f \in Poly (ℂ) \land \forall g \in Poly (ℂ) (\deg (g) \leq d \to \deg (g \circ G) = \deg (g) \cdot N))) \to (\deg (f) \leq d \to \deg (f \circ G) = \deg (f) \cdot N)$
87	77 86	sylbird	$⊢ ((φ \land d \in ℕ_{0}) \land (f \in Poly (ℂ) \land \forall g \in Poly (ℂ) (\deg (g) \leq d \to \deg (g \circ G) = \deg (g) \cdot N))) \to (\deg (f) < d + 1 \to \deg (f \circ G) = \deg (f) \cdot N)$
88		eqid	$⊢ \deg (f) = \deg (f)$
89		simprll	$⊢ ((φ \land d \in ℕ_{0}) \land ((f \in Poly (ℂ) \land \forall g \in Poly (ℂ) (\deg (g) \leq d \to \deg (g \circ G) = \deg (g) \cdot N)) \land \deg (f) = d + 1)) \to f \in Poly (ℂ)$
90	5 4	sseldi	$⊢ φ \to G \in Poly (ℂ)$
91	90	ad2antrr	$⊢ ((φ \land d \in ℕ_{0}) \land ((f \in Poly (ℂ) \land \forall g \in Poly (ℂ) (\deg (g) \leq d \to \deg (g \circ G) = \deg (g) \cdot N)) \land \deg (f) = d + 1)) \to G \in Poly (ℂ)$
92		eqid	$⊢ coeff (f) = coeff (f)$
93		simplr	$⊢ ((φ \land d \in ℕ_{0}) \land ((f \in Poly (ℂ) \land \forall g \in Poly (ℂ) (\deg (g) \leq d \to \deg (g \circ G) = \deg (g) \cdot N)) \land \deg (f) = d + 1)) \to d \in ℕ_{0}$
94		simprr	$⊢ ((φ \land d \in ℕ_{0}) \land ((f \in Poly (ℂ) \land \forall g \in Poly (ℂ) (\deg (g) \leq d \to \deg (g \circ G) = \deg (g) \cdot N)) \land \deg (f) = d + 1)) \to \deg (f) = d + 1$
95		simprlr	$⊢ ((φ \land d \in ℕ_{0}) \land ((f \in Poly (ℂ) \land \forall g \in Poly (ℂ) (\deg (g) \leq d \to \deg (g \circ G) = \deg (g) \cdot N)) \land \deg (f) = d + 1)) \to \forall g \in Poly (ℂ) (\deg (g) \leq d \to \deg (g \circ G) = \deg (g) \cdot N)$
96		fveq2	$⊢ g = h \to \deg (g) = \deg (h)$
97	96	breq1d	$⊢ g = h \to (\deg (g) \leq d \leftrightarrow \deg (h) \leq d)$
98		coeq1	$⊢ g = h \to g \circ G = h \circ G$
99	98	fveq2d	$⊢ g = h \to \deg (g \circ G) = \deg (h \circ G)$
100	96	oveq1d	$⊢ g = h \to \deg (g) \cdot N = \deg (h) \cdot N$
101	99 100	eqeq12d	$⊢ g = h \to (\deg (g \circ G) = \deg (g) \cdot N \leftrightarrow \deg (h \circ G) = \deg (h) \cdot N)$
102	97 101	imbi12d	$⊢ g = h \to ((\deg (g) \leq d \to \deg (g \circ G) = \deg (g) \cdot N) \leftrightarrow (\deg (h) \leq d \to \deg (h \circ G) = \deg (h) \cdot N))$
103	102	cbvralvw	$⊢ \forall g \in Poly (ℂ) (\deg (g) \leq d \to \deg (g \circ G) = \deg (g) \cdot N) \leftrightarrow \forall h \in Poly (ℂ) (\deg (h) \leq d \to \deg (h \circ G) = \deg (h) \cdot N)$
104	95 103	sylib	$⊢ ((φ \land d \in ℕ_{0}) \land ((f \in Poly (ℂ) \land \forall g \in Poly (ℂ) (\deg (g) \leq d \to \deg (g \circ G) = \deg (g) \cdot N)) \land \deg (f) = d + 1)) \to \forall h \in Poly (ℂ) (\deg (h) \leq d \to \deg (h \circ G) = \deg (h) \cdot N)$
105	88 2 89 91 92 93 94 104	dgrcolem2	$⊢ ((φ \land d \in ℕ_{0}) \land ((f \in Poly (ℂ) \land \forall g \in Poly (ℂ) (\deg (g) \leq d \to \deg (g \circ G) = \deg (g) \cdot N)) \land \deg (f) = d + 1)) \to \deg (f \circ G) = \deg (f) \cdot N$
106	105	expr	$⊢ ((φ \land d \in ℕ_{0}) \land (f \in Poly (ℂ) \land \forall g \in Poly (ℂ) (\deg (g) \leq d \to \deg (g \circ G) = \deg (g) \cdot N))) \to (\deg (f) = d + 1 \to \deg (f \circ G) = \deg (f) \cdot N)$
107	87 106	jaod	$⊢ ((φ \land d \in ℕ_{0}) \land (f \in Poly (ℂ) \land \forall g \in Poly (ℂ) (\deg (g) \leq d \to \deg (g \circ G) = \deg (g) \cdot N))) \to ((\deg (f) < d + 1 \lor \deg (f) = d + 1) \to \deg (f \circ G) = \deg (f) \cdot N)$
108	74 107	sylbid	$⊢ ((φ \land d \in ℕ_{0}) \land (f \in Poly (ℂ) \land \forall g \in Poly (ℂ) (\deg (g) \leq d \to \deg (g \circ G) = \deg (g) \cdot N))) \to (\deg (f) \leq d + 1 \to \deg (f \circ G) = \deg (f) \cdot N)$
109	108	expr	$⊢ ((φ \land d \in ℕ_{0}) \land f \in Poly (ℂ)) \to (\forall g \in Poly (ℂ) (\deg (g) \leq d \to \deg (g \circ G) = \deg (g) \cdot N) \to (\deg (f) \leq d + 1 \to \deg (f \circ G) = \deg (f) \cdot N))$
110	109	ralrimdva	$⊢ (φ \land d \in ℕ_{0}) \to (\forall g \in Poly (ℂ) (\deg (g) \leq d \to \deg (g \circ G) = \deg (g) \cdot N) \to \forall f \in Poly (ℂ) (\deg (f) \leq d + 1 \to \deg (f \circ G) = \deg (f) \cdot N))$
111	68 110	syl5bi	$⊢ (φ \land d \in ℕ_{0}) \to (\forall f \in Poly (ℂ) (\deg (f) \leq d \to \deg (f \circ G) = \deg (f) \cdot N) \to \forall f \in Poly (ℂ) (\deg (f) \leq d + 1 \to \deg (f \circ G) = \deg (f) \cdot N))$
112	111	expcom	$⊢ d \in ℕ_{0} \to (φ \to (\forall f \in Poly (ℂ) (\deg (f) \leq d \to \deg (f \circ G) = \deg (f) \cdot N) \to \forall f \in Poly (ℂ) (\deg (f) \leq d + 1 \to \deg (f \circ G) = \deg (f) \cdot N)))$
113	112	a2d	$⊢ d \in ℕ_{0} \to ((φ \to \forall f \in Poly (ℂ) (\deg (f) \leq d \to \deg (f \circ G) = \deg (f) \cdot N)) \to (φ \to \forall f \in Poly (ℂ) (\deg (f) \leq d + 1 \to \deg (f \circ G) = \deg (f) \cdot N)))$
114	13 17 21 25 60 113	nn0ind	$⊢ M \in ℕ_{0} \to (φ \to \forall f \in Poly (ℂ) (\deg (f) \leq M \to \deg (f \circ G) = \deg (f) \cdot N))$
115	9 114	mpcom	$⊢ φ \to \forall f \in Poly (ℂ) (\deg (f) \leq M \to \deg (f \circ G) = \deg (f) \cdot N)$
116	9	nn0red	$⊢ φ \to M \in ℝ$
117	116	leidd	$⊢ φ \to M \leq M$
118		fveq2	$⊢ f = F \to \deg (f) = \deg (F)$
119	118 1	eqtr4di	$⊢ f = F \to \deg (f) = M$
120	119	breq1d	$⊢ f = F \to (\deg (f) \leq M \leftrightarrow M \leq M)$
121		coeq1	$⊢ f = F \to f \circ G = F \circ G$
122	121	fveq2d	$⊢ f = F \to \deg (f \circ G) = \deg (F \circ G)$
123	119	oveq1d	$⊢ f = F \to \deg (f) \cdot N = M \cdot N$
124	122 123	eqeq12d	$⊢ f = F \to (\deg (f \circ G) = \deg (f) \cdot N \leftrightarrow \deg (F \circ G) = M \cdot N)$
125	120 124	imbi12d	$⊢ f = F \to ((\deg (f) \leq M \to \deg (f \circ G) = \deg (f) \cdot N) \leftrightarrow (M \leq M \to \deg (F \circ G) = M \cdot N))$
126	125	rspcv	$⊢ F \in Poly (ℂ) \to (\forall f \in Poly (ℂ) (\deg (f) \leq M \to \deg (f \circ G) = \deg (f) \cdot N) \to (M \leq M \to \deg (F \circ G) = M \cdot N))$
127	6 115 117 126	syl3c	$⊢ φ \to \deg (F \circ G) = M \cdot N$

Metamath Proof Explorer

Theorem dgrco

Proof