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

Theorem pf1mpf 22195
Description: Convert a univariate polynomial function to multivariate. (Contributed by Mario Carneiro, 12-Jun-2015.)
Hypotheses
Ref Expression
pf1rcl.q 𝑄 = ran (eval1𝑅)
pf1f.b 𝐵 = (Base‘𝑅)
mpfpf1.q 𝐸 = ran (1o eval 𝑅)
Assertion
Ref Expression
pf1mpf (𝐹𝑄 → (𝐹 ∘ (𝑥 ∈ (𝐵m 1o) ↦ (𝑥‘∅))) ∈ 𝐸)
Distinct variable groups:   𝑥,𝐵   𝑥,𝐹   𝑥,𝑄   𝑥,𝑅
Allowed substitution hint:   𝐸(𝑥)

Proof of Theorem pf1mpf
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 pf1rcl.q . . 3 𝑄 = ran (eval1𝑅)
21pf1rcl 22192 . 2 (𝐹𝑄𝑅 ∈ CRing)
3 id 22 . . . 4 (𝐹𝑄𝐹𝑄)
43, 1eleqtrdi 2835 . . 3 (𝐹𝑄𝐹 ∈ ran (eval1𝑅))
5 eqid 2724 . . . . . 6 (eval1𝑅) = (eval1𝑅)
6 eqid 2724 . . . . . 6 (Poly1𝑅) = (Poly1𝑅)
7 eqid 2724 . . . . . 6 (𝑅s 𝐵) = (𝑅s 𝐵)
8 pf1f.b . . . . . 6 𝐵 = (Base‘𝑅)
95, 6, 7, 8evl1rhm 22175 . . . . 5 (𝑅 ∈ CRing → (eval1𝑅) ∈ ((Poly1𝑅) RingHom (𝑅s 𝐵)))
102, 9syl 17 . . . 4 (𝐹𝑄 → (eval1𝑅) ∈ ((Poly1𝑅) RingHom (𝑅s 𝐵)))
11 eqid 2724 . . . . 5 (Base‘(Poly1𝑅)) = (Base‘(Poly1𝑅))
12 eqid 2724 . . . . 5 (Base‘(𝑅s 𝐵)) = (Base‘(𝑅s 𝐵))
1311, 12rhmf 20379 . . . 4 ((eval1𝑅) ∈ ((Poly1𝑅) RingHom (𝑅s 𝐵)) → (eval1𝑅):(Base‘(Poly1𝑅))⟶(Base‘(𝑅s 𝐵)))
14 ffn 6708 . . . 4 ((eval1𝑅):(Base‘(Poly1𝑅))⟶(Base‘(𝑅s 𝐵)) → (eval1𝑅) Fn (Base‘(Poly1𝑅)))
15 fvelrnb 6943 . . . 4 ((eval1𝑅) Fn (Base‘(Poly1𝑅)) → (𝐹 ∈ ran (eval1𝑅) ↔ ∃𝑦 ∈ (Base‘(Poly1𝑅))((eval1𝑅)‘𝑦) = 𝐹))
1610, 13, 14, 154syl 19 . . 3 (𝐹𝑄 → (𝐹 ∈ ran (eval1𝑅) ↔ ∃𝑦 ∈ (Base‘(Poly1𝑅))((eval1𝑅)‘𝑦) = 𝐹))
174, 16mpbid 231 . 2 (𝐹𝑄 → ∃𝑦 ∈ (Base‘(Poly1𝑅))((eval1𝑅)‘𝑦) = 𝐹)
18 eqid 2724 . . . . . . . 8 (1o eval 𝑅) = (1o eval 𝑅)
19 eqid 2724 . . . . . . . 8 (1o mPoly 𝑅) = (1o mPoly 𝑅)
20 eqid 2724 . . . . . . . . 9 (PwSer1𝑅) = (PwSer1𝑅)
216, 20, 11ply1bas 22039 . . . . . . . 8 (Base‘(Poly1𝑅)) = (Base‘(1o mPoly 𝑅))
225, 18, 8, 19, 21evl1val 22172 . . . . . . 7 ((𝑅 ∈ CRing ∧ 𝑦 ∈ (Base‘(Poly1𝑅))) → ((eval1𝑅)‘𝑦) = (((1o eval 𝑅)‘𝑦) ∘ (𝑧𝐵 ↦ (1o × {𝑧}))))
2322coeq1d 5852 . . . . . 6 ((𝑅 ∈ CRing ∧ 𝑦 ∈ (Base‘(Poly1𝑅))) → (((eval1𝑅)‘𝑦) ∘ (𝑥 ∈ (𝐵m 1o) ↦ (𝑥‘∅))) = ((((1o eval 𝑅)‘𝑦) ∘ (𝑧𝐵 ↦ (1o × {𝑧}))) ∘ (𝑥 ∈ (𝐵m 1o) ↦ (𝑥‘∅))))
24 coass 6255 . . . . . . 7 ((((1o eval 𝑅)‘𝑦) ∘ (𝑧𝐵 ↦ (1o × {𝑧}))) ∘ (𝑥 ∈ (𝐵m 1o) ↦ (𝑥‘∅))) = (((1o eval 𝑅)‘𝑦) ∘ ((𝑧𝐵 ↦ (1o × {𝑧})) ∘ (𝑥 ∈ (𝐵m 1o) ↦ (𝑥‘∅))))
25 df1o2 8469 . . . . . . . . . . 11 1o = {∅}
268fvexi 6896 . . . . . . . . . . 11 𝐵 ∈ V
27 0ex 5298 . . . . . . . . . . 11 ∅ ∈ V
28 eqid 2724 . . . . . . . . . . 11 (𝑥 ∈ (𝐵m 1o) ↦ (𝑥‘∅)) = (𝑥 ∈ (𝐵m 1o) ↦ (𝑥‘∅))
2925, 26, 27, 28mapsncnv 8884 . . . . . . . . . 10 (𝑥 ∈ (𝐵m 1o) ↦ (𝑥‘∅)) = (𝑧𝐵 ↦ (1o × {𝑧}))
3029coeq1i 5850 . . . . . . . . 9 ((𝑥 ∈ (𝐵m 1o) ↦ (𝑥‘∅)) ∘ (𝑥 ∈ (𝐵m 1o) ↦ (𝑥‘∅))) = ((𝑧𝐵 ↦ (1o × {𝑧})) ∘ (𝑥 ∈ (𝐵m 1o) ↦ (𝑥‘∅)))
3125, 26, 27, 28mapsnf1o2 8885 . . . . . . . . . 10 (𝑥 ∈ (𝐵m 1o) ↦ (𝑥‘∅)):(𝐵m 1o)–1-1-onto𝐵
32 f1ococnv1 6853 . . . . . . . . . 10 ((𝑥 ∈ (𝐵m 1o) ↦ (𝑥‘∅)):(𝐵m 1o)–1-1-onto𝐵 → ((𝑥 ∈ (𝐵m 1o) ↦ (𝑥‘∅)) ∘ (𝑥 ∈ (𝐵m 1o) ↦ (𝑥‘∅))) = ( I ↾ (𝐵m 1o)))
3331, 32mp1i 13 . . . . . . . . 9 ((𝑅 ∈ CRing ∧ 𝑦 ∈ (Base‘(Poly1𝑅))) → ((𝑥 ∈ (𝐵m 1o) ↦ (𝑥‘∅)) ∘ (𝑥 ∈ (𝐵m 1o) ↦ (𝑥‘∅))) = ( I ↾ (𝐵m 1o)))
3430, 33eqtr3id 2778 . . . . . . . 8 ((𝑅 ∈ CRing ∧ 𝑦 ∈ (Base‘(Poly1𝑅))) → ((𝑧𝐵 ↦ (1o × {𝑧})) ∘ (𝑥 ∈ (𝐵m 1o) ↦ (𝑥‘∅))) = ( I ↾ (𝐵m 1o)))
3534coeq2d 5853 . . . . . . 7 ((𝑅 ∈ CRing ∧ 𝑦 ∈ (Base‘(Poly1𝑅))) → (((1o eval 𝑅)‘𝑦) ∘ ((𝑧𝐵 ↦ (1o × {𝑧})) ∘ (𝑥 ∈ (𝐵m 1o) ↦ (𝑥‘∅)))) = (((1o eval 𝑅)‘𝑦) ∘ ( I ↾ (𝐵m 1o))))
3624, 35eqtrid 2776 . . . . . 6 ((𝑅 ∈ CRing ∧ 𝑦 ∈ (Base‘(Poly1𝑅))) → ((((1o eval 𝑅)‘𝑦) ∘ (𝑧𝐵 ↦ (1o × {𝑧}))) ∘ (𝑥 ∈ (𝐵m 1o) ↦ (𝑥‘∅))) = (((1o eval 𝑅)‘𝑦) ∘ ( I ↾ (𝐵m 1o))))
37 eqid 2724 . . . . . . . 8 (𝑅s (𝐵m 1o)) = (𝑅s (𝐵m 1o))
38 eqid 2724 . . . . . . . 8 (Base‘(𝑅s (𝐵m 1o))) = (Base‘(𝑅s (𝐵m 1o)))
39 simpl 482 . . . . . . . 8 ((𝑅 ∈ CRing ∧ 𝑦 ∈ (Base‘(Poly1𝑅))) → 𝑅 ∈ CRing)
40 ovexd 7437 . . . . . . . 8 ((𝑅 ∈ CRing ∧ 𝑦 ∈ (Base‘(Poly1𝑅))) → (𝐵m 1o) ∈ V)
41 1on 8474 . . . . . . . . . . 11 1o ∈ On
4218, 8, 19, 37evlrhm 21971 . . . . . . . . . . 11 ((1o ∈ On ∧ 𝑅 ∈ CRing) → (1o eval 𝑅) ∈ ((1o mPoly 𝑅) RingHom (𝑅s (𝐵m 1o))))
4341, 42mpan 687 . . . . . . . . . 10 (𝑅 ∈ CRing → (1o eval 𝑅) ∈ ((1o mPoly 𝑅) RingHom (𝑅s (𝐵m 1o))))
4421, 38rhmf 20379 . . . . . . . . . 10 ((1o eval 𝑅) ∈ ((1o mPoly 𝑅) RingHom (𝑅s (𝐵m 1o))) → (1o eval 𝑅):(Base‘(Poly1𝑅))⟶(Base‘(𝑅s (𝐵m 1o))))
4543, 44syl 17 . . . . . . . . 9 (𝑅 ∈ CRing → (1o eval 𝑅):(Base‘(Poly1𝑅))⟶(Base‘(𝑅s (𝐵m 1o))))
4645ffvelcdmda 7077 . . . . . . . 8 ((𝑅 ∈ CRing ∧ 𝑦 ∈ (Base‘(Poly1𝑅))) → ((1o eval 𝑅)‘𝑦) ∈ (Base‘(𝑅s (𝐵m 1o))))
4737, 8, 38, 39, 40, 46pwselbas 17436 . . . . . . 7 ((𝑅 ∈ CRing ∧ 𝑦 ∈ (Base‘(Poly1𝑅))) → ((1o eval 𝑅)‘𝑦):(𝐵m 1o)⟶𝐵)
48 fcoi1 6756 . . . . . . 7 (((1o eval 𝑅)‘𝑦):(𝐵m 1o)⟶𝐵 → (((1o eval 𝑅)‘𝑦) ∘ ( I ↾ (𝐵m 1o))) = ((1o eval 𝑅)‘𝑦))
4947, 48syl 17 . . . . . 6 ((𝑅 ∈ CRing ∧ 𝑦 ∈ (Base‘(Poly1𝑅))) → (((1o eval 𝑅)‘𝑦) ∘ ( I ↾ (𝐵m 1o))) = ((1o eval 𝑅)‘𝑦))
5023, 36, 493eqtrd 2768 . . . . 5 ((𝑅 ∈ CRing ∧ 𝑦 ∈ (Base‘(Poly1𝑅))) → (((eval1𝑅)‘𝑦) ∘ (𝑥 ∈ (𝐵m 1o) ↦ (𝑥‘∅))) = ((1o eval 𝑅)‘𝑦))
5145ffnd 6709 . . . . . . 7 (𝑅 ∈ CRing → (1o eval 𝑅) Fn (Base‘(Poly1𝑅)))
52 fnfvelrn 7073 . . . . . . 7 (((1o eval 𝑅) Fn (Base‘(Poly1𝑅)) ∧ 𝑦 ∈ (Base‘(Poly1𝑅))) → ((1o eval 𝑅)‘𝑦) ∈ ran (1o eval 𝑅))
5351, 52sylan 579 . . . . . 6 ((𝑅 ∈ CRing ∧ 𝑦 ∈ (Base‘(Poly1𝑅))) → ((1o eval 𝑅)‘𝑦) ∈ ran (1o eval 𝑅))
54 mpfpf1.q . . . . . 6 𝐸 = ran (1o eval 𝑅)
5553, 54eleqtrrdi 2836 . . . . 5 ((𝑅 ∈ CRing ∧ 𝑦 ∈ (Base‘(Poly1𝑅))) → ((1o eval 𝑅)‘𝑦) ∈ 𝐸)
5650, 55eqeltrd 2825 . . . 4 ((𝑅 ∈ CRing ∧ 𝑦 ∈ (Base‘(Poly1𝑅))) → (((eval1𝑅)‘𝑦) ∘ (𝑥 ∈ (𝐵m 1o) ↦ (𝑥‘∅))) ∈ 𝐸)
57 coeq1 5848 . . . . 5 (((eval1𝑅)‘𝑦) = 𝐹 → (((eval1𝑅)‘𝑦) ∘ (𝑥 ∈ (𝐵m 1o) ↦ (𝑥‘∅))) = (𝐹 ∘ (𝑥 ∈ (𝐵m 1o) ↦ (𝑥‘∅))))
5857eleq1d 2810 . . . 4 (((eval1𝑅)‘𝑦) = 𝐹 → ((((eval1𝑅)‘𝑦) ∘ (𝑥 ∈ (𝐵m 1o) ↦ (𝑥‘∅))) ∈ 𝐸 ↔ (𝐹 ∘ (𝑥 ∈ (𝐵m 1o) ↦ (𝑥‘∅))) ∈ 𝐸))
5956, 58syl5ibcom 244 . . 3 ((𝑅 ∈ CRing ∧ 𝑦 ∈ (Base‘(Poly1𝑅))) → (((eval1𝑅)‘𝑦) = 𝐹 → (𝐹 ∘ (𝑥 ∈ (𝐵m 1o) ↦ (𝑥‘∅))) ∈ 𝐸))
6059rexlimdva 3147 . 2 (𝑅 ∈ CRing → (∃𝑦 ∈ (Base‘(Poly1𝑅))((eval1𝑅)‘𝑦) = 𝐹 → (𝐹 ∘ (𝑥 ∈ (𝐵m 1o) ↦ (𝑥‘∅))) ∈ 𝐸))
612, 17, 60sylc 65 1 (𝐹𝑄 → (𝐹 ∘ (𝑥 ∈ (𝐵m 1o) ↦ (𝑥‘∅))) ∈ 𝐸)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395   = wceq 1533  wcel 2098  wrex 3062  Vcvv 3466  c0 4315  {csn 4621  cmpt 5222   I cid 5564   × cxp 5665  ccnv 5666  ran crn 5668  cres 5669  ccom 5671  Oncon0 6355   Fn wfn 6529  wf 6530  1-1-ontowf1o 6533  cfv 6534  (class class class)co 7402  1oc1o 8455  m cmap 8817  Basecbs 17145  s cpws 17393  CRingccrg 20131   RingHom crh 20363   mPoly cmpl 21770   eval cevl 21946  PwSer1cps1 22019  Poly1cpl1 22021  eval1ce1 22157
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5276  ax-sep 5290  ax-nul 5297  ax-pow 5354  ax-pr 5418  ax-un 7719  ax-cnex 11163  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-mulcom 11171  ax-addass 11172  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1ne0 11176  ax-1rid 11177  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182  ax-pre-ltadd 11183  ax-pre-mulgt0 11184
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3771  df-csb 3887  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-pss 3960  df-nul 4316  df-if 4522  df-pw 4597  df-sn 4622  df-pr 4624  df-tp 4626  df-op 4628  df-uni 4901  df-int 4942  df-iun 4990  df-iin 4991  df-br 5140  df-opab 5202  df-mpt 5223  df-tr 5257  df-id 5565  df-eprel 5571  df-po 5579  df-so 5580  df-fr 5622  df-se 5623  df-we 5624  df-xp 5673  df-rel 5674  df-cnv 5675  df-co 5676  df-dm 5677  df-rn 5678  df-res 5679  df-ima 5680  df-pred 6291  df-ord 6358  df-on 6359  df-lim 6360  df-suc 6361  df-iota 6486  df-fun 6536  df-fn 6537  df-f 6538  df-f1 6539  df-fo 6540  df-f1o 6541  df-fv 6542  df-isom 6543  df-riota 7358  df-ov 7405  df-oprab 7406  df-mpo 7407  df-of 7664  df-ofr 7665  df-om 7850  df-1st 7969  df-2nd 7970  df-supp 8142  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-1o 8462  df-er 8700  df-map 8819  df-pm 8820  df-ixp 8889  df-en 8937  df-dom 8938  df-sdom 8939  df-fin 8940  df-fsupp 9359  df-sup 9434  df-oi 9502  df-card 9931  df-pnf 11248  df-mnf 11249  df-xr 11250  df-ltxr 11251  df-le 11252  df-sub 11444  df-neg 11445  df-nn 12211  df-2 12273  df-3 12274  df-4 12275  df-5 12276  df-6 12277  df-7 12278  df-8 12279  df-9 12280  df-n0 12471  df-z 12557  df-dec 12676  df-uz 12821  df-fz 13483  df-fzo 13626  df-seq 13965  df-hash 14289  df-struct 17081  df-sets 17098  df-slot 17116  df-ndx 17128  df-base 17146  df-ress 17175  df-plusg 17211  df-mulr 17212  df-sca 17214  df-vsca 17215  df-ip 17216  df-tset 17217  df-ple 17218  df-ds 17220  df-hom 17222  df-cco 17223  df-0g 17388  df-gsum 17389  df-prds 17394  df-pws 17396  df-mre 17531  df-mrc 17532  df-acs 17534  df-mgm 18565  df-sgrp 18644  df-mnd 18660  df-mhm 18705  df-submnd 18706  df-grp 18858  df-minusg 18859  df-sbg 18860  df-mulg 18988  df-subg 19042  df-ghm 19131  df-cntz 19225  df-cmn 19694  df-abl 19695  df-mgp 20032  df-rng 20050  df-ur 20079  df-srg 20084  df-ring 20132  df-cring 20133  df-rhm 20366  df-subrng 20438  df-subrg 20463  df-lmod 20700  df-lss 20771  df-lsp 20811  df-assa 21718  df-asp 21719  df-ascl 21720  df-psr 21773  df-mvr 21774  df-mpl 21775  df-opsr 21777  df-evls 21947  df-evl 21948  df-psr1 22024  df-ply1 22026  df-evl1 22159
This theorem is referenced by:  pf1ind  22198
  Copyright terms: Public domain W3C validator