Metamath Proof Explorer

Theorem 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 ⊢ φ → I ∈ V
mdegaddle.r ⊢ φ → R ∈ Ring
mdegvscale.b ⊢ B = Base Y
mdegvscale.k ⊢ K = Base R
mdegvscale.p ⊢ · ˙ = ⋅ Y
mdegvscale.f ⊢ φ → F ∈ K
mdegvscale.g ⊢ φ → G ∈ B
Assertion mdegvscale ⊢ φ → D ⁡ F · ˙ G ≤ D ⁡ G

Proof

Step Hyp Ref Expression
1 mdegaddle.y ⊢ Y = I mPoly R
2 mdegaddle.d ⊢ D = I mDeg R
3 mdegaddle.i ⊢ φ → I ∈ V
4 mdegaddle.r ⊢ φ → R ∈ Ring
5 mdegvscale.b ⊢ B = Base Y
6 mdegvscale.k ⊢ K = Base R
7 mdegvscale.p ⊢ · ˙ = ⋅ Y
8 mdegvscale.f ⊢ φ → F ∈ K
9 mdegvscale.g ⊢ φ → G ∈ B
10 eqid ⊢ ⋅ R = ⋅ R
11 eqid ⊢ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin = a ∈ ℕ 0 I | a -1 ℕ ∈ Fin
12 8 adantr ⊢ φ ∧ x ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin → F ∈ K
13 9 adantr ⊢ φ ∧ x ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin → G ∈ B
14 simpr ⊢ φ ∧ x ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin → x ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin
15 1 7 6 5 10 11 12 13 14 mplvscaval ⊢ φ ∧ x ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin → F · ˙ G ⁡ x = F ⋅ R G ⁡ x
16 15 adantrr ⊢ φ ∧ x ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ∧ D ⁡ G < b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b ⁡ x → F · ˙ G ⁡ x = F ⋅ R G ⁡ x
17 eqid ⊢ 0 R = 0 R
18 eqid ⊢ b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b = b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b
19 9 adantr ⊢ φ ∧ x ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ∧ D ⁡ G < b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b ⁡ x → G ∈ B
20 simprl ⊢ φ ∧ x ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ∧ D ⁡ G < b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b ⁡ x → x ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin
21 simprr ⊢ φ ∧ x ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ∧ D ⁡ G < b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b ⁡ x → D ⁡ G < b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b ⁡ x
22 2 1 5 17 11 18 19 20 21 mdeglt ⊢ φ ∧ x ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ∧ D ⁡ G < b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b ⁡ x → G ⁡ x = 0 R
23 22 oveq2d ⊢ φ ∧ x ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ∧ D ⁡ G < b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b ⁡ x → F ⋅ R G ⁡ x = F ⋅ R 0 R
24 6 10 17 ringrz ⊢ R ∈ Ring ∧ F ∈ K → F ⋅ R 0 R = 0 R
25 4 8 24 syl2anc ⊢ φ → F ⋅ R 0 R = 0 R
26 25 adantr ⊢ φ ∧ x ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ∧ D ⁡ G < b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b ⁡ x → F ⋅ R 0 R = 0 R
27 16 23 26 3eqtrd ⊢ φ ∧ x ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ∧ D ⁡ G < b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b ⁡ x → F · ˙ G ⁡ x = 0 R
28 27 expr ⊢ φ ∧ x ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin → D ⁡ G < b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b ⁡ x → F · ˙ G ⁡ x = 0 R
29 28 ralrimiva ⊢ φ → ∀ x ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin D ⁡ G < b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b ⁡ x → F · ˙ G ⁡ x = 0 R
30 1 mpllmod ⊢ I ∈ V ∧ R ∈ Ring → Y ∈ LMod
31 3 4 30 syl2anc ⊢ φ → Y ∈ LMod
32 1 3 4 mplsca ⊢ φ → R = Scalar ⁡ Y
33 32 fveq2d ⊢ φ → Base R = Base Scalar ⁡ Y
34 6 33 eqtrid ⊢ φ → K = Base Scalar ⁡ Y
35 8 34 eleqtrd ⊢ φ → F ∈ Base Scalar ⁡ Y
36 eqid ⊢ Scalar ⁡ Y = Scalar ⁡ Y
37 eqid ⊢ Base Scalar ⁡ Y = Base Scalar ⁡ Y
38 5 36 7 37 lmodvscl ⊢ Y ∈ LMod ∧ F ∈ Base Scalar ⁡ Y ∧ G ∈ B → F · ˙ G ∈ B
39 31 35 9 38 syl3anc ⊢ φ → F · ˙ G ∈ B
40 2 1 5 mdegxrcl ⊢ G ∈ B → D ⁡ G ∈ ℝ *
41 9 40 syl ⊢ φ → D ⁡ G ∈ ℝ *
42 2 1 5 17 11 18 mdegleb ⊢ F · ˙ G ∈ B ∧ D ⁡ G ∈ ℝ * → D ⁡ F · ˙ G ≤ D ⁡ G ↔ ∀ x ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin D ⁡ G < b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b ⁡ x → F · ˙ G ⁡ x = 0 R
43 39 41 42 syl2anc ⊢ φ → D ⁡ F · ˙ G ≤ D ⁡ G ↔ ∀ x ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin D ⁡ G < b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b ⁡ x → F · ˙ G ⁡ x = 0 R
44 29 43 mpbird ⊢ φ → D ⁡ F · ˙ G ≤ D ⁡ G