Metamath Proof Explorer

Theorem deg1addle2

Description: If both factors have degree bounded by L , then the sum of the polynomials also has degree bounded by L . (Contributed by Stefan O'Rear, 1-Apr-2015)

Ref Expression
Hypotheses deg1addle.y ⊢ 𝑌 = ( Poly1 ‘ 𝑅 )
deg1addle.d ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
deg1addle.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
deg1addle.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
deg1addle.p ⊢ + = ( +g ‘ 𝑌 )
deg1addle.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
deg1addle.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
deg1addle2.l1 ⊢ ( 𝜑 → 𝐿 ∈ ℝ* )
deg1addle2.l2 ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) ≤ 𝐿 )
deg1addle2.l3 ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) ≤ 𝐿 )
Assertion deg1addle2 ( 𝜑 → ( 𝐷 ‘ ( 𝐹 + 𝐺 ) ) ≤ 𝐿 )

Proof

Step Hyp Ref Expression
1 deg1addle.y ⊢ 𝑌 = ( Poly1 ‘ 𝑅 )
2 deg1addle.d ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
3 deg1addle.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
4 deg1addle.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
5 deg1addle.p ⊢ + = ( +g ‘ 𝑌 )
6 deg1addle.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
7 deg1addle.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
8 deg1addle2.l1 ⊢ ( 𝜑 → 𝐿 ∈ ℝ* )
9 deg1addle2.l2 ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) ≤ 𝐿 )
10 deg1addle2.l3 ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) ≤ 𝐿 )
11 1 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑌 ∈ Ring )
12 3 11 syl ⊢ ( 𝜑 → 𝑌 ∈ Ring )
13 4 5 ringacl ⊢ ( ( 𝑌 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐹 + 𝐺 ) ∈ 𝐵 )
14 12 6 7 13 syl3anc ⊢ ( 𝜑 → ( 𝐹 + 𝐺 ) ∈ 𝐵 )
15 2 1 4 deg1xrcl ⊢ ( ( 𝐹 + 𝐺 ) ∈ 𝐵 → ( 𝐷 ‘ ( 𝐹 + 𝐺 ) ) ∈ ℝ* )
16 14 15 syl ⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 + 𝐺 ) ) ∈ ℝ* )
17 2 1 4 deg1xrcl ⊢ ( 𝐺 ∈ 𝐵 → ( 𝐷 ‘ 𝐺 ) ∈ ℝ* )
18 7 17 syl ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) ∈ ℝ* )
19 2 1 4 deg1xrcl ⊢ ( 𝐹 ∈ 𝐵 → ( 𝐷 ‘ 𝐹 ) ∈ ℝ* )
20 6 19 syl ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) ∈ ℝ* )
21 18 20 ifcld ⊢ ( 𝜑 → if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) ∈ ℝ* )
22 1 2 3 4 5 6 7 deg1addle ⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 + 𝐺 ) ) ≤ if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) )
23 xrmaxle ⊢ ( ( ( 𝐷 ‘ 𝐹 ) ∈ ℝ* ∧ ( 𝐷 ‘ 𝐺 ) ∈ ℝ* ∧ 𝐿 ∈ ℝ* ) → ( if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) ≤ 𝐿 ↔ ( ( 𝐷 ‘ 𝐹 ) ≤ 𝐿 ∧ ( 𝐷 ‘ 𝐺 ) ≤ 𝐿 ) ) )
24 20 18 8 23 syl3anc ⊢ ( 𝜑 → ( if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) ≤ 𝐿 ↔ ( ( 𝐷 ‘ 𝐹 ) ≤ 𝐿 ∧ ( 𝐷 ‘ 𝐺 ) ≤ 𝐿 ) ) )
25 9 10 24 mpbir2and ⊢ ( 𝜑 → if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) ≤ 𝐿 )
26 16 21 8 22 25 xrletrd ⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 + 𝐺 ) ) ≤ 𝐿 )