Theorem deg1leb

Description: Property of being of limited degree. (Contributed by Stefan O'Rear, 23-Mar-2015)

	Ref	Expression
Hypotheses	deg1leb.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
	deg1leb.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	deg1leb.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	deg1leb.y	⊢ 0 = ( 0g ‘ 𝑅 )
	deg1leb.a	⊢ 𝐴 = ( coe1 ‘ 𝐹 )
Assertion	deg1leb	⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ* ) → ( ( 𝐷 ‘ 𝐹 ) ≤ 𝐺 ↔ ∀ 𝑥 ∈ ℕ0 ( 𝐺 < 𝑥 → ( 𝐴 ‘ 𝑥 ) = 0 ) ) )

Proof

Step	Hyp	Ref	Expression
1		deg1leb.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
2		deg1leb.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
3		deg1leb.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
4		deg1leb.y	⊢ 0 = ( 0g ‘ 𝑅 )
5		deg1leb.a	⊢ 𝐴 = ( coe1 ‘ 𝐹 )
6	1	deg1fval	⊢ 𝐷 = ( 1o mDeg 𝑅 )
7		eqid	⊢ ( 1o mPoly 𝑅 ) = ( 1o mPoly 𝑅 )
8	2 3	ply1bas	⊢ 𝐵 = ( Base ‘ ( 1o mPoly 𝑅 ) )
9		psr1baslem	⊢ ( ℕ0 ↑m 1o ) = { 𝑎 ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin }
10		tdeglem2	⊢ ( 𝑏 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑏 ‘ ∅ ) ) = ( 𝑏 ∈ ( ℕ0 ↑m 1o ) ↦ ( ℂfld Σg 𝑏 ) )
11	6 7 8 4 9 10	mdegleb	⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ* ) → ( ( 𝐷 ‘ 𝐹 ) ≤ 𝐺 ↔ ∀ 𝑦 ∈ ( ℕ0 ↑m 1o ) ( 𝐺 < ( ( 𝑏 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑏 ‘ ∅ ) ) ‘ 𝑦 ) → ( 𝐹 ‘ 𝑦 ) = 0 ) ) )
12		df1o2	⊢ 1o = { ∅ }
13		nn0ex	⊢ ℕ0 ∈ V
14		0ex	⊢ ∅ ∈ V
15		eqid	⊢ ( 𝑏 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑏 ‘ ∅ ) ) = ( 𝑏 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑏 ‘ ∅ ) )
16	12 13 14 15	mapsnf1o2	⊢ ( 𝑏 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑏 ‘ ∅ ) ) : ( ℕ0 ↑m 1o ) –1-1-onto→ ℕ0
17		f1ofo	⊢ ( ( 𝑏 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑏 ‘ ∅ ) ) : ( ℕ0 ↑m 1o ) –1-1-onto→ ℕ0 → ( 𝑏 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑏 ‘ ∅ ) ) : ( ℕ0 ↑m 1o ) –onto→ ℕ0 )
18		breq2	⊢ ( ( ( 𝑏 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑏 ‘ ∅ ) ) ‘ 𝑦 ) = 𝑥 → ( 𝐺 < ( ( 𝑏 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑏 ‘ ∅ ) ) ‘ 𝑦 ) ↔ 𝐺 < 𝑥 ) )
19		fveqeq2	⊢ ( ( ( 𝑏 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑏 ‘ ∅ ) ) ‘ 𝑦 ) = 𝑥 → ( ( 𝐴 ‘ ( ( 𝑏 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑏 ‘ ∅ ) ) ‘ 𝑦 ) ) = 0 ↔ ( 𝐴 ‘ 𝑥 ) = 0 ) )
20	18 19	imbi12d	⊢ ( ( ( 𝑏 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑏 ‘ ∅ ) ) ‘ 𝑦 ) = 𝑥 → ( ( 𝐺 < ( ( 𝑏 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑏 ‘ ∅ ) ) ‘ 𝑦 ) → ( 𝐴 ‘ ( ( 𝑏 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑏 ‘ ∅ ) ) ‘ 𝑦 ) ) = 0 ) ↔ ( 𝐺 < 𝑥 → ( 𝐴 ‘ 𝑥 ) = 0 ) ) )
21	20	cbvfo	⊢ ( ( 𝑏 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑏 ‘ ∅ ) ) : ( ℕ0 ↑m 1o ) –onto→ ℕ0 → ( ∀ 𝑦 ∈ ( ℕ0 ↑m 1o ) ( 𝐺 < ( ( 𝑏 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑏 ‘ ∅ ) ) ‘ 𝑦 ) → ( 𝐴 ‘ ( ( 𝑏 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑏 ‘ ∅ ) ) ‘ 𝑦 ) ) = 0 ) ↔ ∀ 𝑥 ∈ ℕ0 ( 𝐺 < 𝑥 → ( 𝐴 ‘ 𝑥 ) = 0 ) ) )
22	16 17 21	mp2b	⊢ ( ∀ 𝑦 ∈ ( ℕ0 ↑m 1o ) ( 𝐺 < ( ( 𝑏 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑏 ‘ ∅ ) ) ‘ 𝑦 ) → ( 𝐴 ‘ ( ( 𝑏 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑏 ‘ ∅ ) ) ‘ 𝑦 ) ) = 0 ) ↔ ∀ 𝑥 ∈ ℕ0 ( 𝐺 < 𝑥 → ( 𝐴 ‘ 𝑥 ) = 0 ) )
23		fveq1	⊢ ( 𝑏 = 𝑦 → ( 𝑏 ‘ ∅ ) = ( 𝑦 ‘ ∅ ) )
24		fvex	⊢ ( 𝑦 ‘ ∅ ) ∈ V
25	23 15 24	fvmpt	⊢ ( 𝑦 ∈ ( ℕ0 ↑m 1o ) → ( ( 𝑏 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑏 ‘ ∅ ) ) ‘ 𝑦 ) = ( 𝑦 ‘ ∅ ) )
26	25	fveq2d	⊢ ( 𝑦 ∈ ( ℕ0 ↑m 1o ) → ( 𝐴 ‘ ( ( 𝑏 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑏 ‘ ∅ ) ) ‘ 𝑦 ) ) = ( 𝐴 ‘ ( 𝑦 ‘ ∅ ) ) )
27	26	adantl	⊢ ( ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ* ) ∧ 𝑦 ∈ ( ℕ0 ↑m 1o ) ) → ( 𝐴 ‘ ( ( 𝑏 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑏 ‘ ∅ ) ) ‘ 𝑦 ) ) = ( 𝐴 ‘ ( 𝑦 ‘ ∅ ) ) )
28	5	fvcoe1	⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝑦 ∈ ( ℕ0 ↑m 1o ) ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐴 ‘ ( 𝑦 ‘ ∅ ) ) )
29	28	adantlr	⊢ ( ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ* ) ∧ 𝑦 ∈ ( ℕ0 ↑m 1o ) ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐴 ‘ ( 𝑦 ‘ ∅ ) ) )
30	27 29	eqtr4d	⊢ ( ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ* ) ∧ 𝑦 ∈ ( ℕ0 ↑m 1o ) ) → ( 𝐴 ‘ ( ( 𝑏 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑏 ‘ ∅ ) ) ‘ 𝑦 ) ) = ( 𝐹 ‘ 𝑦 ) )
31	30	eqeq1d	⊢ ( ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ* ) ∧ 𝑦 ∈ ( ℕ0 ↑m 1o ) ) → ( ( 𝐴 ‘ ( ( 𝑏 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑏 ‘ ∅ ) ) ‘ 𝑦 ) ) = 0 ↔ ( 𝐹 ‘ 𝑦 ) = 0 ) )
32	31	imbi2d	⊢ ( ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ* ) ∧ 𝑦 ∈ ( ℕ0 ↑m 1o ) ) → ( ( 𝐺 < ( ( 𝑏 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑏 ‘ ∅ ) ) ‘ 𝑦 ) → ( 𝐴 ‘ ( ( 𝑏 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑏 ‘ ∅ ) ) ‘ 𝑦 ) ) = 0 ) ↔ ( 𝐺 < ( ( 𝑏 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑏 ‘ ∅ ) ) ‘ 𝑦 ) → ( 𝐹 ‘ 𝑦 ) = 0 ) ) )
33	32	ralbidva	⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ* ) → ( ∀ 𝑦 ∈ ( ℕ0 ↑m 1o ) ( 𝐺 < ( ( 𝑏 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑏 ‘ ∅ ) ) ‘ 𝑦 ) → ( 𝐴 ‘ ( ( 𝑏 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑏 ‘ ∅ ) ) ‘ 𝑦 ) ) = 0 ) ↔ ∀ 𝑦 ∈ ( ℕ0 ↑m 1o ) ( 𝐺 < ( ( 𝑏 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑏 ‘ ∅ ) ) ‘ 𝑦 ) → ( 𝐹 ‘ 𝑦 ) = 0 ) ) )
34	22 33	bitr3id	⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ* ) → ( ∀ 𝑥 ∈ ℕ0 ( 𝐺 < 𝑥 → ( 𝐴 ‘ 𝑥 ) = 0 ) ↔ ∀ 𝑦 ∈ ( ℕ0 ↑m 1o ) ( 𝐺 < ( ( 𝑏 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑏 ‘ ∅ ) ) ‘ 𝑦 ) → ( 𝐹 ‘ 𝑦 ) = 0 ) ) )
35	11 34	bitr4d	⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ* ) → ( ( 𝐷 ‘ 𝐹 ) ≤ 𝐺 ↔ ∀ 𝑥 ∈ ℕ0 ( 𝐺 < 𝑥 → ( 𝐴 ‘ 𝑥 ) = 0 ) ) )