This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 · 𝐺 ) ) = ( 𝐷 ‘ 𝐺 ) )