dgrmulc

Description: Scalar multiplication by a nonzero constant does not change the degree of a function. (Contributed by Mario Carneiro, 24-Jul-2014)

		Ref	Expression
	Assertion	dgrmulc	$⊢ (A \in ℂ \land A \neq 0 \land F \in Poly (S)) \to \deg ((ℂ \times \{A\}) \times_{f} F) = \deg (F)$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$⊢ F = 0_{𝑝} \to (ℂ \times \{A\}) \times_{f} F = (ℂ \times \{A\}) \times_{f} 0_{𝑝}$
2	1	fveq2d	$⊢ F = 0_{𝑝} \to \deg ((ℂ \times \{A\}) \times_{f} F) = \deg ((ℂ \times \{A\}) \times_{f} 0_{𝑝})$
3		fveq2	$⊢ F = 0_{𝑝} \to \deg (F) = \deg (0_{𝑝})$
4		dgr0	$⊢ \deg (0_{𝑝}) = 0$
5	3 4	eqtrdi	$⊢ F = 0_{𝑝} \to \deg (F) = 0$
6	2 5	eqeq12d	$⊢ F = 0_{𝑝} \to (\deg ((ℂ \times \{A\}) \times_{f} F) = \deg (F) \leftrightarrow \deg ((ℂ \times \{A\}) \times_{f} 0_{𝑝}) = 0)$
7		ssid	$⊢ ℂ \subseteq ℂ$
8		simpl1	$⊢ ((A \in ℂ \land A \neq 0 \land F \in Poly (S)) \land F \neq 0_{𝑝}) \to A \in ℂ$
9		plyconst	$⊢ (ℂ \subseteq ℂ \land A \in ℂ) \to ℂ \times \{A\} \in Poly (ℂ)$
10	7 8 9	sylancr	$⊢ ((A \in ℂ \land A \neq 0 \land F \in Poly (S)) \land F \neq 0_{𝑝}) \to ℂ \times \{A\} \in Poly (ℂ)$
11		0cn	$⊢ 0 \in ℂ$
12		fvconst2g	$⊢ (A \in ℂ \land 0 \in ℂ) \to (ℂ \times \{A\}) (0) = A$
13	8 11 12	sylancl	$⊢ ((A \in ℂ \land A \neq 0 \land F \in Poly (S)) \land F \neq 0_{𝑝}) \to (ℂ \times \{A\}) (0) = A$
14		simpl2	$⊢ ((A \in ℂ \land A \neq 0 \land F \in Poly (S)) \land F \neq 0_{𝑝}) \to A \neq 0$
15	13 14	eqnetrd	$⊢ ((A \in ℂ \land A \neq 0 \land F \in Poly (S)) \land F \neq 0_{𝑝}) \to (ℂ \times \{A\}) (0) \neq 0$
16		ne0p	$⊢ (0 \in ℂ \land (ℂ \times \{A\}) (0) \neq 0) \to ℂ \times \{A\} \neq 0_{𝑝}$
17	11 15 16	sylancr	$⊢ ((A \in ℂ \land A \neq 0 \land F \in Poly (S)) \land F \neq 0_{𝑝}) \to ℂ \times \{A\} \neq 0_{𝑝}$
18		plyssc	$⊢ Poly (S) \subseteq Poly (ℂ)$
19		simpl3	$⊢ ((A \in ℂ \land A \neq 0 \land F \in Poly (S)) \land F \neq 0_{𝑝}) \to F \in Poly (S)$
20	18 19	sselid	$⊢ ((A \in ℂ \land A \neq 0 \land F \in Poly (S)) \land F \neq 0_{𝑝}) \to F \in Poly (ℂ)$
21		simpr	$⊢ ((A \in ℂ \land A \neq 0 \land F \in Poly (S)) \land F \neq 0_{𝑝}) \to F \neq 0_{𝑝}$
22		eqid	$⊢ \deg (ℂ \times \{A\}) = \deg (ℂ \times \{A\})$
23		eqid	$⊢ \deg (F) = \deg (F)$
24	22 23	dgrmul	$⊢ ((ℂ \times \{A\} \in Poly (ℂ) \land ℂ \times \{A\} \neq 0_{𝑝}) \land (F \in Poly (ℂ) \land F \neq 0_{𝑝})) \to \deg ((ℂ \times \{A\}) \times_{f} F) = \deg (ℂ \times \{A\}) + \deg (F)$
25	10 17 20 21 24	syl22anc	$⊢ ((A \in ℂ \land A \neq 0 \land F \in Poly (S)) \land F \neq 0_{𝑝}) \to \deg ((ℂ \times \{A\}) \times_{f} F) = \deg (ℂ \times \{A\}) + \deg (F)$
26		0dgr	$⊢ A \in ℂ \to \deg (ℂ \times \{A\}) = 0$
27	8 26	syl	$⊢ ((A \in ℂ \land A \neq 0 \land F \in Poly (S)) \land F \neq 0_{𝑝}) \to \deg (ℂ \times \{A\}) = 0$
28	27	oveq1d	$⊢ ((A \in ℂ \land A \neq 0 \land F \in Poly (S)) \land F \neq 0_{𝑝}) \to \deg (ℂ \times \{A\}) + \deg (F) = 0 + \deg (F)$
29		dgrcl	$⊢ F \in Poly (S) \to \deg (F) \in ℕ_{0}$
30	19 29	syl	$⊢ ((A \in ℂ \land A \neq 0 \land F \in Poly (S)) \land F \neq 0_{𝑝}) \to \deg (F) \in ℕ_{0}$
31	30	nn0cnd	$⊢ ((A \in ℂ \land A \neq 0 \land F \in Poly (S)) \land F \neq 0_{𝑝}) \to \deg (F) \in ℂ$
32	31	addid2d	$⊢ ((A \in ℂ \land A \neq 0 \land F \in Poly (S)) \land F \neq 0_{𝑝}) \to 0 + \deg (F) = \deg (F)$
33	25 28 32	3eqtrd	$⊢ ((A \in ℂ \land A \neq 0 \land F \in Poly (S)) \land F \neq 0_{𝑝}) \to \deg ((ℂ \times \{A\}) \times_{f} F) = \deg (F)$
34		cnex	$⊢ ℂ \in V$
35	34	a1i	$⊢ (A \in ℂ \land A \neq 0 \land F \in Poly (S)) \to ℂ \in V$
36		simp1	$⊢ (A \in ℂ \land A \neq 0 \land F \in Poly (S)) \to A \in ℂ$
37	11	a1i	$⊢ (A \in ℂ \land A \neq 0 \land F \in Poly (S)) \to 0 \in ℂ$
38	35 36 37	ofc12	$⊢ (A \in ℂ \land A \neq 0 \land F \in Poly (S)) \to (ℂ \times \{A\}) \times_{f} (ℂ \times \{0\}) = ℂ \times \{A \cdot 0\}$
39	36	mul01d	$⊢ (A \in ℂ \land A \neq 0 \land F \in Poly (S)) \to A \cdot 0 = 0$
40	39	sneqd	$⊢ (A \in ℂ \land A \neq 0 \land F \in Poly (S)) \to \{A \cdot 0\} = \{0\}$
41	40	xpeq2d	$⊢ (A \in ℂ \land A \neq 0 \land F \in Poly (S)) \to ℂ \times \{A \cdot 0\} = ℂ \times \{0\}$
42	38 41	eqtrd	$⊢ (A \in ℂ \land A \neq 0 \land F \in Poly (S)) \to (ℂ \times \{A\}) \times_{f} (ℂ \times \{0\}) = ℂ \times \{0\}$
43		df-0p	$⊢ 0_{𝑝} = ℂ \times \{0\}$
44	43	oveq2i	$⊢ (ℂ \times \{A\}) \times_{f} 0_{𝑝} = (ℂ \times \{A\}) \times_{f} (ℂ \times \{0\})$
45	42 44 43	3eqtr4g	$⊢ (A \in ℂ \land A \neq 0 \land F \in Poly (S)) \to (ℂ \times \{A\}) \times_{f} 0_{𝑝} = 0_{𝑝}$
46	45	fveq2d	$⊢ (A \in ℂ \land A \neq 0 \land F \in Poly (S)) \to \deg ((ℂ \times \{A\}) \times_{f} 0_{𝑝}) = \deg (0_{𝑝})$
47	46 4	eqtrdi	$⊢ (A \in ℂ \land A \neq 0 \land F \in Poly (S)) \to \deg ((ℂ \times \{A\}) \times_{f} 0_{𝑝}) = 0$
48	6 33 47	pm2.61ne	$⊢ (A \in ℂ \land A \neq 0 \land F \in Poly (S)) \to \deg ((ℂ \times \{A\}) \times_{f} F) = \deg (F)$

Metamath Proof Explorer

Theorem dgrmulc

Proof