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

Theorem offval2 7114
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 3113 . . . . 5 (𝜑 → ∀𝑥𝐴 𝐵𝑊)
3 eqid 2765 . . . . . 6 (𝑥𝐴𝐵) = (𝑥𝐴𝐵)
43fnmpt 6200 . . . . 5 (∀𝑥𝐴 𝐵𝑊 → (𝑥𝐴𝐵) Fn 𝐴)
52, 4syl 17 . . . 4 (𝜑 → (𝑥𝐴𝐵) Fn 𝐴)
6 offval2.4 . . . . 5 (𝜑𝐹 = (𝑥𝐴𝐵))
76fneq1d 6161 . . . 4 (𝜑 → (𝐹 Fn 𝐴 ↔ (𝑥𝐴𝐵) Fn 𝐴))
85, 7mpbird 248 . . 3 (𝜑𝐹 Fn 𝐴)
9 offval2.3 . . . . . 6 ((𝜑𝑥𝐴) → 𝐶𝑋)
109ralrimiva 3113 . . . . 5 (𝜑 → ∀𝑥𝐴 𝐶𝑋)
11 eqid 2765 . . . . . 6 (𝑥𝐴𝐶) = (𝑥𝐴𝐶)
1211fnmpt 6200 . . . . 5 (∀𝑥𝐴 𝐶𝑋 → (𝑥𝐴𝐶) Fn 𝐴)
1310, 12syl 17 . . . 4 (𝜑 → (𝑥𝐴𝐶) Fn 𝐴)
14 offval2.5 . . . . 5 (𝜑𝐺 = (𝑥𝐴𝐶))
1514fneq1d 6161 . . . 4 (𝜑 → (𝐺 Fn 𝐴 ↔ (𝑥𝐴𝐶) Fn 𝐴))
1613, 15mpbird 248 . . 3 (𝜑𝐺 Fn 𝐴)
17 offval2.1 . . 3 (𝜑𝐴𝑉)
18 inidm 3984 . . 3 (𝐴𝐴) = 𝐴
196adantr 472 . . . 4 ((𝜑𝑦𝐴) → 𝐹 = (𝑥𝐴𝐵))
2019fveq1d 6379 . . 3 ((𝜑𝑦𝐴) → (𝐹𝑦) = ((𝑥𝐴𝐵)‘𝑦))
2114adantr 472 . . . 4 ((𝜑𝑦𝐴) → 𝐺 = (𝑥𝐴𝐶))
2221fveq1d 6379 . . 3 ((𝜑𝑦𝐴) → (𝐺𝑦) = ((𝑥𝐴𝐶)‘𝑦))
238, 16, 17, 17, 18, 20, 22offval 7104 . 2 (𝜑 → (𝐹𝑓 𝑅𝐺) = (𝑦𝐴 ↦ (((𝑥𝐴𝐵)‘𝑦)𝑅((𝑥𝐴𝐶)‘𝑦))))
24 nffvmpt1 6388 . . . . 5 𝑥((𝑥𝐴𝐵)‘𝑦)
25 nfcv 2907 . . . . 5 𝑥𝑅
26 nffvmpt1 6388 . . . . 5 𝑥((𝑥𝐴𝐶)‘𝑦)
2724, 25, 26nfov 6874 . . . 4 𝑥(((𝑥𝐴𝐵)‘𝑦)𝑅((𝑥𝐴𝐶)‘𝑦))
28 nfcv 2907 . . . 4 𝑦(((𝑥𝐴𝐵)‘𝑥)𝑅((𝑥𝐴𝐶)‘𝑥))
29 fveq2 6377 . . . . 5 (𝑦 = 𝑥 → ((𝑥𝐴𝐵)‘𝑦) = ((𝑥𝐴𝐵)‘𝑥))
30 fveq2 6377 . . . . 5 (𝑦 = 𝑥 → ((𝑥𝐴𝐶)‘𝑦) = ((𝑥𝐴𝐶)‘𝑥))
3129, 30oveq12d 6862 . . . 4 (𝑦 = 𝑥 → (((𝑥𝐴𝐵)‘𝑦)𝑅((𝑥𝐴𝐶)‘𝑦)) = (((𝑥𝐴𝐵)‘𝑥)𝑅((𝑥𝐴𝐶)‘𝑥)))
3227, 28, 31cbvmpt 4910 . . 3 (𝑦𝐴 ↦ (((𝑥𝐴𝐵)‘𝑦)𝑅((𝑥𝐴𝐶)‘𝑦))) = (𝑥𝐴 ↦ (((𝑥𝐴𝐵)‘𝑥)𝑅((𝑥𝐴𝐶)‘𝑥)))
33 simpr 477 . . . . . 6 ((𝜑𝑥𝐴) → 𝑥𝐴)
343fvmpt2 6482 . . . . . 6 ((𝑥𝐴𝐵𝑊) → ((𝑥𝐴𝐵)‘𝑥) = 𝐵)
3533, 1, 34syl2anc 579 . . . . 5 ((𝜑𝑥𝐴) → ((𝑥𝐴𝐵)‘𝑥) = 𝐵)
3611fvmpt2 6482 . . . . . 6 ((𝑥𝐴𝐶𝑋) → ((𝑥𝐴𝐶)‘𝑥) = 𝐶)
3733, 9, 36syl2anc 579 . . . . 5 ((𝜑𝑥𝐴) → ((𝑥𝐴𝐶)‘𝑥) = 𝐶)
3835, 37oveq12d 6862 . . . 4 ((𝜑𝑥𝐴) → (((𝑥𝐴𝐵)‘𝑥)𝑅((𝑥𝐴𝐶)‘𝑥)) = (𝐵𝑅𝐶))
3938mpteq2dva 4905 . . 3 (𝜑 → (𝑥𝐴 ↦ (((𝑥𝐴𝐵)‘𝑥)𝑅((𝑥𝐴𝐶)‘𝑥))) = (𝑥𝐴 ↦ (𝐵𝑅𝐶)))
4032, 39syl5eq 2811 . 2 (𝜑 → (𝑦𝐴 ↦ (((𝑥𝐴𝐵)‘𝑦)𝑅((𝑥𝐴𝐶)‘𝑦))) = (𝑥𝐴 ↦ (𝐵𝑅𝐶)))
4123, 40eqtrd 2799 1 (𝜑 → (𝐹𝑓 𝑅𝐺) = (𝑥𝐴 ↦ (𝐵𝑅𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1652  wcel 2155  wral 3055  cmpt 4890   Fn wfn 6065  cfv 6070  (class class class)co 6844  𝑓 cof 7095
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4932  ax-sep 4943  ax-nul 4951  ax-pow 5003  ax-pr 5064
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-reu 3062  df-rab 3064  df-v 3352  df-sbc 3599  df-csb 3694  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-nul 4082  df-if 4246  df-sn 4337  df-pr 4339  df-op 4343  df-uni 4597  df-iun 4680  df-br 4812  df-opab 4874  df-mpt 4891  df-id 5187  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-iota 6033  df-fun 6072  df-fn 6073  df-f 6074  df-f1 6075  df-fo 6076  df-f1o 6077  df-fv 6078  df-ov 6847  df-oprab 6848  df-mpt2 6849  df-of 7097
This theorem is referenced by:  ofmpteq  7116  ofc12  7122  caofinvl  7124  caofcom  7129  caofass  7131  caofdi  7133  caofdir  7134  caonncan  7135  offval22  7457  ofccat  13998  ofs1  13999  o1add2  14642  o1mul2  14643  o1sub2  14644  o1dif  14648  fsumo1  14831  pwsplusgval  16419  pwsmulrval  16420  pwsvscafval  16423  pwsco1mhm  17639  pwsco2mhm  17640  pwssub  17799  gsumzaddlem  18590  gsummptfsadd  18593  gsummptfidmadd2  18595  gsumzsplit  18596  gsumsub  18617  gsummptfssub  18618  dprdfadd  18689  dprdfsub  18690  dprdfeq0  18691  dprdf11  18692  lmhmvsca  19320  rrgsupp  19568  psrbagaddcl  19647  psrass1lem  19654  psrlinv  19674  psrass1  19682  psrdi  19683  psrdir  19684  psrass23l  19685  psrcom  19686  psrass23  19687  mplsubrglem  19716  mplmonmul  19741  mplcoe1  19742  mplcoe3  19743  mplcoe5  19745  mplmon2  19769  evlslem1  19791  coe1sclmul  19928  coe1sclmul2  19930  uvcresum  20411  grpvrinv  20481  mhmvlin  20482  mamudi  20488  mamudir  20489  mdetunilem9  20706  tsmssub  22234  tgptsmscls  22235  tsmssplit  22237  tsmsxplem2  22239  ovolctb  23551  mbfmulc2re  23709  mbfneg  23711  mbfadd  23722  mbfsub  23723  mbfmulc2  23724  mbfmul  23787  itg2const  23801  itg2mulclem  23807  itg2mulc  23808  itg2splitlem  23809  itg2monolem1  23811  i1fibl  23868  itgitg1  23869  ibladdlem  23880  ibladd  23881  itgaddlem1  23883  iblabslem  23888  iblabs  23889  iblmulc2  23891  itgmulc2lem1  23892  bddmulibl  23899  dvmulf  24000  dvcmulf  24002  dvcof  24005  dvexp  24010  dvmptadd  24017  dvmptmul  24018  dvmptco  24029  dvef  24037  dv11cn  24058  itgsubstlem  24105  mdegmullem  24132  plypf1  24262  plyaddlem1  24263  plymullem1  24264  plyco  24291  dgrcolem1  24323  dgrcolem2  24324  plydiveu  24347  plyremlem  24353  elqaalem3  24370  iaa  24374  taylply2  24416  ulmdvlem1  24448  iblulm  24455  jensenlem2  25008  amgmlem  25010  ftalem7  25099  basellem8  25108  basellem9  25109  dchrmulid2  25271  dchrinvcl  25272  dchrfi  25274  lgseisenlem3  25396  lgseisenlem4  25397  chtppilimlem2  25457  chebbnd2  25460  chto1lb  25461  chpchtlim  25462  chpo1ub  25463  vmadivsum  25465  rpvmasumlem  25470  mudivsum  25513  selberglem1  25528  selberglem2  25529  selberg2lem  25533  selberg2  25534  pntrsumo1  25548  selbergr  25551  ofoprabco  29917  pl1cn  30451  esumadd  30569  poimirlem16  33852  poimirlem19  33855  itg2addnclem  33887  itg2addnclem3  33889  ibladdnclem  33892  itgaddnclem1  33894  iblabsnclem  33899  iblabsnc  33900  iblmulc2nc  33901  itgmulc2nclem1  33902  itgmulc2nclem2  33903  itgmulc2nc  33904  itgabsnc  33905  ftc1anclem3  33913  ftc1anclem4  33914  ftc1anclem5  33915  ftc1anclem6  33916  ftc1anclem7  33917  ftc1anclem8  33918  mendlmod  38443  mendassa  38444  expgrowthi  39209  expgrowth  39211  binomcxplemrat  39226  mulcncff  40722  subcncff  40734  addcncff  40738  divcncff  40745  dvsubf  40769  dvdivf  40778  fourierdlem16  40980  fourierdlem21  40985  fourierdlem22  40986  fourierdlem58  41021  fourierdlem59  41022  fourierdlem72  41035  fourierdlem83  41046  offvalfv  42793  aacllem  43222  amgmwlem  43223  amgmlemALT  43224
  Copyright terms: Public domain W3C validator