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

Theorem offval2 6560
Description: The function operation expressed as a mapping. (Contributed by Mario Carneiro, 20-Jul-2014.)
Hypotheses
Ref Expression
offval2.1  |-  ( ph  ->  A  e.  V )
offval2.2  |-  ( (
ph  /\  x  e.  A )  ->  B  e.  W )
offval2.3  |-  ( (
ph  /\  x  e.  A )  ->  C  e.  X )
offval2.4  |-  ( ph  ->  F  =  ( x  e.  A  |->  B ) )
offval2.5  |-  ( ph  ->  G  =  ( x  e.  A  |->  C ) )
Assertion
Ref Expression
offval2  |-  ( ph  ->  ( F  oF R G )  =  ( x  e.  A  |->  ( B R C ) ) )
Distinct variable groups:    x, A    ph, x    x, R
Allowed substitution hints:    B( x)    C( x)    F( x)    G( x)    V( x)    W( x)    X( x)

Proof of Theorem offval2
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 offval2.2 . . . . . 6  |-  ( (
ph  /\  x  e.  A )  ->  B  e.  W )
21ralrimiva 2840 . . . . 5  |-  ( ph  ->  A. x  e.  A  B  e.  W )
3 eqid 2423 . . . . . 6  |-  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  B )
43fnmpt 5720 . . . . 5  |-  ( A. x  e.  A  B  e.  W  ->  ( x  e.  A  |->  B )  Fn  A )
52, 4syl 17 . . . 4  |-  ( ph  ->  ( x  e.  A  |->  B )  Fn  A
)
6 offval2.4 . . . . 5  |-  ( ph  ->  F  =  ( x  e.  A  |->  B ) )
76fneq1d 5682 . . . 4  |-  ( ph  ->  ( F  Fn  A  <->  ( x  e.  A  |->  B )  Fn  A ) )
85, 7mpbird 236 . . 3  |-  ( ph  ->  F  Fn  A )
9 offval2.3 . . . . . 6  |-  ( (
ph  /\  x  e.  A )  ->  C  e.  X )
109ralrimiva 2840 . . . . 5  |-  ( ph  ->  A. x  e.  A  C  e.  X )
11 eqid 2423 . . . . . 6  |-  ( x  e.  A  |->  C )  =  ( x  e.  A  |->  C )
1211fnmpt 5720 . . . . 5  |-  ( A. x  e.  A  C  e.  X  ->  ( x  e.  A  |->  C )  Fn  A )
1310, 12syl 17 . . . 4  |-  ( ph  ->  ( x  e.  A  |->  C )  Fn  A
)
14 offval2.5 . . . . 5  |-  ( ph  ->  G  =  ( x  e.  A  |->  C ) )
1514fneq1d 5682 . . . 4  |-  ( ph  ->  ( G  Fn  A  <->  ( x  e.  A  |->  C )  Fn  A ) )
1613, 15mpbird 236 . . 3  |-  ( ph  ->  G  Fn  A )
17 offval2.1 . . 3  |-  ( ph  ->  A  e.  V )
18 inidm 3672 . . 3  |-  ( A  i^i  A )  =  A
196adantr 467 . . . 4  |-  ( (
ph  /\  y  e.  A )  ->  F  =  ( x  e.  A  |->  B ) )
2019fveq1d 5881 . . 3  |-  ( (
ph  /\  y  e.  A )  ->  ( F `  y )  =  ( ( x  e.  A  |->  B ) `
 y ) )
2114adantr 467 . . . 4  |-  ( (
ph  /\  y  e.  A )  ->  G  =  ( x  e.  A  |->  C ) )
2221fveq1d 5881 . . 3  |-  ( (
ph  /\  y  e.  A )  ->  ( G `  y )  =  ( ( x  e.  A  |->  C ) `
 y ) )
238, 16, 17, 17, 18, 20, 22offval 6550 . 2  |-  ( ph  ->  ( F  oF R G )  =  ( y  e.  A  |->  ( ( ( x  e.  A  |->  B ) `
 y ) R ( ( x  e.  A  |->  C ) `  y ) ) ) )
24 nffvmpt1 5887 . . . . 5  |-  F/_ x
( ( x  e.  A  |->  B ) `  y )
25 nfcv 2585 . . . . 5  |-  F/_ x R
26 nffvmpt1 5887 . . . . 5  |-  F/_ x
( ( x  e.  A  |->  C ) `  y )
2724, 25, 26nfov 6329 . . . 4  |-  F/_ x
( ( ( x  e.  A  |->  B ) `
 y ) R ( ( x  e.  A  |->  C ) `  y ) )
