Metamath Proof Explorer


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