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

Metamath Proof Explorer

Theorem deg1mul2

Description: Degree of multiplication of two nonzero polynomials when the first leads with a nonzero-divisor coefficient. (Contributed by Stefan O'Rear, 26-Mar-2015)

Ref Expression
Hypotheses deg1mul2.d ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
deg1mul2.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
deg1mul2.e ⊢ 𝐸 = ( RLReg ‘ 𝑅 )
deg1mul2.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
deg1mul2.t ⊢ · = ( .r ‘ 𝑃 )
deg1mul2.z ⊢ 0 = ( 0g ‘ 𝑃 )
deg1mul2.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
deg1mul2.fb ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
deg1mul2.fz ⊢ ( 𝜑 → 𝐹 ≠ 0 )
deg1mul2.fc ⊢ ( 𝜑 → ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) ∈ 𝐸 )
deg1mul2.gb ⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
deg1mul2.gz ⊢ ( 𝜑 → 𝐺 ≠ 0 )
Assertion deg1mul2 ( 𝜑 → ( 𝐷 ‘ ( 𝐹 · 𝐺 ) ) = ( ( 𝐷 ‘ 𝐹 ) + ( 𝐷 ‘ 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 deg1mul2.d ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
2 deg1mul2.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
3 deg1mul2.e ⊢ 𝐸 = ( RLReg ‘ 𝑅 )
4 deg1mul2.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
5 deg1mul2.t ⊢ · = ( .r ‘ 𝑃 )
6 deg1mul2.z ⊢ 0 = ( 0g ‘ 𝑃 )
7 deg1mul2.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
8 deg1mul2.fb ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
9 deg1mul2.fz ⊢ ( 𝜑 → 𝐹 ≠ 0 )
10 deg1mul2.fc ⊢ ( 𝜑 → ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) ∈ 𝐸 )
11 deg1mul2.gb ⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
12 deg1mul2.gz ⊢ ( 𝜑 → 𝐺 ≠ 0 )
13 2 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
14 7 13 syl ⊢ ( 𝜑 → 𝑃 ∈ Ring )
15 4 5 ringcl ⊢ ( ( 𝑃 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐹 · 𝐺 ) ∈ 𝐵 )
16 14 8 11 15 syl3anc ⊢ ( 𝜑 → ( 𝐹 · 𝐺 ) ∈ 𝐵 )
17 1 2 4 deg1xrcl ⊢ ( ( 𝐹 · 𝐺 ) ∈ 𝐵 → ( 𝐷 ‘ ( 𝐹 · 𝐺 ) ) ∈ ℝ* )
18 16 17 syl ⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 · 𝐺 ) ) ∈ ℝ* )
19 1 2 6 4 deg1nn0cl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 )
20 7 8 9 19 syl3anc ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 )
21 1 2 6 4 deg1nn0cl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ 𝐵 ∧ 𝐺 ≠ 0 ) → ( 𝐷 ‘ 𝐺 ) ∈ ℕ0 )
22 7 11 12 21 syl3anc ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) ∈ ℕ0 )
23 20 22 nn0addcld ⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝐹 ) + ( 𝐷 ‘ 𝐺 ) ) ∈ ℕ0 )
24 23 nn0red ⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝐹 ) + ( 𝐷 ‘ 𝐺 ) ) ∈ ℝ )
25 24 rexrd ⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝐹 ) + ( 𝐷 ‘ 𝐺 ) ) ∈ ℝ* )
26 20 nn0red ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) ∈ ℝ )
27 26 leidd ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐹 ) )
28 22 nn0red ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) ∈ ℝ )
29 28 leidd ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) ≤ ( 𝐷 ‘ 𝐺 ) )
30 2 1 7 4 5 8 11 20 22 27 29 deg1mulle2 ⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 · 𝐺 ) ) ≤ ( ( 𝐷 ‘ 𝐹 ) + ( 𝐷 ‘ 𝐺 ) ) )
31 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
32 2 5 31 4 1 6 7 8 9 11 12 coe1mul4 ⊢ ( 𝜑 → ( ( coe1 ‘ ( 𝐹 · 𝐺 ) ) ‘ ( ( 𝐷 ‘ 𝐹 ) + ( 𝐷 ‘ 𝐺 ) ) ) = ( ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) ) )
33 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
34 eqid ⊢ ( coe1 ‘ 𝐺 ) = ( coe1 ‘ 𝐺 )
35 1 2 6 4 33 34 deg1ldg ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ 𝐵 ∧ 𝐺 ≠ 0 ) → ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) ≠ ( 0g ‘ 𝑅 ) )
36 7 11 12 35 syl3anc ⊢ ( 𝜑 → ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) ≠ ( 0g ‘ 𝑅 ) )
37 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
38 34 4 2 37 coe1f ⊢ ( 𝐺 ∈ 𝐵 → ( coe1 ‘ 𝐺 ) : ℕ0 ⟶ ( Base ‘ 𝑅 ) )
39 11 38 syl ⊢ ( 𝜑 → ( coe1 ‘ 𝐺 ) : ℕ0 ⟶ ( Base ‘ 𝑅 ) )
40 39 22 ffvelcdmd ⊢ ( 𝜑 → ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) ∈ ( Base ‘ 𝑅 ) )
41 3 37 31 33 rrgeq0i ⊢ ( ( ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) ∈ 𝐸 ∧ ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) ) = ( 0g ‘ 𝑅 ) → ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) = ( 0g ‘ 𝑅 ) ) )
42 10 40 41 syl2anc ⊢ ( 𝜑 → ( ( ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) ) = ( 0g ‘ 𝑅 ) → ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) = ( 0g ‘ 𝑅 ) ) )
43 42 necon3d ⊢ ( 𝜑 → ( ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) ≠ ( 0g ‘ 𝑅 ) → ( ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) ) ≠ ( 0g ‘ 𝑅 ) ) )
44 36 43 mpd ⊢ ( 𝜑 → ( ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) ) ≠ ( 0g ‘ 𝑅 ) )
45 32 44 eqnetrd ⊢ ( 𝜑 → ( ( coe1 ‘ ( 𝐹 · 𝐺 ) ) ‘ ( ( 𝐷 ‘ 𝐹 ) + ( 𝐷 ‘ 𝐺 ) ) ) ≠ ( 0g ‘ 𝑅 ) )
46 eqid ⊢ ( coe1 ‘ ( 𝐹 · 𝐺 ) ) = ( coe1 ‘ ( 𝐹 · 𝐺 ) )
47 1 2 4 33 46 deg1ge ⊢ ( ( ( 𝐹 · 𝐺 ) ∈ 𝐵 ∧ ( ( 𝐷 ‘ 𝐹 ) + ( 𝐷 ‘ 𝐺 ) ) ∈ ℕ0 ∧ ( ( coe1 ‘ ( 𝐹 · 𝐺 ) ) ‘ ( ( 𝐷 ‘ 𝐹 ) + ( 𝐷 ‘ 𝐺 ) ) ) ≠ ( 0g ‘ 𝑅 ) ) → ( ( 𝐷 ‘ 𝐹 ) + ( 𝐷 ‘ 𝐺 ) ) ≤ ( 𝐷 ‘ ( 𝐹 · 𝐺 ) ) )
48 16 23 45 47 syl3anc ⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝐹 ) + ( 𝐷 ‘ 𝐺 ) ) ≤ ( 𝐷 ‘ ( 𝐹 · 𝐺 ) ) )
49 18 25 30 48 xrletrid ⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 · 𝐺 ) ) = ( ( 𝐷 ‘ 𝐹 ) + ( 𝐷 ‘ 𝐺 ) ) )