28 nfcv 2585 . . . 4  |-  F/_ y
( ( ( x  e.  A  |->  B ) `
 x ) R ( ( x  e.  A  |->  C ) `  x ) )
29 fveq2 5879 . . . . 5  |-  ( y  =  x  ->  (
( x  e.  A  |->  B ) `  y
)  =  ( ( x  e.  A  |->  B ) `  x ) )
30 fveq2 5879 . . . . 5  |-  ( y  =  x  ->  (
( x  e.  A  |->  C ) `  y
)  =  ( ( x  e.  A  |->  C ) `  x ) )
3129, 30oveq12d 6321 . . . 4  |-  ( y  =  x  ->  (
( ( x  e.  A  |->  B ) `  y ) R ( ( x  e.  A  |->  C ) `  y
) )  =  ( ( ( x  e.  A  |->  B ) `  x ) R ( ( x  e.  A  |->  C ) `  x
) ) )
3227, 28, 31cbvmpt 4513 . . 3  |-  ( y  e.  A  |->  ( ( ( x  e.  A  |->  B ) `  y
) R ( ( x  e.  A  |->  C ) `  y ) ) )  =  ( x  e.  A  |->  ( ( ( x  e.  A  |->  B ) `  x ) R ( ( x  e.  A  |->  C ) `  x
) ) )
33 simpr 463 . . . . . 6  |-  ( (
ph  /\  x  e.  A )  ->  x  e.  A )
343fvmpt2 5971 . . . . . 6  |-  ( ( x  e.  A  /\  B  e.  W )  ->  ( ( x  e.  A  |->  B ) `  x )  =  B )
3533, 1, 34syl2anc 666 . . . . 5  |-  ( (
ph  /\  x  e.  A )  ->  (
( x  e.  A  |->  B ) `  x
)  =  B )
3611fvmpt2 5971 . . . . . 6  |-  ( ( x  e.  A  /\  C  e.  X )  ->  ( ( x  e.  A  |->  C ) `  x )  =  C )
3733, 9, 36syl2anc 666 . . . . 5  |-  ( (
ph  /\  x  e.  A )  ->  (
( x  e.  A  |->  C ) `  x
)  =  C )
3835, 37oveq12d 6321 . . . 4  |-  ( (
ph  /\  x  e.  A )  ->  (
( ( x  e.  A  |->  B ) `  x ) R ( ( x  e.  A  |->  C ) `  x
) )  =  ( B R C ) )
3938mpteq2dva 4508 . . 3  |-  ( ph  ->  ( x  e.  A  |->  ( ( ( x  e.  A  |->  B ) `
 x ) R ( ( x  e.  A  |->  C ) `  x ) ) )  =  ( x  e.  A  |->  ( B R C ) ) )
4032, 39syl5eq 2476 . 2  |-  ( ph  ->  ( y  e.  A  |->  ( ( ( x  e.  A  |->  B ) `
 y ) R ( ( x  e.  A  |->  C ) `  y ) ) )  =  ( x  e.  A  |->  ( B R C ) ) )
