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	⊢ 𝑌 = ( 𝐼 mPoly 𝑅 )
	mdegaddle.d	⊢ 𝐷 = ( 𝐼 mDeg 𝑅 )
	mdegaddle.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	mdegaddle.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	mdegvscale.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
	mdegvscale.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	mdegvscale.p	⊢ · = ( ·𝑠 ‘ 𝑌 )
	mdegvscale.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐾 )
	mdegvscale.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
Assertion	mdegvscale	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 · 𝐺 ) ) ≤ ( 𝐷 ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		mdegaddle.y	⊢ 𝑌 = ( 𝐼 mPoly 𝑅 )
2		mdegaddle.d	⊢ 𝐷 = ( 𝐼 mDeg 𝑅 )
3		mdegaddle.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
4		mdegaddle.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
5		mdegvscale.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
6		mdegvscale.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
7		mdegvscale.p	⊢ · = ( ·𝑠 ‘ 𝑌 )
8		mdegvscale.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐾 )
9		mdegvscale.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
10		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
11		eqid	⊢ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } = { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin }
12	8	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) → 𝐹 ∈ 𝐾 )
13	9	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) → 𝐺 ∈ 𝐵 )
14		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) → 𝑥 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } )
15	1 7 6 5 10 11 12 13 14	mplvscaval	⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) → ( ( 𝐹 · 𝐺 ) ‘ 𝑥 ) = ( 𝐹 ( .r ‘ 𝑅 ) ( 𝐺 ‘ 𝑥 ) ) )
16	15	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∧ ( 𝐷 ‘ 𝐺 ) < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑥 ) ) ) → ( ( 𝐹 · 𝐺 ) ‘ 𝑥 ) = ( 𝐹 ( .r ‘ 𝑅 ) ( 𝐺 ‘ 𝑥 ) ) )
17		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
18		eqid	⊢ ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) = ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) )
19	9	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∧ ( 𝐷 ‘ 𝐺 ) < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑥 ) ) ) → 𝐺 ∈ 𝐵 )
20		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∧ ( 𝐷 ‘ 𝐺 ) < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑥 ) ) ) → 𝑥 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } )
21		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∧ ( 𝐷 ‘ 𝐺 ) < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑥 ) ) ) → ( 𝐷 ‘ 𝐺 ) < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑥 ) )
22	2 1 5 17 11 18 19 20 21	mdeglt	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∧ ( 𝐷 ‘ 𝐺 ) < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑥 ) ) ) → ( 𝐺 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) )
23	22	oveq2d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∧ ( 𝐷 ‘ 𝐺 ) < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑥 ) ) ) → ( 𝐹 ( .r ‘ 𝑅 ) ( 𝐺 ‘ 𝑥 ) ) = ( 𝐹 ( .r ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) )
24	6 10 17	ringrz	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ) → ( 𝐹 ( .r ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
25	4 8 24	syl2anc	⊢ ( 𝜑 → ( 𝐹 ( .r ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
26	25	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∧ ( 𝐷 ‘ 𝐺 ) < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑥 ) ) ) → ( 𝐹 ( .r ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
27	16 23 26	3eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∧ ( 𝐷 ‘ 𝐺 ) < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑥 ) ) ) → ( ( 𝐹 · 𝐺 ) ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) )
28	27	expr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) → ( ( 𝐷 ‘ 𝐺 ) < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑥 ) → ( ( 𝐹 · 𝐺 ) ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) )
29	28	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ( ( 𝐷 ‘ 𝐺 ) < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑥 ) → ( ( 𝐹 · 𝐺 ) ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) )
30	1	mpllmod	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) → 𝑌 ∈ LMod )
31	3 4 30	syl2anc	⊢ ( 𝜑 → 𝑌 ∈ LMod )
32	1 3 4	mplsca	⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑌 ) )
33	32	fveq2d	⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑌 ) ) )
34	6 33	syl5eq	⊢ ( 𝜑 → 𝐾 = ( Base ‘ ( Scalar ‘ 𝑌 ) ) )
35	8 34	eleqtrd	⊢ ( 𝜑 → 𝐹 ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) )
36		eqid	⊢ ( Scalar ‘ 𝑌 ) = ( Scalar ‘ 𝑌 )
37		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑌 ) ) = ( Base ‘ ( Scalar ‘ 𝑌 ) )
38	5 36 7 37	lmodvscl	⊢ ( ( 𝑌 ∈ LMod ∧ 𝐹 ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ∧ 𝐺 ∈ 𝐵 ) → ( 𝐹 · 𝐺 ) ∈ 𝐵 )
39	31 35 9 38	syl3anc	⊢ ( 𝜑 → ( 𝐹 · 𝐺 ) ∈ 𝐵 )
40	2 1 5	mdegxrcl	⊢ ( 𝐺 ∈ 𝐵 → ( 𝐷 ‘ 𝐺 ) ∈ ℝ* )
41	9 40	syl	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) ∈ ℝ* )
42	2 1 5 17 11 18	mdegleb	⊢ ( ( ( 𝐹 · 𝐺 ) ∈ 𝐵 ∧ ( 𝐷 ‘ 𝐺 ) ∈ ℝ* ) → ( ( 𝐷 ‘ ( 𝐹 · 𝐺 ) ) ≤ ( 𝐷 ‘ 𝐺 ) ↔ ∀ 𝑥 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ( ( 𝐷 ‘ 𝐺 ) < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑥 ) → ( ( 𝐹 · 𝐺 ) ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) )
43	39 41 42	syl2anc	⊢ ( 𝜑 → ( ( 𝐷 ‘ ( 𝐹 · 𝐺 ) ) ≤ ( 𝐷 ‘ 𝐺 ) ↔ ∀ 𝑥 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ( ( 𝐷 ‘ 𝐺 ) < ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) ‘ 𝑥 ) → ( ( 𝐹 · 𝐺 ) ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) )
44	29 43	mpbird	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 · 𝐺 ) ) ≤ ( 𝐷 ‘ 𝐺 ) )