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

Theorem offval2 6473
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 2806 . . . . 5  |-  ( ph  ->  A. x  e.  A  B  e.  W )
3 eqid 2392 . . . . . 6  |-  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  B )
43fnmpt 5628 . . . . 5  |-  ( A. x  e.  A  B  e.  W  ->  ( x  e.  A  |->  B )  Fn  A )
52, 4syl 16 . . . 4  |-  ( ph  ->  ( x  e.  A  |->  B )  Fn  A
)
6 offval2.4 . . . . 5  |-  ( ph  ->  F  =  ( x  e.  A  |->  B ) )
76fneq1d 5592 . . . 4  |-  ( ph  ->  ( F  Fn  A  <->  ( x  e.  A  |->  B )  Fn  A ) )
85, 7mpbird 232 . . 3  |-  ( ph  ->  F  Fn  A )
9 offval2.3 . . . . . 6  |-  ( (
ph  /\  x  e.  A )  ->  C  e.  X )
109ralrimiva 2806 . . . . 5  |-  ( ph  ->  A. x  e.  A  C  e.  X )
11 eqid 2392 . . . . . 6  |-  ( x  e.  A  |->  C )  =  ( x  e.  A  |->  C )
1211fnmpt 5628 . . . . 5  |-  ( A. x  e.  A  C  e.  X  ->  ( x  e.  A  |->  C )  Fn  A )
1310, 12syl 16 . . . 4  |-  ( ph  ->  ( x  e.  A  |->  C )  Fn  A
)
14 offval2.5 . . . . 5  |-  ( ph  ->  G  =  ( x  e.  A  |->  C ) )
1514fneq1d 5592 . . . 4  |-  ( ph  ->  ( G  Fn  A  <->  ( x  e.  A  |->  C )  Fn  A ) )
1613, 15mpbird 232 . . 3  |-  ( ph  ->  G  Fn  A )
17 offval2.1 . . 3  |-  ( ph  ->  A  e.  V )
18 inidm 3634 . . 3  |-  ( A  i^i  A )  =  A
196adantr 463 . . . 4  |-  ( (
ph  /\  y  e.  A )  ->  F  =  ( x  e.  A  |->  B ) )
2019fveq1d 5789 . . 3  |-  ( (
ph  /\  y  e.  A )  ->  ( F `  y )  =  ( ( x  e.  A  |->  B ) `
 y ) )
2114adantr 463 . . . 4  |-  ( (
ph  /\  y  e.  A )  ->  G  =  ( x  e.  A  |->  C ) )
2221fveq1d 5789 . . 3  |-  ( (
ph  /\  y  e.  A )  ->  ( G `  y )  =  ( ( x  e.  A  |->  C ) `
 y ) )
238, 16, 17, 17, 18, 20, 22offval 6464 . 2  |-  ( ph  ->  ( F  oF R G )  =  ( y  e.  A  |->  ( ( ( x  e.  A  |->  B ) `
 y ) R ( ( x  e.  A  |->  C ) `  y ) ) ) )
24 nffvmpt1 5795 . . . . 5  |-  F/_ x
( ( x  e.  A  |->  B ) `  y )
25 nfcv 2554 . . . . 5  |-  F/_ x R
26 nffvmpt1 5795 . . . . 5  |-  F/_ x
( ( x  e.  A  |->  C ) `  y )
2724, 25, 26nfov 6240 . . . 4  |-  F/_ x
( ( ( x  e.  A  |->  B ) `
 y ) R ( ( x  e.  A  |->  C ) `  y ) )
28 nfcv 2554 . . . 4  |-  F/_ y
( ( ( x  e.  A  |->  B ) `
 x ) R ( ( x  e.  A  |->  C ) `  x ) )
