Metamath Proof Explorer

Theorem deg1tm

Description: Exact degree of a polynomial term. (Contributed by Stefan O'Rear, 27-Mar-2015)

Ref Expression
Hypotheses deg1tm.d ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
deg1tm.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
deg1tm.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
deg1tm.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
deg1tm.m ⊢ · = ( ·𝑠 ‘ 𝑃 )
deg1tm.n ⊢ 𝑁 = ( mulGrp ‘ 𝑃 )
deg1tm.e ⊢ ↑ = ( .g ‘ 𝑁 )
deg1tm.z ⊢ 0 = ( 0g ‘ 𝑅 )
Assertion deg1tm ( ( 𝑅 ∈ Ring ∧ ( 𝐶 ∈ 𝐾 ∧ 𝐶 ≠ 0 ) ∧ 𝐹 ∈ ℕ0 ) → ( 𝐷 ‘ ( 𝐶 · ( 𝐹 ↑ 𝑋 ) ) ) = 𝐹 )

Proof

Step Hyp Ref Expression
1 deg1tm.d ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
2 deg1tm.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
3 deg1tm.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
4 deg1tm.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
5 deg1tm.m ⊢ · = ( ·𝑠 ‘ 𝑃 )
6 deg1tm.n ⊢ 𝑁 = ( mulGrp ‘ 𝑃 )
7 deg1tm.e ⊢ ↑ = ( .g ‘ 𝑁 )
8 deg1tm.z ⊢ 0 = ( 0g ‘ 𝑅 )
9 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
10 2 3 4 5 6 7 9 ply1tmcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐹 ∈ ℕ0 ) → ( 𝐶 · ( 𝐹 ↑ 𝑋 ) ) ∈ ( Base ‘ 𝑃 ) )
11 10 3adant2r ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐶 ∈ 𝐾 ∧ 𝐶 ≠ 0 ) ∧ 𝐹 ∈ ℕ0 ) → ( 𝐶 · ( 𝐹 ↑ 𝑋 ) ) ∈ ( Base ‘ 𝑃 ) )
12 1 3 9 deg1xrcl ⊢ ( ( 𝐶 · ( 𝐹 ↑ 𝑋 ) ) ∈ ( Base ‘ 𝑃 ) → ( 𝐷 ‘ ( 𝐶 · ( 𝐹 ↑ 𝑋 ) ) ) ∈ ℝ* )
13 11 12 syl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐶 ∈ 𝐾 ∧ 𝐶 ≠ 0 ) ∧ 𝐹 ∈ ℕ0 ) → ( 𝐷 ‘ ( 𝐶 · ( 𝐹 ↑ 𝑋 ) ) ) ∈ ℝ* )
14 simp3 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐶 ∈ 𝐾 ∧ 𝐶 ≠ 0 ) ∧ 𝐹 ∈ ℕ0 ) → 𝐹 ∈ ℕ0 )
15 14 nn0red ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐶 ∈ 𝐾 ∧ 𝐶 ≠ 0 ) ∧ 𝐹 ∈ ℕ0 ) → 𝐹 ∈ ℝ )
16 15 rexrd ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐶 ∈ 𝐾 ∧ 𝐶 ≠ 0 ) ∧ 𝐹 ∈ ℕ0 ) → 𝐹 ∈ ℝ* )
17 1 2 3 4 5 6 7 deg1tmle ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐹 ∈ ℕ0 ) → ( 𝐷 ‘ ( 𝐶 · ( 𝐹 ↑ 𝑋 ) ) ) ≤ 𝐹 )
18 17 3adant2r ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐶 ∈ 𝐾 ∧ 𝐶 ≠ 0 ) ∧ 𝐹 ∈ ℕ0 ) → ( 𝐷 ‘ ( 𝐶 · ( 𝐹 ↑ 𝑋 ) ) ) ≤ 𝐹 )
19 8 2 3 4 5 6 7 coe1tmfv1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐹 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝐶 · ( 𝐹 ↑ 𝑋 ) ) ) ‘ 𝐹 ) = 𝐶 )
20 19 3adant2r ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐶 ∈ 𝐾 ∧ 𝐶 ≠ 0 ) ∧ 𝐹 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝐶 · ( 𝐹 ↑ 𝑋 ) ) ) ‘ 𝐹 ) = 𝐶 )
21 simp2r ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐶 ∈ 𝐾 ∧ 𝐶 ≠ 0 ) ∧ 𝐹 ∈ ℕ0 ) → 𝐶 ≠ 0 )
22 20 21 eqnetrd ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐶 ∈ 𝐾 ∧ 𝐶 ≠ 0 ) ∧ 𝐹 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝐶 · ( 𝐹 ↑ 𝑋 ) ) ) ‘ 𝐹 ) ≠ 0 )
23 eqid ⊢ ( coe1 ‘ ( 𝐶 · ( 𝐹 ↑ 𝑋 ) ) ) = ( coe1 ‘ ( 𝐶 · ( 𝐹 ↑ 𝑋 ) ) )
24 1 3 9 8 23 deg1ge ⊢ ( ( ( 𝐶 · ( 𝐹 ↑ 𝑋 ) ) ∈ ( Base ‘ 𝑃 ) ∧ 𝐹 ∈ ℕ0 ∧ ( ( coe1 ‘ ( 𝐶 · ( 𝐹 ↑ 𝑋 ) ) ) ‘ 𝐹 ) ≠ 0 ) → 𝐹 ≤ ( 𝐷 ‘ ( 𝐶 · ( 𝐹 ↑ 𝑋 ) ) ) )
25 11 14 22 24 syl3anc ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐶 ∈ 𝐾 ∧ 𝐶 ≠ 0 ) ∧ 𝐹 ∈ ℕ0 ) → 𝐹 ≤ ( 𝐷 ‘ ( 𝐶 · ( 𝐹 ↑ 𝑋 ) ) ) )
26 13 16 18 25 xrletrid ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐶 ∈ 𝐾 ∧ 𝐶 ≠ 0 ) ∧ 𝐹 ∈ ℕ0 ) → ( 𝐷 ‘ ( 𝐶 · ( 𝐹 ↑ 𝑋 ) ) ) = 𝐹 )