Theorem deg1tmle

Description: Limiting 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 ‘ 𝑁 )
Assertion	deg1tmle	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐹 ∈ ℕ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		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
9		simpl1	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐹 ∈ ℕ0 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐹 < 𝑥 ) ) → 𝑅 ∈ Ring )
10		simpl2	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐹 ∈ ℕ0 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐹 < 𝑥 ) ) → 𝐶 ∈ 𝐾 )
11		simpl3	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐹 ∈ ℕ0 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐹 < 𝑥 ) ) → 𝐹 ∈ ℕ0 )
12		simprl	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐹 ∈ ℕ0 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐹 < 𝑥 ) ) → 𝑥 ∈ ℕ0 )
13	11	nn0red	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐹 ∈ ℕ0 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐹 < 𝑥 ) ) → 𝐹 ∈ ℝ )
14		simprr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐹 ∈ ℕ0 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐹 < 𝑥 ) ) → 𝐹 < 𝑥 )
15	13 14	ltned	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐹 ∈ ℕ0 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐹 < 𝑥 ) ) → 𝐹 ≠ 𝑥 )
16	8 2 3 4 5 6 7 9 10 11 12 15	coe1tmfv2	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐹 ∈ ℕ0 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐹 < 𝑥 ) ) → ( ( coe1 ‘ ( 𝐶 · ( 𝐹 ↑ 𝑋 ) ) ) ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) )
17	16	expr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐹 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ( 𝐹 < 𝑥 → ( ( coe1 ‘ ( 𝐶 · ( 𝐹 ↑ 𝑋 ) ) ) ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) )
18	17	ralrimiva	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐹 ∈ ℕ0 ) → ∀ 𝑥 ∈ ℕ0 ( 𝐹 < 𝑥 → ( ( coe1 ‘ ( 𝐶 · ( 𝐹 ↑ 𝑋 ) ) ) ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) )
19		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
20	2 3 4 5 6 7 19	ply1tmcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐹 ∈ ℕ0 ) → ( 𝐶 · ( 𝐹 ↑ 𝑋 ) ) ∈ ( Base ‘ 𝑃 ) )
21		nn0re	⊢ ( 𝐹 ∈ ℕ0 → 𝐹 ∈ ℝ )
22	21	rexrd	⊢ ( 𝐹 ∈ ℕ0 → 𝐹 ∈ ℝ* )
23	22	3ad2ant3	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐹 ∈ ℕ0 ) → 𝐹 ∈ ℝ* )
24		eqid	⊢ ( coe1 ‘ ( 𝐶 · ( 𝐹 ↑ 𝑋 ) ) ) = ( coe1 ‘ ( 𝐶 · ( 𝐹 ↑ 𝑋 ) ) )
25	1 3 19 8 24	deg1leb	⊢ ( ( ( 𝐶 · ( 𝐹 ↑ 𝑋 ) ) ∈ ( Base ‘ 𝑃 ) ∧ 𝐹 ∈ ℝ* ) → ( ( 𝐷 ‘ ( 𝐶 · ( 𝐹 ↑ 𝑋 ) ) ) ≤ 𝐹 ↔ ∀ 𝑥 ∈ ℕ0 ( 𝐹 < 𝑥 → ( ( coe1 ‘ ( 𝐶 · ( 𝐹 ↑ 𝑋 ) ) ) ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) )
26	20 23 25	syl2anc	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐹 ∈ ℕ0 ) → ( ( 𝐷 ‘ ( 𝐶 · ( 𝐹 ↑ 𝑋 ) ) ) ≤ 𝐹 ↔ ∀ 𝑥 ∈ ℕ0 ( 𝐹 < 𝑥 → ( ( coe1 ‘ ( 𝐶 · ( 𝐹 ↑ 𝑋 ) ) ) ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) )
27	18 26	mpbird	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐹 ∈ ℕ0 ) → ( 𝐷 ‘ ( 𝐶 · ( 𝐹 ↑ 𝑋 ) ) ) ≤ 𝐹 )