MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  deg1le0 Structured version   Visualization version   GIF version

Theorem deg1le0 25014
Description: A polynomial has nonpositive degree iff it is a constant. (Contributed by Stefan O'Rear, 29-Mar-2015.)
Hypotheses
Ref Expression
deg1le0.d 𝐷 = ( deg1𝑅)
deg1le0.p 𝑃 = (Poly1𝑅)
deg1le0.b 𝐵 = (Base‘𝑃)
deg1le0.a 𝐴 = (algSc‘𝑃)
Assertion
Ref Expression
deg1le0 ((𝑅 ∈ Ring ∧ 𝐹𝐵) → ((𝐷𝐹) ≤ 0 ↔ 𝐹 = (𝐴‘((coe1𝐹)‘0))))

Proof of Theorem deg1le0
StepHypRef Expression
1 eqid 2737 . . 3 (1o mPoly 𝑅) = (1o mPoly 𝑅)
2 deg1le0.d . . . 4 𝐷 = ( deg1𝑅)
32deg1fval 24983 . . 3 𝐷 = (1o mDeg 𝑅)
4 1on 8214 . . . 4 1o ∈ On
54a1i 11 . . 3 ((𝑅 ∈ Ring ∧ 𝐹𝐵) → 1o ∈ On)
6 simpl 486 . . 3 ((𝑅 ∈ Ring ∧ 𝐹𝐵) → 𝑅 ∈ Ring)
7 deg1le0.p . . . 4 𝑃 = (Poly1𝑅)
8 eqid 2737 . . . 4 (PwSer1𝑅) = (PwSer1𝑅)
9 deg1le0.b . . . 4 𝐵 = (Base‘𝑃)
107, 8, 9ply1bas 21121 . . 3 𝐵 = (Base‘(1o mPoly 𝑅))
11 deg1le0.a . . . 4 𝐴 = (algSc‘𝑃)
127, 11ply1ascl 21184 . . 3 𝐴 = (algSc‘(1o mPoly 𝑅))
13 simpr 488 . . 3 ((𝑅 ∈ Ring ∧ 𝐹𝐵) → 𝐹𝐵)
141, 3, 5, 6, 10, 12, 13mdegle0 24980 . 2 ((𝑅 ∈ Ring ∧ 𝐹𝐵) → ((𝐷𝐹) ≤ 0 ↔ 𝐹 = (𝐴‘(𝐹‘(1o × {0})))))
15 0nn0 12110 . . . . 5 0 ∈ ℕ0
16 eqid 2737 . . . . . 6 (coe1𝐹) = (coe1𝐹)
1716coe1fv 21132 . . . . 5 ((𝐹𝐵 ∧ 0 ∈ ℕ0) → ((coe1𝐹)‘0) = (𝐹‘(1o × {0})))
1813, 15, 17sylancl 589 . . . 4 ((𝑅 ∈ Ring ∧ 𝐹𝐵) → ((coe1𝐹)‘0) = (𝐹‘(1o × {0})))
1918fveq2d 6726 . . 3 ((𝑅 ∈ Ring ∧ 𝐹𝐵) → (𝐴‘((coe1𝐹)‘0)) = (𝐴‘(𝐹‘(1o × {0}))))
2019eqeq2d 2748 . 2 ((𝑅 ∈ Ring ∧ 𝐹𝐵) → (𝐹 = (𝐴‘((coe1𝐹)‘0)) ↔ 𝐹 = (𝐴‘(𝐹‘(1o × {0})))))
2114, 20bitr4d 285 1 ((𝑅 ∈ Ring ∧ 𝐹𝐵) → ((𝐷𝐹) ≤ 0 ↔ 𝐹 = (𝐴‘((coe1𝐹)‘0))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1543  wcel 2110  {csn 4546   class class class wbr 5058   × cxp 5554  Oncon0 6218  cfv 6385  (class class class)co 7218  1oc1o 8200  0cc0 10734  cle 10873  0cn0 12095  Basecbs 16765  Ringcrg 19567  algSccascl 20819   mPoly cmpl 20870  PwSer1cps1 21101  Poly1cpl1 21103  coe1cco1 21104   deg1 cdg1 24954
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-rep 5184  ax-sep 5197  ax-nul 5204  ax-pow 5263  ax-pr 5327  ax-un 7528  ax-cnex 10790  ax-resscn 10791  ax-1cn 10792  ax-icn 10793  ax-addcl 10794  ax-addrcl 10795  ax-mulcl 10796  ax-mulrcl 10797  ax-mulcom 10798  ax-addass 10799  ax-mulass 10800  ax-distr 10801  ax-i2m1 10802  ax-1ne0 10803  ax-1rid 10804  ax-rnegex 10805  ax-rrecex 10806  ax-cnre 10807  ax-pre-lttri 10808  ax-pre-lttrn 10809  ax-pre-ltadd 10810  ax-pre-mulgt0 10811  ax-pre-sup 10812  ax-addf 10813  ax-mulf 10814
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3415  df-sbc 3700  df-csb 3817  df-dif 3874  df-un 3876  df-in 3878  df-ss 3888  df-pss 3890  df-nul 4243  df-if 4445  df-pw 4520  df-sn 4547  df-pr 4549  df-tp 4551  df-op 4553  df-uni 4825  df-int 4865  df-iun 4911  df-iin 4912  df-br 5059  df-opab 5121  df-mpt 5141  df-tr 5167  df-id 5460  df-eprel 5465  df-po 5473  df-so 5474  df-fr 5514  df-se 5515  df-we 5516  df-xp 5562  df-rel 5563  df-cnv 5564  df-co 5565  df-dm 5566  df-rn 5567  df-res 5568  df-ima 5569  df-pred 6165  df-ord 6221  df-on 6222  df-lim 6223  df-suc 6224  df-iota 6343  df-fun 6387  df-fn 6388  df-f 6389  df-f1 6390  df-fo 6391  df-f1o 6392  df-fv 6393  df-isom 6394  df-riota 7175  df-ov 7221  df-oprab 7222  df-mpo 7223  df-of 7474  df-ofr 7475  df-om 7650  df-1st 7766  df-2nd 7767  df-supp 7909  df-wrecs 8052  df-recs 8113  df-rdg 8151  df-1o 8207  df-er 8396  df-map 8515  df-pm 8516  df-ixp 8584  df-en 8632  df-dom 8633  df-sdom 8634  df-fin 8635  df-fsupp 8991  df-sup 9063  df-oi 9131  df-card 9560  df-pnf 10874  df-mnf 10875  df-xr 10876  df-ltxr 10877  df-le 10878  df-sub 11069  df-neg 11070  df-nn 11836  df-2 11898  df-3 11899  df-4 11900  df-5 11901  df-6 11902  df-7 11903  df-8 11904  df-9 11905  df-n0 12096  df-z 12182  df-dec 12299  df-uz 12444  df-fz 13101  df-fzo 13244  df-seq 13580  df-hash 13902  df-struct 16705  df-sets 16722  df-slot 16740  df-ndx 16750  df-base 16766  df-ress 16790  df-plusg 16820  df-mulr 16821  df-starv 16822  df-sca 16823  df-vsca 16824  df-tset 16826  df-ple 16827  df-ds 16829  df-unif 16830  df-0g 16951  df-gsum 16952  df-mre 17094  df-mrc 17095  df-acs 17097  df-mgm 18119  df-sgrp 18168  df-mnd 18179  df-mhm 18223  df-submnd 18224  df-grp 18373  df-minusg 18374  df-mulg 18494  df-subg 18545  df-ghm 18625  df-cntz 18716  df-cmn 19177  df-abl 19178  df-mgp 19510  df-ur 19522  df-ring 19569  df-cring 19570  df-subrg 19803  df-cnfld 20369  df-ascl 20822  df-psr 20873  df-mpl 20875  df-opsr 20877  df-psr1 21106  df-ply1 21108  df-coe1 21109  df-mdeg 24955  df-deg1 24956
This theorem is referenced by:  deg1sclle  25015  ply1rem  25066  fta1g  25070
  Copyright terms: Public domain W3C validator