29 fveq2 5787 . . . . 5  |-  ( y  =  x  ->  (
( x  e.  A  |->  B ) `  y
)  =  ( ( x  e.  A  |->  B ) `  x ) )
30 fveq2 5787 . . . . 5  |-  ( y  =  x  ->  (
( x  e.  A  |->  C ) `  y
)  =  ( ( x  e.  A  |->  C ) `  x ) )
3129, 30oveq12d 6232 . . . 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 4470 . . 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 459 . . . . . 6  |-  ( (
ph  /\  x  e.  A )  ->  x  e.  A )
343fvmpt2 5878 . . . . . 6  |-  ( ( x  e.  A  /\  B  e.  W )  ->  ( ( x  e.  A  |->  B ) `  x )  =  B )
3533, 1, 34syl2anc 659 . . . . 5  |-  ( (
ph  /\  x  e.  A )  ->  (
( x  e.  A  |->  B ) `  x
)  =  B )
3611fvmpt2 5878 . . . . . 6  |-  ( ( x  e.  A  /\  C  e.  X )  ->  ( ( x  e.  A  |->  C ) `  x )  =  C )
3733, 9, 36syl2anc 659 . . . . 5  |-  ( (
ph  /\  x  e.  A )  ->  (
( x  e.  A  |->  C ) `  x
)  =  C )
3835, 37oveq12d 6232 . . . 4  |-  ( (
ph  /\  x  e.  A )  ->  (
( ( x  e.  A  |->  B ) `  x ) R ( ( x  e.  A  |->  C ) `  x
) )  =  ( B R C ) )
3938mpteq2dva 4466 . . 3  |-  ( ph  ->  ( x  e.  A  |->  ( ( ( x  e.  A  |->  B ) `
 x ) R ( ( x  e.  A  |->  C ) `  x ) ) )  =  ( x  e.  A  |->  ( B R C ) ) )
4032, 39syl5eq 2445 . 2  |-  ( ph  ->  ( y  e.  A  |->  ( ( ( x  e.  A  |->  B ) `
 y ) R ( ( x  e.  A  |->  C ) `  y ) ) )  =  ( x  e.  A  |->  ( B R C ) ) )
