mdegvscale

Description: The degree of a scalar multiple of a polynomial is at most the degree of the original polynomial. (Contributed by Stefan O'Rear, 26-Mar-2015)

	Ref	Expression
Hypotheses	mdegaddle.y	$⊢ Y = I mPoly R$
	mdegaddle.d	$⊢ D = I mDeg R$
	mdegaddle.i	$⊢ φ \to I \in V$
	mdegaddle.r	$⊢ φ \to R \in Ring$
	mdegvscale.b	$⊢ B = {Base}_{Y}$
	mdegvscale.k	$⊢ K = {Base}_{R}$
	mdegvscale.p	$⊢ \underset{˙}{\cdot} = \cdot_{Y}$
	mdegvscale.f	$⊢ φ \to F \in K$
	mdegvscale.g	$⊢ φ \to G \in B$
Assertion	mdegvscale	$⊢ φ \to D (F \underset{˙}{\cdot} G) \leq D (G)$

Proof

Step	Hyp	Ref	Expression
1		mdegaddle.y	$⊢ Y = I mPoly R$
2		mdegaddle.d	$⊢ D = I mDeg R$
3		mdegaddle.i	$⊢ φ \to I \in V$
4		mdegaddle.r	$⊢ φ \to R \in Ring$
5		mdegvscale.b	$⊢ B = {Base}_{Y}$
6		mdegvscale.k	$⊢ K = {Base}_{R}$
7		mdegvscale.p	$⊢ \underset{˙}{\cdot} = \cdot_{Y}$
8		mdegvscale.f	$⊢ φ \to F \in K$
9		mdegvscale.g	$⊢ φ \to G \in B$
10		eqid	$⊢ \cdot_{R} = \cdot_{R}$
11		eqid	$⊢ \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} = \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\}$
12	8	adantr	$⊢ (φ \land x \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\}) \to F \in K$
13	9	adantr	$⊢ (φ \land x \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\}) \to G \in B$
14		simpr	$⊢ (φ \land x \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\}) \to x \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\}$
15	1 7 6 5 10 11 12 13 14	mplvscaval	$⊢ (φ \land x \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\}) \to (F \underset{˙}{\cdot} G) (x) = F \cdot_{R} G (x)$
16	15	adantrr	$⊢ (φ \land (x \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} \land D (G) < (b \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} ⟼ \sum_{ℂ_{fld}} b) (x))) \to (F \underset{˙}{\cdot} G) (x) = F \cdot_{R} G (x)$
17		eqid	$⊢ 0_{R} = 0_{R}$
18		eqid	$⊢ (b \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} ⟼ \sum_{ℂ_{fld}} b) = (b \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} ⟼ \sum_{ℂ_{fld}} b)$
19	9	adantr	$⊢ (φ \land (x \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} \land D (G) < (b \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} ⟼ \sum_{ℂ_{fld}} b) (x))) \to G \in B$
20		simprl	$⊢ (φ \land (x \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} \land D (G) < (b \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} ⟼ \sum_{ℂ_{fld}} b) (x))) \to x \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\}$
21		simprr	$⊢ (φ \land (x \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} \land D (G) < (b \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} ⟼ \sum_{ℂ_{fld}} b) (x))) \to D (G) < (b \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} ⟼ \sum_{ℂ_{fld}} b) (x)$
22	2 1 5 17 11 18 19 20 21	mdeglt	$⊢ (φ \land (x \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} \land D (G) < (b \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} ⟼ \sum_{ℂ_{fld}} b) (x))) \to G (x) = 0_{R}$
23	22	oveq2d	$⊢ (φ \land (x \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} \land D (G) < (b \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} ⟼ \sum_{ℂ_{fld}} b) (x))) \to F \cdot_{R} G (x) = F \cdot_{R} 0_{R}$
24	6 10 17	ringrz	$⊢ (R \in Ring \land F \in K) \to F \cdot_{R} 0_{R} = 0_{R}$
25	4 8 24	syl2anc	$⊢ φ \to F \cdot_{R} 0_{R} = 0_{R}$
26	25	adantr	$⊢ (φ \land (x \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} \land D (G) < (b \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} ⟼ \sum_{ℂ_{fld}} b) (x))) \to F \cdot_{R} 0_{R} = 0_{R}$
27	16 23 26	3eqtrd	$⊢ (φ \land (x \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} \land D (G) < (b \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} ⟼ \sum_{ℂ_{fld}} b) (x))) \to (F \underset{˙}{\cdot} G) (x) = 0_{R}$
28	27	expr	$⊢ (φ \land x \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\}) \to (D (G) < (b \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} ⟼ \sum_{ℂ_{fld}} b) (x) \to (F \underset{˙}{\cdot} G) (x) = 0_{R})$
29	28	ralrimiva	$⊢ φ \to \forall x \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} (D (G) < (b \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} ⟼ \sum_{ℂ_{fld}} b) (x) \to (F \underset{˙}{\cdot} G) (x) = 0_{R})$
30	1	mpllmod	$⊢ (I \in V \land R \in Ring) \to Y \in LMod$
31	3 4 30	syl2anc	$⊢ φ \to Y \in LMod$
32	1 3 4	mplsca	$⊢ φ \to R = Scalar (Y)$
33	32	fveq2d	$⊢ φ \to {Base}_{R} = {Base}_{Scalar (Y)}$
34	6 33	eqtrid	$⊢ φ \to K = {Base}_{Scalar (Y)}$
35	8 34	eleqtrd	$⊢ φ \to F \in {Base}_{Scalar (Y)}$
36		eqid	$⊢ Scalar (Y) = Scalar (Y)$
37		eqid	$⊢ {Base}_{Scalar (Y)} = {Base}_{Scalar (Y)}$
38	5 36 7 37	lmodvscl	$⊢ (Y \in LMod \land F \in {Base}_{Scalar (Y)} \land G \in B) \to F \underset{˙}{\cdot} G \in B$
39	31 35 9 38	syl3anc	$⊢ φ \to F \underset{˙}{\cdot} G \in B$
40	2 1 5	mdegxrcl	$⊢ G \in B \to D (G) \in ℝ^{*}$
41	9 40	syl	$⊢ φ \to D (G) \in ℝ^{*}$
42	2 1 5 17 11 18	mdegleb	$⊢ (F \underset{˙}{\cdot} G \in B \land D (G) \in ℝ^{*}) \to (D (F \underset{˙}{\cdot} G) \leq D (G) \leftrightarrow \forall x \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} (D (G) < (b \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} ⟼ \sum_{ℂ_{fld}} b) (x) \to (F \underset{˙}{\cdot} G) (x) = 0_{R}))$
43	39 41 42	syl2anc	$⊢ φ \to (D (F \underset{˙}{\cdot} G) \leq D (G) \leftrightarrow \forall x \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} (D (G) < (b \in \{a \in ({ℕ_{0}}^{I}) \| a^{-1} [ℕ] \in Fin\} ⟼ \sum_{ℂ_{fld}} b) (x) \to (F \underset{˙}{\cdot} G) (x) = 0_{R}))$
44	29 43	mpbird	$⊢ φ \to D (F \underset{˙}{\cdot} G) \leq D (G)$

Metamath Proof Explorer

Theorem mdegvscale

Proof