Metamath Proof Explorer


Theorem deg1ldg

Description: A nonzero univariate polynomial always has a nonzero leading coefficient. (Contributed by Stefan O'Rear, 23-Mar-2015)

Ref Expression
Hypotheses deg1z.d 𝐷 = ( deg1𝑅 )
deg1z.p 𝑃 = ( Poly1𝑅 )
deg1z.z 0 = ( 0g𝑃 )
deg1nn0cl.b 𝐵 = ( Base ‘ 𝑃 )
deg1ldg.y 𝑌 = ( 0g𝑅 )
deg1ldg.a 𝐴 = ( coe1𝐹 )
Assertion deg1ldg ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐹0 ) → ( 𝐴 ‘ ( 𝐷𝐹 ) ) ≠ 𝑌 )

Proof

Step Hyp Ref Expression
1 deg1z.d 𝐷 = ( deg1𝑅 )
2 deg1z.p 𝑃 = ( Poly1𝑅 )
3 deg1z.z 0 = ( 0g𝑃 )
4 deg1nn0cl.b 𝐵 = ( Base ‘ 𝑃 )
5 deg1ldg.y 𝑌 = ( 0g𝑅 )
6 deg1ldg.a 𝐴 = ( coe1𝐹 )
7 1 deg1fval 𝐷 = ( 1o mDeg 𝑅 )
8 eqid ( 1o mPoly 𝑅 ) = ( 1o mPoly 𝑅 )
9 eqid ( PwSer1𝑅 ) = ( PwSer1𝑅 )
10 2 9 4 ply1bas 𝐵 = ( Base ‘ ( 1o mPoly 𝑅 ) )
11 psr1baslem ( ℕ0m 1o ) = { 𝑐 ∈ ( ℕ0m 1o ) ∣ ( 𝑐 “ ℕ ) ∈ Fin }
12 tdeglem2 ( 𝑎 ∈ ( ℕ0m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) = ( 𝑎 ∈ ( ℕ0m 1o ) ↦ ( ℂfld Σg 𝑎 ) )
13 8 2 3 ply1mpl0 0 = ( 0g ‘ ( 1o mPoly 𝑅 ) )
14 7 8 10 5 11 12 13 mdegldg ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐹0 ) → ∃ 𝑏 ∈ ( ℕ0m 1o ) ( ( 𝐹𝑏 ) ≠ 𝑌 ∧ ( ( 𝑎 ∈ ( ℕ0m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) = ( 𝐷𝐹 ) ) )
15 6 fvcoe1 ( ( 𝐹𝐵𝑏 ∈ ( ℕ0m 1o ) ) → ( 𝐹𝑏 ) = ( 𝐴 ‘ ( 𝑏 ‘ ∅ ) ) )
16 15 3ad2antl2 ( ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐹0 ) ∧ 𝑏 ∈ ( ℕ0m 1o ) ) → ( 𝐹𝑏 ) = ( 𝐴 ‘ ( 𝑏 ‘ ∅ ) ) )
17 fveq1 ( 𝑎 = 𝑏 → ( 𝑎 ‘ ∅ ) = ( 𝑏 ‘ ∅ ) )
18 eqid ( 𝑎 ∈ ( ℕ0m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) = ( 𝑎 ∈ ( ℕ0m 1o ) ↦ ( 𝑎 ‘ ∅ ) )
19 fvex ( 𝑏 ‘ ∅ ) ∈ V
20 17 18 19 fvmpt ( 𝑏 ∈ ( ℕ0m 1o ) → ( ( 𝑎 ∈ ( ℕ0m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) = ( 𝑏 ‘ ∅ ) )
21 20 fveq2d ( 𝑏 ∈ ( ℕ0m 1o ) → ( 𝐴 ‘ ( ( 𝑎 ∈ ( ℕ0m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) ) = ( 𝐴 ‘ ( 𝑏 ‘ ∅ ) ) )
22 21 adantl ( ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐹0 ) ∧ 𝑏 ∈ ( ℕ0m 1o ) ) → ( 𝐴 ‘ ( ( 𝑎 ∈ ( ℕ0m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) ) = ( 𝐴 ‘ ( 𝑏 ‘ ∅ ) ) )
23 16 22 eqtr4d ( ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐹0 ) ∧ 𝑏 ∈ ( ℕ0m 1o ) ) → ( 𝐹𝑏 ) = ( 𝐴 ‘ ( ( 𝑎 ∈ ( ℕ0m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) ) )
24 23 neeq1d ( ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐹0 ) ∧ 𝑏 ∈ ( ℕ0m 1o ) ) → ( ( 𝐹𝑏 ) ≠ 𝑌 ↔ ( 𝐴 ‘ ( ( 𝑎 ∈ ( ℕ0m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) ) ≠ 𝑌 ) )
25 24 anbi1d ( ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐹0 ) ∧ 𝑏 ∈ ( ℕ0m 1o ) ) → ( ( ( 𝐹𝑏 ) ≠ 𝑌 ∧ ( ( 𝑎 ∈ ( ℕ0m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) = ( 𝐷𝐹 ) ) ↔ ( ( 𝐴 ‘ ( ( 𝑎 ∈ ( ℕ0m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) ) ≠ 𝑌 ∧ ( ( 𝑎 ∈ ( ℕ0m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) = ( 𝐷𝐹 ) ) ) )
26 25 biancomd ( ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐹0 ) ∧ 𝑏 ∈ ( ℕ0m 1o ) ) → ( ( ( 𝐹𝑏 ) ≠ 𝑌 ∧ ( ( 𝑎 ∈ ( ℕ0m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) = ( 𝐷𝐹 ) ) ↔ ( ( ( 𝑎 ∈ ( ℕ0m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) = ( 𝐷𝐹 ) ∧ ( 𝐴 ‘ ( ( 𝑎 ∈ ( ℕ0m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) ) ≠ 𝑌 ) ) )
27 26 rexbidva ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐹0 ) → ( ∃ 𝑏 ∈ ( ℕ0m 1o ) ( ( 𝐹𝑏 ) ≠ 𝑌 ∧ ( ( 𝑎 ∈ ( ℕ0m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) = ( 𝐷𝐹 ) ) ↔ ∃ 𝑏 ∈ ( ℕ0m 1o ) ( ( ( 𝑎 ∈ ( ℕ0m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) = ( 𝐷𝐹 ) ∧ ( 𝐴 ‘ ( ( 𝑎 ∈ ( ℕ0m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) ) ≠ 𝑌 ) ) )
28 df1o2 1o = { ∅ }
29 nn0ex 0 ∈ V
30 0ex ∅ ∈ V
31 28 29 30 18 mapsnf1o2 ( 𝑎 ∈ ( ℕ0m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) : ( ℕ0m 1o ) –1-1-onto→ ℕ0
32 f1ofo ( ( 𝑎 ∈ ( ℕ0m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) : ( ℕ0m 1o ) –1-1-onto→ ℕ0 → ( 𝑎 ∈ ( ℕ0m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) : ( ℕ0m 1o ) –onto→ ℕ0 )
33 eqeq1 ( ( ( 𝑎 ∈ ( ℕ0m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) = 𝑑 → ( ( ( 𝑎 ∈ ( ℕ0m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) = ( 𝐷𝐹 ) ↔ 𝑑 = ( 𝐷𝐹 ) ) )
34 fveq2 ( ( ( 𝑎 ∈ ( ℕ0m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) = 𝑑 → ( 𝐴 ‘ ( ( 𝑎 ∈ ( ℕ0m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) ) = ( 𝐴𝑑 ) )
35 34 neeq1d ( ( ( 𝑎 ∈ ( ℕ0m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) = 𝑑 → ( ( 𝐴 ‘ ( ( 𝑎 ∈ ( ℕ0m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) ) ≠ 𝑌 ↔ ( 𝐴𝑑 ) ≠ 𝑌 ) )
36 33 35 anbi12d ( ( ( 𝑎 ∈ ( ℕ0m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) = 𝑑 → ( ( ( ( 𝑎 ∈ ( ℕ0m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) = ( 𝐷𝐹 ) ∧ ( 𝐴 ‘ ( ( 𝑎 ∈ ( ℕ0m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) ) ≠ 𝑌 ) ↔ ( 𝑑 = ( 𝐷𝐹 ) ∧ ( 𝐴𝑑 ) ≠ 𝑌 ) ) )
37 36 cbvexfo ( ( 𝑎 ∈ ( ℕ0m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) : ( ℕ0m 1o ) –onto→ ℕ0 → ( ∃ 𝑏 ∈ ( ℕ0m 1o ) ( ( ( 𝑎 ∈ ( ℕ0m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) = ( 𝐷𝐹 ) ∧ ( 𝐴 ‘ ( ( 𝑎 ∈ ( ℕ0m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) ) ≠ 𝑌 ) ↔ ∃ 𝑑 ∈ ℕ0 ( 𝑑 = ( 𝐷𝐹 ) ∧ ( 𝐴𝑑 ) ≠ 𝑌 ) ) )
38 31 32 37 mp2b ( ∃ 𝑏 ∈ ( ℕ0m 1o ) ( ( ( 𝑎 ∈ ( ℕ0m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) = ( 𝐷𝐹 ) ∧ ( 𝐴 ‘ ( ( 𝑎 ∈ ( ℕ0m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) ) ≠ 𝑌 ) ↔ ∃ 𝑑 ∈ ℕ0 ( 𝑑 = ( 𝐷𝐹 ) ∧ ( 𝐴𝑑 ) ≠ 𝑌 ) )
39 27 38 bitrdi ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐹0 ) → ( ∃ 𝑏 ∈ ( ℕ0m 1o ) ( ( 𝐹𝑏 ) ≠ 𝑌 ∧ ( ( 𝑎 ∈ ( ℕ0m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) = ( 𝐷𝐹 ) ) ↔ ∃ 𝑑 ∈ ℕ0 ( 𝑑 = ( 𝐷𝐹 ) ∧ ( 𝐴𝑑 ) ≠ 𝑌 ) ) )
40 1 2 3 4 deg1nn0cl ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐹0 ) → ( 𝐷𝐹 ) ∈ ℕ0 )
41 fveq2 ( 𝑑 = ( 𝐷𝐹 ) → ( 𝐴𝑑 ) = ( 𝐴 ‘ ( 𝐷𝐹 ) ) )
42 41 neeq1d ( 𝑑 = ( 𝐷𝐹 ) → ( ( 𝐴𝑑 ) ≠ 𝑌 ↔ ( 𝐴 ‘ ( 𝐷𝐹 ) ) ≠ 𝑌 ) )
43 42 ceqsrexv ( ( 𝐷𝐹 ) ∈ ℕ0 → ( ∃ 𝑑 ∈ ℕ0 ( 𝑑 = ( 𝐷𝐹 ) ∧ ( 𝐴𝑑 ) ≠ 𝑌 ) ↔ ( 𝐴 ‘ ( 𝐷𝐹 ) ) ≠ 𝑌 ) )
44 40 43 syl ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐹0 ) → ( ∃ 𝑑 ∈ ℕ0 ( 𝑑 = ( 𝐷𝐹 ) ∧ ( 𝐴𝑑 ) ≠ 𝑌 ) ↔ ( 𝐴 ‘ ( 𝐷𝐹 ) ) ≠ 𝑌 ) )
45 39 44 bitrd ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐹0 ) → ( ∃ 𝑏 ∈ ( ℕ0m 1o ) ( ( 𝐹𝑏 ) ≠ 𝑌 ∧ ( ( 𝑎 ∈ ( ℕ0m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) = ( 𝐷𝐹 ) ) ↔ ( 𝐴 ‘ ( 𝐷𝐹 ) ) ≠ 𝑌 ) )
46 14 45 mpbid ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐹0 ) → ( 𝐴 ‘ ( 𝐷𝐹 ) ) ≠ 𝑌 )