Theorem mdegvsca

Description: The degree of a scalar multiple of a polynomial is exactly the degree of the original polynomial when the multiple is a nonzero-divisor. (Contributed by Stefan O'Rear, 28-Mar-2015) (Proof shortened by AV, 27-Jul-2019)

	Ref	Expression
Hypotheses	mdegaddle.y	⊢ 𝑌 = ( 𝐼 mPoly 𝑅 )
	mdegaddle.d	⊢ 𝐷 = ( 𝐼 mDeg 𝑅 )
	mdegaddle.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	mdegaddle.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	mdegvsca.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
	mdegvsca.e	⊢ 𝐸 = ( RLReg ‘ 𝑅 )
	mdegvsca.p	⊢ · = ( ·𝑠 ‘ 𝑌 )
	mdegvsca.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐸 )
	mdegvsca.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
Assertion	mdegvsca	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 · 𝐺 ) ) = ( 𝐷 ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		mdegaddle.y	⊢ 𝑌 = ( 𝐼 mPoly 𝑅 )
2		mdegaddle.d	⊢ 𝐷 = ( 𝐼 mDeg 𝑅 )
3		mdegaddle.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
4		mdegaddle.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
5		mdegvsca.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
6		mdegvsca.e	⊢ 𝐸 = ( RLReg ‘ 𝑅 )
7		mdegvsca.p	⊢ · = ( ·𝑠 ‘ 𝑌 )
8		mdegvsca.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐸 )
9		mdegvsca.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
10		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
11		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
12		eqid	⊢ { 𝑥 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑥 “ ℕ ) ∈ Fin } = { 𝑥 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑥 “ ℕ ) ∈ Fin }
13	6 10	rrgss	⊢ 𝐸 ⊆ ( Base ‘ 𝑅 )
14	13 8	sselid	⊢ ( 𝜑 → 𝐹 ∈ ( Base ‘ 𝑅 ) )
15	1 7 10 5 11 12 14 9	mplvsca	⊢ ( 𝜑 → ( 𝐹 · 𝐺 ) = ( ( { 𝑥 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑥 “ ℕ ) ∈ Fin } × { 𝐹 } ) ∘f ( .r ‘ 𝑅 ) 𝐺 ) )
16	15	oveq1d	⊢ ( 𝜑 → ( ( 𝐹 · 𝐺 ) supp ( 0g ‘ 𝑅 ) ) = ( ( ( { 𝑥 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑥 “ ℕ ) ∈ Fin } × { 𝐹 } ) ∘f ( .r ‘ 𝑅 ) 𝐺 ) supp ( 0g ‘ 𝑅 ) ) )
17		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
18		ovex	⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
19	18	rabex	⊢ { 𝑥 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑥 “ ℕ ) ∈ Fin } ∈ V
20	19	a1i	⊢ ( 𝜑 → { 𝑥 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑥 “ ℕ ) ∈ Fin } ∈ V )
21	1 10 5 12 9	mplelf	⊢ ( 𝜑 → 𝐺 : { 𝑥 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑥 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
22	6 10 11 17 20 4 8 21	rrgsupp	⊢ ( 𝜑 → ( ( ( { 𝑥 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑥 “ ℕ ) ∈ Fin } × { 𝐹 } ) ∘f ( .r ‘ 𝑅 ) 𝐺 ) supp ( 0g ‘ 𝑅 ) ) = ( 𝐺 supp ( 0g ‘ 𝑅 ) ) )
23	16 22	eqtrd	⊢ ( 𝜑 → ( ( 𝐹 · 𝐺 ) supp ( 0g ‘ 𝑅 ) ) = ( 𝐺 supp ( 0g ‘ 𝑅 ) ) )
24	23	imaeq2d	⊢ ( 𝜑 → ( ( 𝑦 ∈ { 𝑥 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑥 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑦 ) ) “ ( ( 𝐹 · 𝐺 ) supp ( 0g ‘ 𝑅 ) ) ) = ( ( 𝑦 ∈ { 𝑥 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑥 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑦 ) ) “ ( 𝐺 supp ( 0g ‘ 𝑅 ) ) ) )
25	24	supeq1d	⊢ ( 𝜑 → sup ( ( ( 𝑦 ∈ { 𝑥 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑥 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑦 ) ) “ ( ( 𝐹 · 𝐺 ) supp ( 0g ‘ 𝑅 ) ) ) , ℝ* , < ) = sup ( ( ( 𝑦 ∈ { 𝑥 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑥 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑦 ) ) “ ( 𝐺 supp ( 0g ‘ 𝑅 ) ) ) , ℝ* , < ) )
26	1 3 4	mpllmodd	⊢ ( 𝜑 → 𝑌 ∈ LMod )
27	1 3 4	mplsca	⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑌 ) )
28	27	fveq2d	⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑌 ) ) )
29	14 28	eleqtrd	⊢ ( 𝜑 → 𝐹 ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) )
30		eqid	⊢ ( Scalar ‘ 𝑌 ) = ( Scalar ‘ 𝑌 )
31		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑌 ) ) = ( Base ‘ ( Scalar ‘ 𝑌 ) )
32	5 30 7 31	lmodvscl	⊢ ( ( 𝑌 ∈ LMod ∧ 𝐹 ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ∧ 𝐺 ∈ 𝐵 ) → ( 𝐹 · 𝐺 ) ∈ 𝐵 )
33	26 29 9 32	syl3anc	⊢ ( 𝜑 → ( 𝐹 · 𝐺 ) ∈ 𝐵 )
34		eqid	⊢ ( 𝑦 ∈ { 𝑥 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑥 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑦 ) ) = ( 𝑦 ∈ { 𝑥 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑥 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑦 ) )
35	2 1 5 17 12 34	mdegval	⊢ ( ( 𝐹 · 𝐺 ) ∈ 𝐵 → ( 𝐷 ‘ ( 𝐹 · 𝐺 ) ) = sup ( ( ( 𝑦 ∈ { 𝑥 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑥 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑦 ) ) “ ( ( 𝐹 · 𝐺 ) supp ( 0g ‘ 𝑅 ) ) ) , ℝ* , < ) )
36	33 35	syl	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 · 𝐺 ) ) = sup ( ( ( 𝑦 ∈ { 𝑥 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑥 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑦 ) ) “ ( ( 𝐹 · 𝐺 ) supp ( 0g ‘ 𝑅 ) ) ) , ℝ* , < ) )
37	2 1 5 17 12 34	mdegval	⊢ ( 𝐺 ∈ 𝐵 → ( 𝐷 ‘ 𝐺 ) = sup ( ( ( 𝑦 ∈ { 𝑥 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑥 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑦 ) ) “ ( 𝐺 supp ( 0g ‘ 𝑅 ) ) ) , ℝ* , < ) )
38	9 37	syl	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) = sup ( ( ( 𝑦 ∈ { 𝑥 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑥 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑦 ) ) “ ( 𝐺 supp ( 0g ‘ 𝑅 ) ) ) , ℝ* , < ) )
39	25 36 38	3eqtr4d	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 · 𝐺 ) ) = ( 𝐷 ‘ 𝐺 ) )