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

Theorem offval2 6790
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 2948 . . . . 5 (𝜑 → ∀𝑥𝐴 𝐵𝑊)
3 eqid 2609 . . . . . 6 (𝑥𝐴𝐵) = (𝑥𝐴𝐵)
43fnmpt 5919 . . . . 5 (∀𝑥𝐴 𝐵𝑊 → (𝑥𝐴𝐵) Fn 𝐴)
52, 4syl 17 . . . 4 (𝜑 → (𝑥𝐴𝐵) Fn 𝐴)
6 offval2.4 . . . . 5 (𝜑𝐹 = (𝑥𝐴𝐵))
76fneq1d 5881 . . . 4 (𝜑 → (𝐹 Fn 𝐴 ↔ (𝑥𝐴𝐵) Fn 𝐴))
85, 7mpbird 245 . . 3 (𝜑𝐹 Fn 𝐴)
9 offval2.3 . . . . . 6 ((𝜑𝑥𝐴) → 𝐶𝑋)
109ralrimiva 2948 . . . . 5 (𝜑 → ∀𝑥𝐴 𝐶𝑋)
11 eqid 2609 . . . . . 6 (𝑥𝐴𝐶) = (𝑥𝐴𝐶)
1211fnmpt 5919 . . . . 5 (∀𝑥𝐴 𝐶𝑋 → (𝑥𝐴𝐶) Fn 𝐴)
1310, 12syl 17 . . . 4 (𝜑 → (𝑥𝐴𝐶) Fn 𝐴)
14 offval2.5 . . . . 5 (𝜑𝐺 = (𝑥𝐴𝐶))
1514fneq1d 5881 . . . 4 (𝜑 → (𝐺 Fn 𝐴 ↔ (𝑥𝐴𝐶) Fn 𝐴))
1613, 15mpbird 245 . . 3 (𝜑𝐺 Fn 𝐴)
17 offval2.1 . . 3 (𝜑𝐴𝑉)
18 inidm 3783 . . 3 (𝐴𝐴) = 𝐴
196adantr 479 . . . 4 ((𝜑𝑦𝐴) → 𝐹 = (𝑥𝐴𝐵))
2019fveq1d 6090 . . 3 ((𝜑𝑦𝐴) → (𝐹𝑦) = ((𝑥𝐴𝐵)‘𝑦))
2114adantr 479 . . . 4 ((𝜑𝑦𝐴) → 𝐺 = (𝑥𝐴𝐶))
2221fveq1d 6090 . . 3 ((𝜑𝑦𝐴) → (𝐺𝑦) = ((𝑥𝐴𝐶)‘𝑦))
238, 16, 17, 17, 18, 20, 22offval 6780 . 2 (𝜑 → (𝐹𝑓 𝑅𝐺) = (𝑦𝐴 ↦ (((𝑥𝐴𝐵)‘𝑦)𝑅((𝑥𝐴𝐶)‘𝑦))))
24 nffvmpt1 6096 . . . . 5 𝑥((𝑥𝐴𝐵)‘𝑦)
25 nfcv 2750 . . . . 5 𝑥𝑅
26 nffvmpt1 6096 . . . . 5 𝑥((𝑥𝐴𝐶)‘𝑦)
2724, 25, 26nfov 6553 . . . 4 𝑥(((𝑥𝐴𝐵)‘𝑦)𝑅((𝑥𝐴𝐶)‘𝑦))
28 nfcv 2750 . . . 4 𝑦(((𝑥𝐴𝐵)‘𝑥)𝑅((𝑥𝐴𝐶)‘𝑥))
29 fveq2 6088 . . . . 5 (𝑦 = 𝑥 → ((𝑥𝐴𝐵)‘𝑦) = ((𝑥𝐴𝐵)‘𝑥))
30 fveq2 6088 . . . . 5 (𝑦 = 𝑥 → ((𝑥𝐴𝐶)‘𝑦) = ((𝑥𝐴𝐶)‘𝑥))
3129, 30oveq12d 6545 . . . 4 (𝑦 = 𝑥 → (((𝑥𝐴𝐵)‘𝑦)𝑅((𝑥𝐴𝐶)‘𝑦)) = (((𝑥𝐴𝐵)‘𝑥)𝑅((𝑥𝐴𝐶)‘𝑥)))
3227, 28, 31cbvmpt 4671 . . 3 (𝑦𝐴 ↦ (((𝑥𝐴𝐵)‘𝑦)𝑅((𝑥𝐴𝐶)‘𝑦))) = (𝑥𝐴 ↦ (((𝑥𝐴𝐵)‘𝑥)𝑅((𝑥𝐴𝐶)‘𝑥)))
33 simpr 475 . . . . . 6 ((𝜑𝑥𝐴) → 𝑥𝐴)
343fvmpt2 6185 . . . . . 6 ((𝑥𝐴𝐵𝑊) → ((𝑥𝐴𝐵)‘𝑥) = 𝐵)
3533, 1, 34syl2anc 690 . . . . 5 ((𝜑𝑥𝐴) → ((𝑥𝐴𝐵)‘𝑥) = 𝐵)
3611fvmpt2 6185 . . . . . 6 ((𝑥𝐴𝐶𝑋) → ((𝑥𝐴𝐶)‘𝑥) = 𝐶)
3733, 9, 36syl2anc 690 . . . . 5 ((𝜑𝑥𝐴) → ((𝑥𝐴𝐶)‘𝑥) = 𝐶)
3835, 37oveq12d 6545 . . . 4 ((𝜑𝑥𝐴) → (((𝑥𝐴𝐵)‘𝑥)𝑅((𝑥𝐴𝐶)‘𝑥)) = (𝐵𝑅𝐶))
3938mpteq2dva 4666 . . 3 (𝜑 → (𝑥𝐴 ↦ (((𝑥𝐴𝐵)‘𝑥)𝑅((𝑥𝐴𝐶)‘𝑥))) = (𝑥𝐴 ↦ (𝐵𝑅𝐶)))
4032, 39syl5eq 2655 . 2 (𝜑 → (𝑦𝐴 ↦ (((𝑥𝐴𝐵)‘𝑦)𝑅((𝑥𝐴𝐶)‘𝑦))) = (𝑥𝐴 ↦ (𝐵𝑅𝐶)))
4123, 40eqtrd 2643 1 (𝜑 → (𝐹𝑓 𝑅𝐺) = (𝑥𝐴 ↦ (𝐵𝑅𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = wceq 1474  wcel 1976  wral 2895  cmpt 4637   Fn wfn 5785  cfv 5790  (class class class)co 6527  𝑓 cof 6771
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-ral 2900  df-rex 2901  df-reu 2902  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-id 4943  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-of 6773
This theorem is referenced by:  ofmpteq  6792  ofc12  6798  caofinvl  6800  caofcom  6805  caofass  6807  caofdi  6809  caofdir  6810  caonncan  6811  offval22  7118  ofccat  13505  ofs1  13506  o1add2  14151  o1mul2  14152  o1sub2  14153  o1dif  14157  fsumo1  14334  pwsplusgval  15922  pwsmulrval  15923  pwsvscafval  15926  pwsco1mhm  17142  pwsco2mhm  17143  pwssub  17301  gsumzaddlem  18093  gsummptfsadd  18096  gsummptfidmadd2  18098  gsumzsplit  18099  gsumsub  18120  gsummptfssub  18121  dprdfadd  18191  dprdfsub  18192  dprdfeq0  18193  dprdf11  18194  lmhmvsca  18815  rrgsupp  19061  psrbagaddcl  19140  psrass1lem  19147  psrlinv  19167  psrass1  19175  psrdi  19176  psrdir  19177  psrass23l  19178  psrcom  19179  psrass23  19180  mplsubrglem  19209  mplmonmul  19234  mplcoe1  19235  mplcoe3  19236  mplcoe5  19238  mplmon2  19263  evlslem1  19285  coe1sclmul  19422  coe1sclmul2  19424  uvcresum  19899  grpvrinv  19969  mhmvlin  19970  mamudi  19976  mamudir  19977  mdetunilem9  20193  tsmssub  21710  tgptsmscls  21711  tsmssplit  21713  tsmsxplem2  21715  ovolctb  23010  mbfmulc2re  23166  mbfneg  23168  mbfadd  23179  mbfsub  23180  mbfmulc2  23181  mbfmul  23244  itg2const  23258  itg2mulclem  23264  itg2mulc  23265  itg2splitlem  23266  itg2monolem1  23268  i1fibl  23325  itgitg1  23326  ibladdlem  23337  ibladd  23338  itgaddlem1  23340  iblabslem  23345  iblabs  23346  iblmulc2  23348  itgmulc2lem1  23349  bddmulibl  23356  dvmulf  23457  dvcmulf  23459  dvcof  23462  dvexp  23467  dvmptadd  23474  dvmptmul  23475  dvmptco  23486  dvef  23492  dv11cn  23513  itgsubstlem  23560  mdegmullem  23587  plypf1  23717  plyaddlem1  23718  plymullem1  23719  plyco  23746  dgrcolem1  23778  dgrcolem2  23779  plydiveu  23802  plyremlem  23808  elqaalem3  23825  iaa  23829  taylply2  23871  ulmdvlem1  23903  iblulm  23910  jensenlem2  24459  amgmlem  24461  ftalem7  24550  basellem8  24559  basellem9  24560  dchrmulid2  24722  dchrinvcl  24723  dchrfi  24725  lgseisenlem3  24847  lgseisenlem4  24848  chtppilimlem2  24908  chebbnd2  24911  chto1lb  24912  chpchtlim  24913  chpo1ub  24914  vmadivsum  24916  rpvmasumlem  24921  mudivsum  24964  selberglem1  24979  selberglem2  24980  selberg2lem  24984  selberg2  24985  pntrsumo1  24999  selbergr  25002  ofoprabco  28681  pl1cn  29163  esumadd  29280  poimirlem16  32419  poimirlem19  32422  itg2addnclem  32455  itg2addnclem3  32457  ibladdnclem  32460  itgaddnclem1  32462  iblabsnclem  32467  iblabsnc  32468  iblmulc2nc  32469  itgmulc2nclem1  32470  itgmulc2nclem2  32471  itgmulc2nc  32472  itgabsnc  32473  ftc1anclem3  32481  ftc1anclem4  32482  ftc1anclem5  32483  ftc1anclem6  32484  ftc1anclem7  32485  ftc1anclem8  32486  mendlmod  36606  mendassa  36607  expgrowthi  37378  expgrowth  37380  binomcxplemrat  37395  mulcncff  38577  subcncff  38589  addcncff  38594  divcncff  38601  dvsubf  38626  dvdivf  38636  fourierdlem16  38840  fourierdlem21  38845  fourierdlem22  38846  fourierdlem58  38881  fourierdlem59  38882  fourierdlem72  38895  fourierdlem83  38906  offvalfv  41936  aacllem  42339  amgmwlem  42340  amgmlemALT  42341
  Copyright terms: Public domain W3C validator