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

Theorem offval2 7081
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 3105 . . . . 5 (𝜑 → ∀𝑥𝐴 𝐵𝑊)
3 eqid 2761 . . . . . 6 (𝑥𝐴𝐵) = (𝑥𝐴𝐵)
43fnmpt 6182 . . . . 5 (∀𝑥𝐴 𝐵𝑊 → (𝑥𝐴𝐵) Fn 𝐴)
52, 4syl 17 . . . 4 (𝜑 → (𝑥𝐴𝐵) Fn 𝐴)
6 offval2.4 . . . . 5 (𝜑𝐹 = (𝑥𝐴𝐵))
76fneq1d 6143 . . . 4 (𝜑 → (𝐹 Fn 𝐴 ↔ (𝑥𝐴𝐵) Fn 𝐴))
85, 7mpbird 247 . . 3 (𝜑𝐹 Fn 𝐴)
9 offval2.3 . . . . . 6 ((𝜑𝑥𝐴) → 𝐶𝑋)
109ralrimiva 3105 . . . . 5 (𝜑 → ∀𝑥𝐴 𝐶𝑋)
11 eqid 2761 . . . . . 6 (𝑥𝐴𝐶) = (𝑥𝐴𝐶)
1211fnmpt 6182 . . . . 5 (∀𝑥𝐴 𝐶𝑋 → (𝑥𝐴𝐶) Fn 𝐴)
1310, 12syl 17 . . . 4 (𝜑 → (𝑥𝐴𝐶) Fn 𝐴)
14 offval2.5 . . . . 5 (𝜑𝐺 = (𝑥𝐴𝐶))
1514fneq1d 6143 . . . 4 (𝜑 → (𝐺 Fn 𝐴 ↔ (𝑥𝐴𝐶) Fn 𝐴))
1613, 15mpbird 247 . . 3 (𝜑𝐺 Fn 𝐴)
17 offval2.1 . . 3 (𝜑𝐴𝑉)
18 inidm 3966 . . 3 (𝐴𝐴) = 𝐴
196adantr 472 . . . 4 ((𝜑𝑦𝐴) → 𝐹 = (𝑥𝐴𝐵))
2019fveq1d 6356 . . 3 ((𝜑𝑦𝐴) → (𝐹𝑦) = ((𝑥𝐴𝐵)‘𝑦))
2114adantr 472 . . . 4 ((𝜑𝑦𝐴) → 𝐺 = (𝑥𝐴𝐶))
2221fveq1d 6356 . . 3 ((𝜑𝑦𝐴) → (𝐺𝑦) = ((𝑥𝐴𝐶)‘𝑦))
238, 16, 17, 17, 18, 20, 22offval 7071 . 2 (𝜑 → (𝐹𝑓 𝑅𝐺) = (𝑦𝐴 ↦ (((𝑥𝐴𝐵)‘𝑦)𝑅((𝑥𝐴𝐶)‘𝑦))))
24 nffvmpt1 6362 . . . . 5 𝑥((𝑥𝐴𝐵)‘𝑦)
25 nfcv 2903 . . . . 5 𝑥𝑅
26 nffvmpt1 6362 . . . . 5 𝑥((𝑥𝐴𝐶)‘𝑦)
2724, 25, 26nfov 6841 . . . 4 𝑥(((𝑥𝐴𝐵)‘𝑦)𝑅((𝑥𝐴𝐶)‘𝑦))
28 nfcv 2903 . . . 4 𝑦(((𝑥𝐴𝐵)‘𝑥)𝑅((𝑥𝐴𝐶)‘𝑥))
29 fveq2 6354 . . . . 5 (𝑦 = 𝑥 → ((𝑥𝐴𝐵)‘𝑦) = ((𝑥𝐴𝐵)‘𝑥))
30 fveq2 6354 . . . . 5 (𝑦 = 𝑥 → ((𝑥𝐴𝐶)‘𝑦) = ((𝑥𝐴𝐶)‘𝑥))
3129, 30oveq12d 6833 . . . 4 (𝑦 = 𝑥 → (((𝑥𝐴𝐵)‘𝑦)𝑅((𝑥𝐴𝐶)‘𝑦)) = (((𝑥𝐴𝐵)‘𝑥)𝑅((𝑥𝐴𝐶)‘𝑥)))
3227, 28, 31cbvmpt 4902 . . 3 (𝑦𝐴 ↦ (((𝑥𝐴𝐵)‘𝑦)𝑅((𝑥𝐴𝐶)‘𝑦))) = (𝑥𝐴 ↦ (((𝑥𝐴𝐵)‘𝑥)𝑅((𝑥𝐴𝐶)‘𝑥)))
33 simpr 479 . . . . . 6 ((𝜑𝑥𝐴) → 𝑥𝐴)
343fvmpt2 6455 . . . . . 6 ((𝑥𝐴𝐵𝑊) → ((𝑥𝐴𝐵)‘𝑥) = 𝐵)
3533, 1, 34syl2anc 696 . . . . 5 ((𝜑𝑥𝐴) → ((𝑥𝐴𝐵)‘𝑥) = 𝐵)
3611fvmpt2 6455 . . . . . 6 ((𝑥𝐴𝐶𝑋) → ((𝑥𝐴𝐶)‘𝑥) = 𝐶)
3733, 9, 36syl2anc 696 . . . . 5 ((𝜑𝑥𝐴) → ((𝑥𝐴𝐶)‘𝑥) = 𝐶)
3835, 37oveq12d 6833 . . . 4 ((𝜑𝑥𝐴) → (((𝑥𝐴𝐵)‘𝑥)𝑅((𝑥𝐴𝐶)‘𝑥)) = (𝐵𝑅𝐶))
3938mpteq2dva 4897 . . 3 (𝜑 → (𝑥𝐴 ↦ (((𝑥𝐴𝐵)‘𝑥)𝑅((𝑥𝐴𝐶)‘𝑥))) = (𝑥𝐴 ↦ (𝐵𝑅𝐶)))
4032, 39syl5eq 2807 . 2 (𝜑 → (𝑦𝐴 ↦ (((𝑥𝐴𝐵)‘𝑦)𝑅((𝑥𝐴𝐶)‘𝑦))) = (𝑥𝐴 ↦ (𝐵𝑅𝐶)))
4123, 40eqtrd 2795 1 (𝜑 → (𝐹𝑓 𝑅𝐺) = (𝑥𝐴 ↦ (𝐵𝑅𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1632  wcel 2140  wral 3051  cmpt 4882   Fn wfn 6045  cfv 6050  (class class class)co 6815  𝑓 cof 7062
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-8 2142  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741  ax-rep 4924  ax-sep 4934  ax-nul 4942  ax-pow 4993  ax-pr 5056
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-eu 2612  df-mo 2613  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-ne 2934  df-ral 3056  df-rex 3057  df-reu 3058  df-rab 3060  df-v 3343  df-sbc 3578  df-csb 3676  df-dif 3719  df-un 3721  df-in 3723  df-ss 3730  df-nul 4060  df-if 4232  df-sn 4323  df-pr 4325  df-op 4329  df-uni 4590  df-iun 4675  df-br 4806  df-opab 4866  df-mpt 4883  df-id 5175  df-xp 5273  df-rel 5274  df-cnv 5275  df-co 5276  df-dm 5277  df-rn 5278  df-res 5279  df-ima 5280  df-iota 6013  df-fun 6052  df-fn 6053  df-f 6054  df-f1 6055  df-fo 6056  df-f1o 6057  df-fv 6058  df-ov 6818  df-oprab 6819  df-mpt2 6820  df-of 7064
This theorem is referenced by:  ofmpteq  7083  ofc12  7089  caofinvl  7091  caofcom  7096  caofass  7098  caofdi  7100  caofdir  7101  caonncan  7102  offval22  7423  ofccat  13930  ofs1  13931  o1add2  14574  o1mul2  14575  o1sub2  14576  o1dif  14580  fsumo1  14764  pwsplusgval  16373  pwsmulrval  16374  pwsvscafval  16377  pwsco1mhm  17592  pwsco2mhm  17593  pwssub  17751  gsumzaddlem  18542  gsummptfsadd  18545  gsummptfidmadd2  18547  gsumzsplit  18548  gsumsub  18569  gsummptfssub  18570  dprdfadd  18640  dprdfsub  18641  dprdfeq0  18642  dprdf11  18643  lmhmvsca  19268  rrgsupp  19514  psrbagaddcl  19593  psrass1lem  19600  psrlinv  19620  psrass1  19628  psrdi  19629  psrdir  19630  psrass23l  19631  psrcom  19632  psrass23  19633  mplsubrglem  19662  mplmonmul  19687  mplcoe1  19688  mplcoe3  19689  mplcoe5  19691  mplmon2  19716  evlslem1  19738  coe1sclmul  19875  coe1sclmul2  19877  uvcresum  20355  grpvrinv  20425  mhmvlin  20426  mamudi  20432  mamudir  20433  mdetunilem9  20649  tsmssub  22174  tgptsmscls  22175  tsmssplit  22177  tsmsxplem2  22179  ovolctb  23479  mbfmulc2re  23635  mbfneg  23637  mbfadd  23648  mbfsub  23649  mbfmulc2  23650  mbfmul  23713  itg2const  23727  itg2mulclem  23733  itg2mulc  23734  itg2splitlem  23735  itg2monolem1  23737  i1fibl  23794  itgitg1  23795  ibladdlem  23806  ibladd  23807  itgaddlem1  23809  iblabslem  23814  iblabs  23815  iblmulc2  23817  itgmulc2lem1  23818  bddmulibl  23825  dvmulf  23926  dvcmulf  23928  dvcof  23931  dvexp  23936  dvmptadd  23943  dvmptmul  23944  dvmptco  23955  dvef  23963  dv11cn  23984  itgsubstlem  24031  mdegmullem  24058  plypf1  24188  plyaddlem1  24189  plymullem1  24190  plyco  24217  dgrcolem1  24249  dgrcolem2  24250  plydiveu  24273  plyremlem  24279  elqaalem3  24296  iaa  24300  taylply2  24342  ulmdvlem1  24374  iblulm  24381  jensenlem2  24935  amgmlem  24937  ftalem7  25026  basellem8  25035  basellem9  25036  dchrmulid2  25198  dchrinvcl  25199  dchrfi  25201  lgseisenlem3  25323  lgseisenlem4  25324  chtppilimlem2  25384  chebbnd2  25387  chto1lb  25388  chpchtlim  25389  chpo1ub  25390  vmadivsum  25392  rpvmasumlem  25397  mudivsum  25440  selberglem1  25455  selberglem2  25456  selberg2lem  25460  selberg2  25461  pntrsumo1  25475  selbergr  25478  ofoprabco  29795  pl1cn  30332  esumadd  30450  poimirlem16  33757  poimirlem19  33760  itg2addnclem  33793  itg2addnclem3  33795  ibladdnclem  33798  itgaddnclem1  33800  iblabsnclem  33805  iblabsnc  33806  iblmulc2nc  33807  itgmulc2nclem1  33808  itgmulc2nclem2  33809  itgmulc2nc  33810  itgabsnc  33811  ftc1anclem3  33819  ftc1anclem4  33820  ftc1anclem5  33821  ftc1anclem6  33822  ftc1anclem7  33823  ftc1anclem8  33824  mendlmod  38284  mendassa  38285  expgrowthi  39053  expgrowth  39055  binomcxplemrat  39070  mulcncff  40603  subcncff  40615  addcncff  40619  divcncff  40626  dvsubf  40650  dvdivf  40659  fourierdlem16  40862  fourierdlem21  40867  fourierdlem22  40868  fourierdlem58  40903  fourierdlem59  40904  fourierdlem72  40917  fourierdlem83  40928  offvalfv  42650  aacllem  43079  amgmwlem  43080  amgmlemALT  43081
  Copyright terms: Public domain W3C validator