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

Theorem ply1bas 21140
Description: The value of the base set of univariate polynomials. (Contributed by Mario Carneiro, 9-Feb-2015.)
Hypotheses
Ref Expression
ply1val.1 𝑃 = (Poly1𝑅)
ply1val.2 𝑆 = (PwSer1𝑅)
ply1bas.u 𝑈 = (Base‘𝑃)
Assertion
Ref Expression
ply1bas 𝑈 = (Base‘(1o mPoly 𝑅))

Proof of Theorem ply1bas
StepHypRef Expression
1 ply1bas.u . 2 𝑈 = (Base‘𝑃)
2 eqid 2738 . . . 4 (1o mPoly 𝑅) = (1o mPoly 𝑅)
3 eqid 2738 . . . 4 (1o mPwSer 𝑅) = (1o mPwSer 𝑅)
4 eqid 2738 . . . 4 (Base‘(1o mPoly 𝑅)) = (Base‘(1o mPoly 𝑅))
5 ply1val.2 . . . . 5 𝑆 = (PwSer1𝑅)
6 eqid 2738 . . . . 5 (Base‘𝑆) = (Base‘𝑆)
75, 6, 3psr1bas2 21135 . . . 4 (Base‘𝑆) = (Base‘(1o mPwSer 𝑅))
82, 3, 4, 7mplbasss 20983 . . 3 (Base‘(1o mPoly 𝑅)) ⊆ (Base‘𝑆)
9 ply1val.1 . . . . 5 𝑃 = (Poly1𝑅)
109, 5ply1val 21139 . . . 4 𝑃 = (𝑆s (Base‘(1o mPoly 𝑅)))
1110, 6ressbas2 16815 . . 3 ((Base‘(1o mPoly 𝑅)) ⊆ (Base‘𝑆) → (Base‘(1o mPoly 𝑅)) = (Base‘𝑃))
128, 11ax-mp 5 . 2 (Base‘(1o mPoly 𝑅)) = (Base‘𝑃)
131, 12eqtr4i 2769 1 𝑈 = (Base‘(1o mPoly 𝑅))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1543  wss 3880  cfv 6397  (class class class)co 7231  1oc1o 8215  Basecbs 16784   mPwSer cmps 20887   mPoly cmpl 20889  PwSer1cps1 21120  Poly1cpl1 21122
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 2113  ax-9 2121  ax-10 2142  ax-11 2159  ax-12 2176  ax-ext 2709  ax-rep 5193  ax-sep 5206  ax-nul 5213  ax-pow 5272  ax-pr 5336  ax-un 7541  ax-cnex 10809  ax-resscn 10810  ax-1cn 10811  ax-icn 10812  ax-addcl 10813  ax-addrcl 10814  ax-mulcl 10815  ax-mulrcl 10816  ax-mulcom 10817  ax-addass 10818  ax-mulass 10819  ax-distr 10820  ax-i2m1 10821  ax-1ne0 10822  ax-1rid 10823  ax-rnegex 10824  ax-rrecex 10825  ax-cnre 10826  ax-pre-lttri 10827  ax-pre-lttrn 10828  ax-pre-ltadd 10829  ax-pre-mulgt0 10830
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 2072  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3067  df-rex 3068  df-reu 3069  df-rab 3071  df-v 3422  df-sbc 3709  df-csb 3826  df-dif 3883  df-un 3885  df-in 3887  df-ss 3897  df-pss 3899  df-nul 4252  df-if 4454  df-pw 4529  df-sn 4556  df-pr 4558  df-tp 4560  df-op 4562  df-uni 4834  df-iun 4920  df-br 5068  df-opab 5130  df-mpt 5150  df-tr 5176  df-id 5469  df-eprel 5474  df-po 5482  df-so 5483  df-fr 5523  df-we 5525  df-xp 5571  df-rel 5572  df-cnv 5573  df-co 5574  df-dm 5575  df-rn 5576  df-res 5577  df-ima 5578  df-pred 6175  df-ord 6233  df-on 6234  df-lim 6235  df-suc 6236  df-iota 6355  df-fun 6399  df-fn 6400  df-f 6401  df-f1 6402  df-fo 6403  df-f1o 6404  df-fv 6405  df-riota 7188  df-ov 7234  df-oprab 7235  df-mpo 7236  df-om 7663  df-wrecs 8067  df-recs 8128  df-rdg 8166  df-er 8411  df-en 8647  df-dom 8648  df-sdom 8649  df-pnf 10893  df-mnf 10894  df-xr 10895  df-ltxr 10896  df-le 10897  df-sub 11088  df-neg 11089  df-nn 11855  df-2 11917  df-3 11918  df-4 11919  df-5 11920  df-6 11921  df-7 11922  df-8 11923  df-9 11924  df-dec 12318  df-sets 16741  df-slot 16759  df-ndx 16769  df-base 16785  df-ress 16809  df-ple 16846  df-psr 20892  df-mpl 20894  df-opsr 20896  df-psr1 21125  df-ply1 21127
This theorem is referenced by:  ply1lss  21141  ply1subrg  21142  ply1crng  21143  ply1assa  21144  ply1basf  21147  ply1bascl2  21149  vr1cl  21162  ressply1bas2  21173  ressply1add  21175  ressply1mul  21176  ressply1vsca  21177  subrgply1  21178  ply1baspropd  21188  ply1ring  21193  ply1lmod  21197  ply1mpl0  21200  ply1mpl1  21202  subrg1asclcl  21205  subrgvr1cl  21207  coe1add  21209  coe1tm  21218  ply1coe  21241  evls1rhm  21262  evls1sca  21263  evl1rhm  21272  evl1sca  21274  evl1var  21276  evls1var  21278  mpfpf1  21291  pf1mpf  21292  deg1xrf  25003  deg1cl  25005  deg1nn0cl  25010  deg1ldg  25014  deg1leb  25017  deg1val  25018  deg1vscale  25026  deg1vsca  25027  deg1mulle2  25031  deg1le0  25033  fply1  31405
  Copyright terms: Public domain W3C validator