4123, 40eqtrd 2464 1  |-  ( ph  ->  ( F  oF R G )  =  ( x  e.  A  |->  ( B R C ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    = wceq 1438    e. wcel 1869   A.wral 2776    |-> cmpt 4480    Fn wfn 5594   ` cfv 5599  (class class class)co 6303    oFcof 6541
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-8 1871  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-rep 4534  ax-sep 4544  ax-nul 4553  ax-pow 4600  ax-pr 4658
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-eu 2270  df-mo 2271  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-ral 2781  df-rex 2782  df-reu 2783  df-rab 2785  df-v 3084  df-sbc 3301  df-csb 3397  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3763  df-if 3911  df-sn 3998  df-pr 4000  df-op 4004  df-uni 4218  df-iun 4299  df-br 4422  df-opab 4481  df-mpt 4482  df-id 4766  df-xp 4857  df-rel 4858  df-cnv 4859  df-co 4860  df-dm 4861  df-rn 4862  df-res 4863  df-ima 4864  df-iota 5563  df-fun 5601  df-fn 5602  df-f 5603  df-f1 5604  df-fo 5605  df-f1o 5606  df-fv 5607  df-ov 6306  df-oprab 6307  df-mpt2 6308  df-of 6543
This theorem is referenced by:  ofmpteq  6562  ofc12  6568  caofinvl  6570  caofcom  6575  caofass  6577  caofdi  6579  caofdir  6580  caonncan  6581  offval22  6884  o1add2  13680  o1mul2  13681  o1sub2  13682  o1dif  13686  fsumo1  13865  pwsplusgval  15381  pwsmulrval  15382  pwsvscafval  15385  pwsco1mhm  16610  pwsco2mhm  16611  pwssub  16792  gsumzaddlem  17547  gsummptfsadd  17550  gsummptfidmadd2  17552  gsumzsplit  17553  gsumsub  17574  gsummptfssub  17575  dprdfadd  17646  dprdfsub  17647  dprdfeq0  17648  dprdf11  17649  lmhmvsca  18261  rrgsupp  18508  psrbagaddcl  18587  psrass1lem  18594  psrlinv  18614  psrass1  18622  psrdi  18623  psrdir  18624  psrass23l  18625  psrcom  18626  psrass23  18627  mplsubrglem  18656  mplmonmul  18681  mplcoe1  18682  mplcoe3  18683  mplcoe5  18685  mplmon2  18709  evlslem1  18731  coe1sclmul  18868  coe1sclmul2  18870  uvcresum  19343  grpvrinv  19413  mhmvlin  19414  mamudi  19420  mamudir  19421  mdetunilem9  19637  tsmssub  21155  tgptsmscls  21156  tsmssplit  21158  tsmsxplem2  21160  ovolctb  22435  mbfmulc2re  22596  mbfneg  22598  mbfadd  22609  mbfsub  22610  mbfmulc2  22611  mbfmul  22676  itg2const  22690  itg2mulclem  22696  itg2mulc  22697  itg2splitlem  22698  itg2monolem1  22700  i1fibl  22757  itgitg1  22758  ibladdlem  22769  ibladd  22770  itgaddlem1  22772  iblabslem  22777  iblabs  22778  iblmulc2  22780  itgmulc2lem1  22781  bddmulibl  22788  dvmulf  22889  dvcmulf  22891  dvcof  22894  dvexp  22899  dvmptadd  22906  dvmptmul  22907  dvmptco  22918  dvef  22924  dv11cn  22945  itgsubstlem  22992  mdegmullem  23019  plypf1  23158  plyaddlem1  23159  plymullem1  23160  plyco  23187  dgrcolem1  23219  dgrcolem2  23220  plydiveu  23243  plyremlem  23249  elqaalem3  23266  elqaalem3OLD  23269  iaa  23273  taylply2  23315  ulmdvlem1  23347  iblulm  23354  jensenlem2  23905  amgmlem  23907  ftalem7  23997  basellem8  24006  basellem9  24007  dchrmulid2  24172  dchrinvcl  24173  dchrfi  24175  lgseisenlem3  24271  lgseisenlem4  24272  chtppilimlem2  24304  chebbnd2  24307  chto1lb  24308  chpchtlim  24309  chpo1ub  24310  vmadivsum  24312  rpvmasumlem  24317  mudivsum  24360  selberglem1  24375  selberglem2  24376  selberg2lem  24380  selberg2  24381  pntrsumo1  24395  selbergr  24398  ofoprabco  28263  pl1cn  28763  esumadd  28880  ofccat  29431  ofs1  29433  poimirlem16  31914  poimirlem19  31917  itg2addnclem  31951  itg2addnclem3  31953  ibladdnclem  31956  itgaddnclem1  31958  iblabsnclem  31963  iblabsnc  31964  iblmulc2nc  31965  itgmulc2nclem1  31966  itgmulc2nclem2  31967  itgmulc2nc  31968  itgabsnc  31969  ftc1anclem3  31977  ftc1anclem4  31978  ftc1anclem5  31979  ftc1anclem6  31980  ftc1anclem7  31981  ftc1anclem8  31982  mendlmod  36023  mendassa  36024  expgrowthi  36584  expgrowth  36586  binomcxplemrat  36601  mulcncff  37609  subcncff  37621  addcncff  37626  divcncff  37633  dvsubf  37648  dvdivf  37658  fourierdlem16  37849  fourierdlem21  37854  fourierdlem22  37855  fourierdlem58  37892  fourierdlem59  37893  fourierdlem72  37906  fourierdlem83  37917  offvalfv  39468  aacllem  39884
  Copyright terms: Public domain W3C validator