4123, 40eqtrd 2433 1  |-  ( ph  ->  ( F  oF R G )  =  ( x  e.  A  |->  ( B R C ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    = wceq 1399    e. wcel 1836   A.wral 2742    |-> cmpt 4438    Fn wfn 5504   ` cfv 5509  (class class class)co 6214    oFcof 6455
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-8 1838  ax-9 1840  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2016  ax-ext 2370  ax-rep 4491  ax-sep 4501  ax-nul 4509  ax-pow 4556  ax-pr 4614
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-eu 2232  df-mo 2233  df-clab 2378  df-cleq 2384  df-clel 2387  df-nfc 2542  df-ne 2589  df-ral 2747  df-rex 2748  df-reu 2749  df-rab 2751  df-v 3049  df-sbc 3266  df-csb 3362  df-dif 3405  df-un 3407  df-in 3409  df-ss 3416  df-nul 3725  df-if 3871  df-sn 3958  df-pr 3960  df-op 3964  df-uni 4177  df-iun 4258  df-br 4381  df-opab 4439  df-mpt 4440  df-id 4722  df-xp 4932  df-rel 4933  df-cnv 4934  df-co 4935  df-dm 4936  df-rn 4937  df-res 4938  df-ima 4939  df-iota 5473  df-fun 5511  df-fn 5512  df-f 5513  df-f1 5514  df-fo 5515  df-f1o 5516  df-fv 5517  df-ov 6217  df-oprab 6218  df-mpt2 6219  df-of 6457
This theorem is referenced by:  ofmpteq  6475  ofc12  6482  caofinvl  6484  caofcom  6489  caofass  6491  caofdi  6493  caofdir  6494  caonncan  6495  offval22  6796  o1add2  13467  o1mul2  13468  o1sub2  13469  o1dif  13473  fsumo1  13647  pwsplusgval  14916  pwsmulrval  14917  pwsvscafval  14920  pwsco1mhm  16137  pwsco2mhm  16138  pwssub  16319  gsumzaddlem  17070  gsumzaddlemOLD  17072  gsummptfsadd  17076  gsummptfsaddOLD  17077  gsummptfidmadd2  17079  gsumzsplit  17080  gsumzsplitOLD  17081  gsumsub  17108  gsummptfssub  17109  dprdfadd  17192  dprdfsub  17193  dprdfeq0  17194  dprdf11  17195  dprdfaddOLD  17199  dprdfsubOLD  17200  dprdfeq0OLD  17201  dprdf11OLD  17202  lmhmvsca  17823  rrgsupp  18071  rrgsuppOLD  18072  psrbagaddcl  18152  psrbagaddclOLD  18153  psrass1lem  18161  psrlinv  18182  psrass1  18192  psrdi  18193  psrdir  18194  psrass23l  18195  psrcom  18196  psrass23  18197  mplsubrglem  18232  mplsubrglemOLD  18233  mplmonmul  18258  mplcoe1  18259  mplcoe3  18260  mplcoe3OLD  18261  mplcoe5  18263  mplcoe2OLD  18265  mplmon2  18290  evlslem1  18316  coe1sclmul  18455  coe1sclmul2  18457  uvcresum  18932  grpvrinv  19002  mhmvlin  19003  mamudi  19009  mamudir  19010  mdetunilem9  19226  tsmssub  20755  tgptsmscls  20756  tsmssplit  20758  tsmsxplem2  20760  ovolctb  22005  mbfmulc2re  22159  mbfneg  22161  mbfadd  22172  mbfsub  22173  mbfmulc2  22174  mbfmul  22237  itg2const  22251  itg2mulclem  22257  itg2mulc  22258  itg2splitlem  22259  itg2monolem1  22261  i1fibl  22318  itgitg1  22319  ibladdlem  22330  ibladd  22331  itgaddlem1  22333  iblabslem  22338  iblabs  22339  iblmulc2  22341  itgmulc2lem1  22342  bddmulibl  22349  dvmulf  22450  dvcmulf  22452  dvcof  22455  dvexp  22460  dvmptadd  22467  dvmptmul  22468  dvmptco  22479  dvef  22485  dv11cn  22506  itgsubstlem  22553  mdegmullem  22582  plypf1  22713  plyaddlem1  22714  plymullem1  22715  plyco  22742  dgrcolem1  22774  dgrcolem2  22775  plydiveu  22798  plyremlem  22804  elqaalem3  22821  iaa  22825  taylply2  22867  ulmdvlem1  22899  iblulm  22906  jensenlem2  23453  amgmlem  23455  ftalem7  23488  basellem8  23497  basellem9  23498  dchrmulid2  23663  dchrinvcl  23664  dchrfi  23666  lgseisenlem3  23762  lgseisenlem4  23763  chtppilimlem2  23795  chebbnd2  23798  chto1lb  23799  chpchtlim  23800  chpo1ub  23801  vmadivsum  23803  rpvmasumlem  23808  mudivsum  23851  selberglem1  23866  selberglem2  23867  selberg2lem  23871  selberg2  23872  pntrsumo1  23886  selbergr  23889  ofoprabco  27681  pl1cn  28122  esumadd  28236  ofccat  28716  ofs1  28718  itg2addnclem  30268  itg2addnclem3  30270  ibladdnclem  30273  itgaddnclem1  30275  iblabsnclem  30280  iblabsnc  30281  iblmulc2nc  30282  itgmulc2nclem1  30283  itgmulc2nclem2  30284  itgmulc2nc  30285  itgabsnc  30286  ftc1anclem3  30294  ftc1anclem4  30295  ftc1anclem5  30296  ftc1anclem6  30297  ftc1anclem7  30298  ftc1anclem8  30299  mendlmod  31346  mendassa  31347  expgrowthi  31442  expgrowth  31444  binomcxplemrat  31459  mulcncff  31871  subcncff  31883  addcncff  31888  divcncff  31895  dvsubf  31910  dvdivf  31920  fourierdlem16  32106  fourierdlem21  32111  fourierdlem22  32112  fourierdlem58  32148  fourierdlem59  32149  fourierdlem72  32162  fourierdlem83  32173  offvalfv  33167  aacllem  33585
  Copyright terms: Public domain W3C validator