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

Theorem offval2 6956
Description: The function operation expressed as a mapping. (Contributed by Mario Carneiro, 20-Jul-2014.)
Hypotheses
Ref Expression
offval2.1 (𝜑𝐴𝑉)
offval2.2 ((𝜑𝑥𝐴) → 𝐵𝑊)
offval2.3 ((𝜑𝑥𝐴) → 𝐶𝑋)
offval2.4 (𝜑𝐹 = (𝑥𝐴𝐵))
offval2.5 (𝜑𝐺 = (𝑥𝐴𝐶))
Assertion
Ref Expression
offval2 (𝜑 → (𝐹𝑓 𝑅𝐺) = (𝑥𝐴 ↦ (𝐵𝑅𝐶)))
Distinct variable groups:   𝑥,𝐴   𝜑,𝑥   𝑥,𝑅
Allowed substitution hints:   𝐵(𝑥)   𝐶(𝑥)   𝐹(𝑥)   𝐺(𝑥)   𝑉(𝑥)   𝑊(𝑥)   𝑋(𝑥)

Proof of Theorem offval2
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 offval2.2 . . . . . 6 ((𝜑𝑥𝐴) → 𝐵𝑊)
21ralrimiva 2995 . . . . 5 (𝜑 → ∀𝑥𝐴 𝐵𝑊)
3 eqid 2651 . . . . . 6 (𝑥𝐴𝐵) = (𝑥𝐴𝐵)
43fnmpt 6058 . . . . 5 (∀𝑥𝐴 𝐵𝑊 → (𝑥𝐴𝐵) Fn 𝐴)
52, 4syl 17 . . . 4 (𝜑 → (𝑥𝐴𝐵) Fn 𝐴)
6 offval2.4 . . . . 5 (𝜑𝐹 = (𝑥𝐴𝐵))
76fneq1d 6019 . . . 4 (𝜑 → (𝐹 Fn 𝐴 ↔ (𝑥𝐴𝐵) Fn 𝐴))
85, 7mpbird 247 . . 3 (𝜑𝐹 Fn 𝐴)
9 offval2.3 . . . . . 6 ((𝜑𝑥𝐴) → 𝐶𝑋)
109ralrimiva 2995 . . . . 5 (𝜑 → ∀𝑥𝐴 𝐶𝑋)
11 eqid 2651 . . . . . 6 (𝑥𝐴𝐶) = (𝑥𝐴𝐶)
1211fnmpt 6058 . . . . 5 (∀𝑥𝐴 𝐶𝑋 → (𝑥𝐴𝐶) Fn 𝐴)
1310, 12syl 17 . . . 4 (𝜑 → (𝑥𝐴𝐶) Fn 𝐴)
14 offval2.5 . . . . 5 (𝜑𝐺 = (𝑥𝐴𝐶))
1514fneq1d 6019 . . . 4 (𝜑 → (𝐺 Fn 𝐴 ↔ (𝑥𝐴𝐶) Fn 𝐴))
1613, 15mpbird 247 . . 3 (𝜑𝐺 Fn 𝐴)
17 offval2.1 . . 3 (𝜑𝐴𝑉)
18 inidm 3855 . . 3 (𝐴𝐴) = 𝐴
196adantr 480 . . . 4 ((𝜑𝑦𝐴) → 𝐹 = (𝑥𝐴𝐵))
2019fveq1d 6231 . . 3 ((𝜑𝑦𝐴) → (𝐹𝑦) = ((𝑥𝐴𝐵)‘𝑦))
2114adantr 480 . . . 4 ((𝜑𝑦𝐴) → 𝐺 = (𝑥𝐴𝐶))
2221fveq1d 6231 . . 3 ((𝜑𝑦𝐴) → (𝐺𝑦) = ((𝑥𝐴𝐶)‘𝑦))
238, 16, 17, 17, 18, 20, 22offval 6946 . 2 (𝜑 → (𝐹𝑓 𝑅𝐺) = (𝑦𝐴 ↦ (((𝑥𝐴𝐵)‘𝑦)𝑅((𝑥𝐴𝐶)‘𝑦))))
24 nffvmpt1 6237 . . . . 5 𝑥((𝑥𝐴𝐵)‘𝑦)
25 nfcv 2793 . . . . 5 𝑥𝑅
26 nffvmpt1 6237 . . . . 5 𝑥((𝑥𝐴𝐶)‘𝑦)
2724, 25, 26nfov 6716 . . . 4 𝑥(((𝑥𝐴𝐵)‘𝑦)𝑅((𝑥𝐴𝐶)‘𝑦))
28 nfcv 2793 . . . 4 𝑦(((𝑥𝐴𝐵)‘𝑥)𝑅((𝑥𝐴𝐶)‘𝑥))
29 fveq2 6229 . . . . 5 (𝑦 = 𝑥 → ((𝑥𝐴𝐵)‘𝑦) = ((𝑥𝐴𝐵)‘𝑥))
30 fveq2 6229 . . . . 5 (𝑦 = 𝑥 → ((𝑥𝐴𝐶)‘𝑦) = ((𝑥𝐴𝐶)‘𝑥))
3129, 30oveq12d 6708 . . . 4 (𝑦 = 𝑥 → (((𝑥𝐴𝐵)‘𝑦)𝑅((𝑥𝐴𝐶)‘𝑦)) = (((𝑥𝐴𝐵)‘𝑥)𝑅((𝑥𝐴𝐶)‘𝑥)))
3227, 28, 31cbvmpt 4782 . . 3 (𝑦𝐴 ↦ (((𝑥𝐴𝐵)‘𝑦)𝑅((𝑥𝐴𝐶)‘𝑦))) = (𝑥𝐴 ↦ (((𝑥𝐴𝐵)‘𝑥)𝑅((𝑥𝐴𝐶)‘𝑥)))
33 simpr 476 . . . . . 6 ((𝜑𝑥𝐴) → 𝑥𝐴)
343fvmpt2 6330 . . . . . 6 ((𝑥𝐴𝐵𝑊) → ((𝑥𝐴𝐵)‘𝑥) = 𝐵)
3533, 1, 34syl2anc 694 . . . . 5 ((𝜑𝑥𝐴) → ((𝑥𝐴𝐵)‘𝑥) = 𝐵)
3611fvmpt2 6330 . . . . . 6 ((𝑥𝐴𝐶𝑋) → ((𝑥𝐴𝐶)‘𝑥) = 𝐶)
3733, 9, 36syl2anc 694 . . . . 5 ((𝜑𝑥𝐴) → ((𝑥𝐴𝐶)‘𝑥) = 𝐶)
3835, 37oveq12d 6708 . . . 4 ((𝜑𝑥𝐴) → (((𝑥𝐴𝐵)‘𝑥)𝑅((𝑥𝐴𝐶)‘𝑥)) = (𝐵𝑅𝐶))
3938mpteq2dva 4777 . . 3 (𝜑 → (𝑥𝐴 ↦ (((𝑥𝐴𝐵)‘𝑥)𝑅((𝑥𝐴𝐶)‘𝑥))) = (𝑥𝐴 ↦ (𝐵𝑅𝐶)))
4032, 39syl5eq 2697 . 2 (𝜑 → (𝑦𝐴 ↦ (((𝑥𝐴𝐵)‘𝑦)𝑅((𝑥𝐴𝐶)‘𝑦))) = (𝑥𝐴 ↦ (𝐵𝑅𝐶)))
4123, 40eqtrd 2685 1 (𝜑 → (𝐹𝑓 𝑅𝐺) = (𝑥𝐴 ↦ (𝐵𝑅𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1523  wcel 2030  wral 2941  cmpt 4762   Fn wfn 5921  cfv 5926  (class class class)co 6690  𝑓 cof 6937
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-of 6939
This theorem is referenced by:  ofmpteq  6958  ofc12  6964  caofinvl  6966  caofcom  6971  caofass  6973  caofdi  6975  caofdir  6976  caonncan  6977  offval22  7298  ofccat  13754  ofs1  13755  o1add2  14398  o1mul2  14399  o1sub2  14400  o1dif  14404  fsumo1  14588  pwsplusgval  16197  pwsmulrval  16198  pwsvscafval  16201  pwsco1mhm  17417  pwsco2mhm  17418  pwssub  17576  gsumzaddlem  18367  gsummptfsadd  18370  gsummptfidmadd2  18372  gsumzsplit  18373  gsumsub  18394  gsummptfssub  18395  dprdfadd  18465  dprdfsub  18466  dprdfeq0  18467  dprdf11  18468  lmhmvsca  19093  rrgsupp  19339  psrbagaddcl  19418  psrass1lem  19425  psrlinv  19445  psrass1  19453  psrdi  19454  psrdir  19455  psrass23l  19456  psrcom  19457  psrass23  19458  mplsubrglem  19487  mplmonmul  19512  mplcoe1  19513  mplcoe3  19514  mplcoe5  19516  mplmon2  19541  evlslem1  19563  coe1sclmul  19700  coe1sclmul2  19702  uvcresum  20180  grpvrinv  20250  mhmvlin  20251  mamudi  20257  mamudir  20258  mdetunilem9  20474  tsmssub  21999  tgptsmscls  22000  tsmssplit  22002  tsmsxplem2  22004  ovolctb  23304  mbfmulc2re  23460  mbfneg  23462  mbfadd  23473  mbfsub  23474  mbfmulc2  23475  mbfmul  23538  itg2const  23552  itg2mulclem  23558  itg2mulc  23559  itg2splitlem  23560  itg2monolem1  23562  i1fibl  23619  itgitg1  23620  ibladdlem  23631  ibladd  23632  itgaddlem1  23634  iblabslem  23639  iblabs  23640  iblmulc2  23642  itgmulc2lem1  23643  bddmulibl  23650  dvmulf  23751  dvcmulf  23753  dvcof  23756  dvexp  23761  dvmptadd  23768  dvmptmul  23769  dvmptco  23780  dvef  23788  dv11cn  23809  itgsubstlem  23856  mdegmullem  23883  plypf1  24013  plyaddlem1  24014  plymullem1  24015  plyco  24042  dgrcolem1  24074  dgrcolem2  24075  plydiveu  24098  plyremlem  24104  elqaalem3  24121  iaa  24125  taylply2  24167  ulmdvlem1  24199  iblulm  24206  jensenlem2  24759  amgmlem  24761  ftalem7  24850  basellem8  24859  basellem9  24860  dchrmulid2  25022  dchrinvcl  25023  dchrfi  25025  lgseisenlem3  25147  lgseisenlem4  25148  chtppilimlem2  25208  chebbnd2  25211  chto1lb  25212  chpchtlim  25213  chpo1ub  25214  vmadivsum  25216  rpvmasumlem  25221  mudivsum  25264  selberglem1  25279  selberglem2  25280  selberg2lem  25284  selberg2  25285  pntrsumo1  25299  selbergr  25302  ofoprabco  29592  pl1cn  30129  esumadd  30247  poimirlem16  33555  poimirlem19  33558  itg2addnclem  33591  itg2addnclem3  33593  ibladdnclem  33596  itgaddnclem1  33598  iblabsnclem  33603  iblabsnc  33604  iblmulc2nc  33605  itgmulc2nclem1  33606  itgmulc2nclem2  33607  itgmulc2nc  33608  itgabsnc  33609  ftc1anclem3  33617  ftc1anclem4  33618  ftc1anclem5  33619  ftc1anclem6  33620  ftc1anclem7  33621  ftc1anclem8  33622  mendlmod  38080  mendassa  38081  expgrowthi  38849  expgrowth  38851  binomcxplemrat  38866  mulcncff  40399  subcncff  40411  addcncff  40415  divcncff  40422  dvsubf  40446  dvdivf  40455  fourierdlem16  40658  fourierdlem21  40663  fourierdlem22  40664  fourierdlem58  40699  fourierdlem59  40700  fourierdlem72  40713  fourierdlem83  40724  offvalfv  42446  aacllem  42875  amgmwlem  42876  amgmlemALT  42877
  Copyright terms: Public domain W3C validator