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

Theorem offval2 7416
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 (𝜑 → (𝐹f 𝑅𝐺) = (𝑥𝐴 ↦ (𝐵𝑅𝐶)))
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 3187 . . . . 5 (𝜑 → ∀𝑥𝐴 𝐵𝑊)
3 eqid 2826 . . . . . 6 (𝑥𝐴𝐵) = (𝑥𝐴𝐵)
43fnmpt 6485 . . . . 5 (∀𝑥𝐴 𝐵𝑊 → (𝑥𝐴𝐵) Fn 𝐴)
52, 4syl 17 . . . 4 (𝜑 → (𝑥𝐴𝐵) Fn 𝐴)
6 offval2.4 . . . . 5 (𝜑𝐹 = (𝑥𝐴𝐵))
76fneq1d 6443 . . . 4 (𝜑 → (𝐹 Fn 𝐴 ↔ (𝑥𝐴𝐵) Fn 𝐴))
85, 7mpbird 258 . . 3 (𝜑𝐹 Fn 𝐴)
9 offval2.3 . . . . . 6 ((𝜑𝑥𝐴) → 𝐶𝑋)
109ralrimiva 3187 . . . . 5 (𝜑 → ∀𝑥𝐴 𝐶𝑋)
11 eqid 2826 . . . . . 6 (𝑥𝐴𝐶) = (𝑥𝐴𝐶)
1211fnmpt 6485 . . . . 5 (∀𝑥𝐴 𝐶𝑋 → (𝑥𝐴𝐶) Fn 𝐴)
1310, 12syl 17 . . . 4 (𝜑 → (𝑥𝐴𝐶) Fn 𝐴)
14 offval2.5 . . . . 5 (𝜑𝐺 = (𝑥𝐴𝐶))
1514fneq1d 6443 . . . 4 (𝜑 → (𝐺 Fn 𝐴 ↔ (𝑥𝐴𝐶) Fn 𝐴))
1613, 15mpbird 258 . . 3 (𝜑𝐺 Fn 𝐴)
17 offval2.1 . . 3 (𝜑𝐴𝑉)
18 inidm 4199 . . 3 (𝐴𝐴) = 𝐴
196adantr 481 . . . 4 ((𝜑𝑦𝐴) → 𝐹 = (𝑥𝐴𝐵))
2019fveq1d 6669 . . 3 ((𝜑𝑦𝐴) → (𝐹𝑦) = ((𝑥𝐴𝐵)‘𝑦))
2114adantr 481 . . . 4 ((𝜑𝑦𝐴) → 𝐺 = (𝑥𝐴𝐶))
2221fveq1d 6669 . . 3 ((𝜑𝑦𝐴) → (𝐺𝑦) = ((𝑥𝐴𝐶)‘𝑦))
238, 16, 17, 17, 18, 20, 22offval 7406 . 2 (𝜑 → (𝐹f 𝑅𝐺) = (𝑦𝐴 ↦ (((𝑥𝐴𝐵)‘𝑦)𝑅((𝑥𝐴𝐶)‘𝑦))))
24 nffvmpt1 6678 . . . . 5 𝑥((𝑥𝐴𝐵)‘𝑦)
25 nfcv 2982 . . . . 5 𝑥𝑅
26 nffvmpt1 6678 . . . . 5 𝑥((𝑥𝐴𝐶)‘𝑦)
2724, 25, 26nfov 7178 . . . 4 𝑥(((𝑥𝐴𝐵)‘𝑦)𝑅((𝑥𝐴𝐶)‘𝑦))
28 nfcv 2982 . . . 4 𝑦(((𝑥𝐴𝐵)‘𝑥)𝑅((𝑥𝐴𝐶)‘𝑥))
29 fveq2 6667 . . . . 5 (𝑦 = 𝑥 → ((𝑥𝐴𝐵)‘𝑦) = ((𝑥𝐴𝐵)‘𝑥))
30 fveq2 6667 . . . . 5 (𝑦 = 𝑥 → ((𝑥𝐴𝐶)‘𝑦) = ((𝑥𝐴𝐶)‘𝑥))
3129, 30oveq12d 7166 . . . 4 (𝑦 = 𝑥 → (((𝑥𝐴𝐵)‘𝑦)𝑅((𝑥𝐴𝐶)‘𝑦)) = (((𝑥𝐴𝐵)‘𝑥)𝑅((𝑥𝐴𝐶)‘𝑥)))
3227, 28, 31cbvmpt 5164 . . 3 (𝑦𝐴 ↦ (((𝑥𝐴𝐵)‘𝑦)𝑅((𝑥𝐴𝐶)‘𝑦))) = (𝑥𝐴 ↦ (((𝑥𝐴𝐵)‘𝑥)𝑅((𝑥𝐴𝐶)‘𝑥)))
33 simpr 485 . . . . . 6 ((𝜑𝑥𝐴) → 𝑥𝐴)
343fvmpt2 6775 . . . . . 6 ((𝑥𝐴𝐵𝑊) → ((𝑥𝐴𝐵)‘𝑥) = 𝐵)
3533, 1, 34syl2anc 584 . . . . 5 ((𝜑𝑥𝐴) → ((𝑥𝐴𝐵)‘𝑥) = 𝐵)
3611fvmpt2 6775 . . . . . 6 ((𝑥𝐴𝐶𝑋) → ((𝑥𝐴𝐶)‘𝑥) = 𝐶)
3733, 9, 36syl2anc 584 . . . . 5 ((𝜑𝑥𝐴) → ((𝑥𝐴𝐶)‘𝑥) = 𝐶)
3835, 37oveq12d 7166 . . . 4 ((𝜑𝑥𝐴) → (((𝑥𝐴𝐵)‘𝑥)𝑅((𝑥𝐴𝐶)‘𝑥)) = (𝐵𝑅𝐶))
3938mpteq2dva 5158 . . 3 (𝜑 → (𝑥𝐴 ↦ (((𝑥𝐴𝐵)‘𝑥)𝑅((𝑥𝐴𝐶)‘𝑥))) = (𝑥𝐴 ↦ (𝐵𝑅𝐶)))
4032, 39syl5eq 2873 . 2 (𝜑 → (𝑦𝐴 ↦ (((𝑥𝐴𝐵)‘𝑦)𝑅((𝑥𝐴𝐶)‘𝑦))) = (𝑥𝐴 ↦ (𝐵𝑅𝐶)))
4123, 40eqtrd 2861 1 (𝜑 → (𝐹f 𝑅𝐺) = (𝑥𝐴 ↦ (𝐵𝑅𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1530  wcel 2107  wral 3143  cmpt 5143   Fn wfn 6347  cfv 6352  (class class class)co 7148  f cof 7397
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 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-rep 5187  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5326
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-ral 3148  df-rex 3149  df-reu 3150  df-rab 3152  df-v 3502  df-sbc 3777  df-csb 3888  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4838  df-iun 4919  df-br 5064  df-opab 5126  df-mpt 5144  df-id 5459  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-iota 6312  df-fun 6354  df-fn 6355  df-f 6356  df-f1 6357  df-fo 6358  df-f1o 6359  df-fv 6360  df-ov 7151  df-oprab 7152  df-mpo 7153  df-of 7399
This theorem is referenced by:  ofmpteq  7418  ofc12  7424  caofinvl  7426  caofcom  7431  caofass  7433  caofdi  7435  caofdir  7436  caonncan  7437  offval22  7774  ofccat  14319  ofs1  14320  o1add2  14970  o1mul2  14971  o1sub2  14972  o1dif  14976  fsumo1  15157  pwsplusgval  16753  pwsmulrval  16754  pwsvscafval  16757  pwsco1mhm  17979  pwsco2mhm  17980  pwssub  18143  gsumzaddlem  18961  gsummptfsadd  18964  gsummptfidmadd2  18966  gsumzsplit  18967  gsumsub  18988  gsummptfssub  18989  dprdfadd  19062  dprdfsub  19063  dprdfeq0  19064  dprdf11  19065  lmhmvsca  19737  rrgsupp  19983  psrbagaddcl  20069  psrass1lem  20076  psrlinv  20096  psrass1  20104  psrdi  20105  psrdir  20106  psrass23l  20107  psrcom  20108  psrass23  20109  mplsubrglem  20138  mplmonmul  20163  mplcoe1  20164  mplcoe3  20165  mplcoe5  20167  mplmon2  20191  evlslem1  20213  coe1sclmul  20367  coe1sclmul2  20369  uvcresum  20853  grpvrinv  20923  mhmvlin  20924  mamudi  20928  mamudir  20929  mdetunilem9  21145  tsmssub  22672  tgptsmscls  22673  tsmssplit  22675  tsmsxplem2  22677  ovolctb  24006  mbfmulc2re  24164  mbfneg  24166  mbfadd  24177  mbfsub  24178  mbfmulc2  24179  mbfmul  24242  itg2const  24256  itg2mulclem  24262  itg2mulc  24263  itg2splitlem  24264  itg2monolem1  24266  i1fibl  24323  itgitg1  24324  ibladdlem  24335  ibladd  24336  itgaddlem1  24338  iblabslem  24343  iblabs  24344  iblmulc2  24346  itgmulc2lem1  24347  bddmulibl  24354  dvmulf  24455  dvcmulf  24457  dvcof  24460  dvexp  24465  dvmptadd  24472  dvmptmul  24473  dvmptco  24484  dvef  24492  dv11cn  24513  itgsubstlem  24560  mdegmullem  24587  plypf1  24717  plyaddlem1  24718  plymullem1  24719  plyco  24746  dgrcolem1  24778  dgrcolem2  24779  plydiveu  24802  plyremlem  24808  elqaalem3  24825  iaa  24829  taylply2  24871  ulmdvlem1  24903  iblulm  24910  jensenlem2  25479  amgmlem  25481  ftalem7  25570  basellem8  25579  basellem9  25580  dchrmulid2  25742  dchrinvcl  25743  dchrfi  25745  lgseisenlem3  25867  lgseisenlem4  25868  chtppilimlem2  25964  chebbnd2  25967  chto1lb  25968  chpchtlim  25969  chpo1ub  25970  vmadivsum  25972  rpvmasumlem  25977  mudivsum  26020  selberglem1  26035  selberglem2  26036  selberg2lem  26040  selberg2  26041  pntrsumo1  26055  selbergr  26058  ofoprabco  30324  pl1cn  31084  esumadd  31202  poimirlem16  34775  poimirlem19  34778  itg2addnclem  34810  itg2addnclem3  34812  ibladdnclem  34815  itgaddnclem1  34817  iblabsnclem  34822  iblabsnc  34823  iblmulc2nc  34824  itgmulc2nclem1  34825  itgmulc2nclem2  34826  itgmulc2nc  34827  itgabsnc  34828  ftc1anclem3  34836  ftc1anclem4  34837  ftc1anclem5  34838  ftc1anclem6  34839  ftc1anclem7  34840  ftc1anclem8  34841  mendlmod  39658  mendassa  39659  expgrowthi  40530  expgrowth  40532  binomcxplemrat  40547  mulcncff  42016  subcncff  42028  addcncff  42032  divcncff  42039  dvsubf  42063  dvdivf  42072  fourierdlem16  42274  fourierdlem21  42279  fourierdlem22  42280  fourierdlem58  42315  fourierdlem59  42316  fourierdlem72  42329  fourierdlem83  42340  offvalfv  44223  aacllem  44734  amgmwlem  44735  amgmlemALT  44736
  Copyright terms: Public domain W3C validator