Metamath Proof Explorer

Theorem dgrsub

Description: The degree of a difference of polynomials is at most the maximum of the degrees. (Contributed by Mario Carneiro, 26-Jul-2014)

Ref Expression
Hypotheses dgrsub.1 ⊢ 𝑀 = ( deg ‘ 𝐹 )
dgrsub.2 ⊢ 𝑁 = ( deg ‘ 𝐺 )
Assertion dgrsub ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( deg ‘ ( 𝐹 ∘f − 𝐺 ) ) ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) )

Proof

Step Hyp Ref Expression
1 dgrsub.1 ⊢ 𝑀 = ( deg ‘ 𝐹 )
2 dgrsub.2 ⊢ 𝑁 = ( deg ‘ 𝐺 )
3 plyssc ⊢ ( Poly ‘ 𝑆 ) ⊆ ( Poly ‘ ℂ )
4 3 sseli ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 ∈ ( Poly ‘ ℂ ) )
5 ssid ⊢ ℂ ⊆ ℂ
6 neg1cn ⊢ - 1 ∈ ℂ
7 plyconst ⊢ ( ( ℂ ⊆ ℂ ∧ - 1 ∈ ℂ ) → ( ℂ × { - 1 } ) ∈ ( Poly ‘ ℂ ) )
8 5 6 7 mp2an ⊢ ( ℂ × { - 1 } ) ∈ ( Poly ‘ ℂ )
9 3 sseli ⊢ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → 𝐺 ∈ ( Poly ‘ ℂ ) )
10 plymulcl ⊢ ( ( ( ℂ × { - 1 } ) ∈ ( Poly ‘ ℂ ) ∧ 𝐺 ∈ ( Poly ‘ ℂ ) ) → ( ( ℂ × { - 1 } ) ∘f · 𝐺 ) ∈ ( Poly ‘ ℂ ) )
11 8 9 10 sylancr ⊢ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → ( ( ℂ × { - 1 } ) ∘f · 𝐺 ) ∈ ( Poly ‘ ℂ ) )
12 eqid ⊢ ( deg ‘ ( ( ℂ × { - 1 } ) ∘f · 𝐺 ) ) = ( deg ‘ ( ( ℂ × { - 1 } ) ∘f · 𝐺 ) )
13 1 12 dgradd ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℂ ) ∧ ( ( ℂ × { - 1 } ) ∘f · 𝐺 ) ∈ ( Poly ‘ ℂ ) ) → ( deg ‘ ( 𝐹 ∘f + ( ( ℂ × { - 1 } ) ∘f · 𝐺 ) ) ) ≤ if ( 𝑀 ≤ ( deg ‘ ( ( ℂ × { - 1 } ) ∘f · 𝐺 ) ) , ( deg ‘ ( ( ℂ × { - 1 } ) ∘f · 𝐺 ) ) , 𝑀 ) )
14 4 11 13 syl2an ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( deg ‘ ( 𝐹 ∘f + ( ( ℂ × { - 1 } ) ∘f · 𝐺 ) ) ) ≤ if ( 𝑀 ≤ ( deg ‘ ( ( ℂ × { - 1 } ) ∘f · 𝐺 ) ) , ( deg ‘ ( ( ℂ × { - 1 } ) ∘f · 𝐺 ) ) , 𝑀 ) )
15 cnex ⊢ ℂ ∈ V
16 plyf ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 : ℂ ⟶ ℂ )
17 plyf ⊢ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → 𝐺 : ℂ ⟶ ℂ )
18 ofnegsub ⊢ ( ( ℂ ∈ V ∧ 𝐹 : ℂ ⟶ ℂ ∧ 𝐺 : ℂ ⟶ ℂ ) → ( 𝐹 ∘f + ( ( ℂ × { - 1 } ) ∘f · 𝐺 ) ) = ( 𝐹 ∘f − 𝐺 ) )
19 15 16 17 18 mp3an3an ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( 𝐹 ∘f + ( ( ℂ × { - 1 } ) ∘f · 𝐺 ) ) = ( 𝐹 ∘f − 𝐺 ) )
20 19 fveq2d ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( deg ‘ ( 𝐹 ∘f + ( ( ℂ × { - 1 } ) ∘f · 𝐺 ) ) ) = ( deg ‘ ( 𝐹 ∘f − 𝐺 ) ) )
21 neg1ne0 ⊢ - 1 ≠ 0
22 dgrmulc ⊢ ( ( - 1 ∈ ℂ ∧ - 1 ≠ 0 ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( deg ‘ ( ( ℂ × { - 1 } ) ∘f · 𝐺 ) ) = ( deg ‘ 𝐺 ) )
23 6 21 22 mp3an12 ⊢ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → ( deg ‘ ( ( ℂ × { - 1 } ) ∘f · 𝐺 ) ) = ( deg ‘ 𝐺 ) )
24 23 2 eqtr4di ⊢ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → ( deg ‘ ( ( ℂ × { - 1 } ) ∘f · 𝐺 ) ) = 𝑁 )
25 24 adantl ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( deg ‘ ( ( ℂ × { - 1 } ) ∘f · 𝐺 ) ) = 𝑁 )
26 25 breq2d ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( 𝑀 ≤ ( deg ‘ ( ( ℂ × { - 1 } ) ∘f · 𝐺 ) ) ↔ 𝑀 ≤ 𝑁 ) )
27 26 25 ifbieq1d ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → if ( 𝑀 ≤ ( deg ‘ ( ( ℂ × { - 1 } ) ∘f · 𝐺 ) ) , ( deg ‘ ( ( ℂ × { - 1 } ) ∘f · 𝐺 ) ) , 𝑀 ) = if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) )
28 14 20 27 3brtr3d ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( deg ‘ ( 𝐹 ∘f − 𝐺 ) ) ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) )