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

Theorem ply1ascl 20967
 Description: The univariate polynomial ring inherits the multivariate ring's scalar function. (Contributed by Stefan O'Rear, 28-Mar-2015.) (Proof shortened by Fan Zheng, 26-Jun-2016.)
Hypotheses
Ref Expression
ply1ascl.p 𝑃 = (Poly1𝑅)
ply1ascl.a 𝐴 = (algSc‘𝑃)
Assertion
Ref Expression
ply1ascl 𝐴 = (algSc‘(1o mPoly 𝑅))

Proof of Theorem ply1ascl
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ply1ascl.a . 2 𝐴 = (algSc‘𝑃)
2 eqid 2759 . . . 4 (Scalar‘𝑃) = (Scalar‘𝑃)
3 eqid 2759 . . . 4 (Scalar‘(1o mPoly 𝑅)) = (Scalar‘(1o mPoly 𝑅))
4 ply1ascl.p . . . . . 6 𝑃 = (Poly1𝑅)
54ply1sca 20962 . . . . 5 (𝑅 ∈ V → 𝑅 = (Scalar‘𝑃))
65fveq2d 6655 . . . 4 (𝑅 ∈ V → (Base‘𝑅) = (Base‘(Scalar‘𝑃)))
7 eqid 2759 . . . . . 6 (1o mPoly 𝑅) = (1o mPoly 𝑅)
8 1on 8112 . . . . . . 7 1o ∈ On
98a1i 11 . . . . . 6 (𝑅 ∈ V → 1o ∈ On)
10 id 22 . . . . . 6 (𝑅 ∈ V → 𝑅 ∈ V)
117, 9, 10mplsca 20761 . . . . 5 (𝑅 ∈ V → 𝑅 = (Scalar‘(1o mPoly 𝑅)))
1211fveq2d 6655 . . . 4 (𝑅 ∈ V → (Base‘𝑅) = (Base‘(Scalar‘(1o mPoly 𝑅))))
13 eqid 2759 . . . . . . 7 ( ·𝑠𝑃) = ( ·𝑠𝑃)
144, 7, 13ply1vsca 20935 . . . . . 6 ( ·𝑠𝑃) = ( ·𝑠 ‘(1o mPoly 𝑅))
1514a1i 11 . . . . 5 (𝑅 ∈ V → ( ·𝑠𝑃) = ( ·𝑠 ‘(1o mPoly 𝑅)))
1615oveqdr 7171 . . . 4 ((𝑅 ∈ V ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ V)) → (𝑥( ·𝑠𝑃)𝑦) = (𝑥( ·𝑠 ‘(1o mPoly 𝑅))𝑦))
17 eqid 2759 . . . . . 6 (1r𝑃) = (1r𝑃)
187, 4, 17ply1mpl1 20966 . . . . 5 (1r𝑃) = (1r‘(1o mPoly 𝑅))
1918a1i 11 . . . 4 (𝑅 ∈ V → (1r𝑃) = (1r‘(1o mPoly 𝑅)))
20 fvexd 6666 . . . 4 (𝑅 ∈ V → (1r𝑃) ∈ V)
212, 3, 6, 12, 16, 19, 20asclpropd 20645 . . 3 (𝑅 ∈ V → (algSc‘𝑃) = (algSc‘(1o mPoly 𝑅)))
22 fvprc 6643 . . . . . 6 𝑅 ∈ V → (Poly1𝑅) = ∅)
234, 22syl5eq 2806 . . . . 5 𝑅 ∈ V → 𝑃 = ∅)
24 reldmmpl 20740 . . . . . 6 Rel dom mPoly
2524ovprc2 7183 . . . . 5 𝑅 ∈ V → (1o mPoly 𝑅) = ∅)
2623, 25eqtr4d 2797 . . . 4 𝑅 ∈ V → 𝑃 = (1o mPoly 𝑅))
2726fveq2d 6655 . . 3 𝑅 ∈ V → (algSc‘𝑃) = (algSc‘(1o mPoly 𝑅)))
2821, 27pm2.61i 185 . 2 (algSc‘𝑃) = (algSc‘(1o mPoly 𝑅))
291, 28eqtri 2782 1 𝐴 = (algSc‘(1o mPoly 𝑅))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ∧ wa 400   = wceq 1539   ∈ wcel 2112  Vcvv 3407  ∅c0 4221  Oncon0 6162  ‘cfv 6328  (class class class)co 7143  1oc1o 8098  Basecbs 16526  Scalarcsca 16611   ·𝑠 cvsca 16612  1rcur 19304  algSccascl 20602   mPoly cmpl 20653  Poly1cpl1 20886 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-rep 5149  ax-sep 5162  ax-nul 5169  ax-pow 5227  ax-pr 5291  ax-un 7452  ax-cnex 10616  ax-resscn 10617  ax-1cn 10618  ax-icn 10619  ax-addcl 10620  ax-addrcl 10621  ax-mulcl 10622  ax-mulrcl 10623  ax-mulcom 10624  ax-addass 10625  ax-mulass 10626  ax-distr 10627  ax-i2m1 10628  ax-1ne0 10629  ax-1rid 10630  ax-rnegex 10631  ax-rrecex 10632  ax-cnre 10633  ax-pre-lttri 10634  ax-pre-lttrn 10635  ax-pre-ltadd 10636  ax-pre-mulgt0 10637 This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2899  df-ne 2950  df-nel 3054  df-ral 3073  df-rex 3074  df-reu 3075  df-rab 3077  df-v 3409  df-sbc 3694  df-csb 3802  df-dif 3857  df-un 3859  df-in 3861  df-ss 3871  df-pss 3873  df-nul 4222  df-if 4414  df-pw 4489  df-sn 4516  df-pr 4518  df-tp 4520  df-op 4522  df-uni 4792  df-int 4832  df-iun 4878  df-br 5026  df-opab 5088  df-mpt 5106  df-tr 5132  df-id 5423  df-eprel 5428  df-po 5436  df-so 5437  df-fr 5476  df-we 5478  df-xp 5523  df-rel 5524  df-cnv 5525  df-co 5526  df-dm 5527  df-rn 5528  df-res 5529  df-ima 5530  df-pred 6119  df-ord 6165  df-on 6166  df-lim 6167  df-suc 6168  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-riota 7101  df-ov 7146  df-oprab 7147  df-mpo 7148  df-of 7398  df-om 7573  df-1st 7686  df-2nd 7687  df-supp 7829  df-wrecs 7950  df-recs 8011  df-rdg 8049  df-1o 8105  df-oadd 8109  df-er 8292  df-map 8411  df-en 8521  df-dom 8522  df-sdom 8523  df-fin 8524  df-fsupp 8852  df-pnf 10700  df-mnf 10701  df-xr 10702  df-ltxr 10703  df-le 10704  df-sub 10895  df-neg 10896  df-nn 11660  df-2 11722  df-3 11723  df-4 11724  df-5 11725  df-6 11726  df-7 11727  df-8 11728  df-9 11729  df-n0 11920  df-z 12006  df-dec 12123  df-uz 12268  df-fz 12925  df-struct 16528  df-ndx 16529  df-slot 16530  df-base 16532  df-sets 16533  df-ress 16534  df-plusg 16621  df-mulr 16622  df-sca 16624  df-vsca 16625  df-tset 16627  df-ple 16628  df-0g 16758  df-mgp 19293  df-ur 19305  df-ascl 20605  df-psr 20656  df-mpl 20658  df-opsr 20660  df-psr1 20889  df-ply1 20891 This theorem is referenced by:  subrg1ascl  20968  subrg1asclcl  20969  evls1sca  21027  evl1sca  21038  pf1ind  21059  deg1le0  24796
 Copyright terms: Public domain W3C validator