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