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

Theorem offval2 6539
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 2878 . . . . 5  |-  ( ph  ->  A. x  e.  A  B  e.  W )
3 eqid 2467 . . . . . 6  |-  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  B )
43fnmpt 5706 . . . . 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 5670 . . . 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 2878 . . . . 5  |-  ( ph  ->  A. x  e.  A  C  e.  X )
11 eqid 2467 . . . . . 6  |-  ( x  e.  A  |->  C )  =  ( x  e.  A  |->  C )
1211fnmpt 5706 . . . . 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 5670 . . . 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 3707 . . 3  |-  ( A  i^i  A )  =  A
196adantr 465 . . . 4  |-  ( (
ph  /\  y  e.  A )  ->  F  =  ( x  e.  A  |->  B ) )
2019fveq1d 5867 . . 3  |-  ( (
ph  /\  y  e.  A )  ->  ( F `  y )  =  ( ( x  e.  A  |->  B ) `
 y ) )
2114adantr 465 . . . 4  |-  ( (
ph  /\  y  e.  A )  ->  G  =  ( x  e.  A  |->  C ) )
2221fveq1d 5867 . . 3  |-  ( (
ph  /\  y  e.  A )  ->  ( G `  y )  =  ( ( x  e.  A  |->  C ) `
 y ) )
238, 16, 17, 17, 18, 20, 22offval 6530 . 2  |-  ( ph  ->  ( F  oF R G )  =  ( y  e.  A  |->  ( ( ( x  e.  A  |->  B ) `
 y ) R ( ( x  e.  A  |->  C ) `  y ) ) ) )
24 nffvmpt1 5873 . . . . 5  |-  F/_ x
( ( x  e.  A  |->  B ) `  y )
25 nfcv 2629 . . . . 5  |-  F/_ x R
26 nffvmpt1 5873 . . . . 5  |-  F/_ x
( ( x  e.  A  |->  C ) `  y )
2724, 25, 26nfov 6306 . . . 4  |-  F/_ x
( ( ( x  e.  A  |->  B ) `
 y ) R ( ( x  e.  A  |->  C ) `  y ) )
28 nfcv 2629 . . . 4  |-  F/_ y
( ( ( x  e.  A  |->  B ) `
 x ) R ( ( x  e.  A  |->  C ) `  x ) )
29 fveq2 5865 . . . . 5  |-  ( y  =  x  ->  (
( x  e.  A  |->  B ) `  y
)  =  ( ( x  e.  A  |->  B ) `  x ) )
30 fveq2 5865 . . . . 5  |-  ( y  =  x  ->  (
( x  e.  A  |->  C ) `  y
)  =  ( ( x  e.  A  |->  C ) `  x ) )
3129, 30oveq12d 6301 . . . 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 4537 . . 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 461 . . . . . 6  |-  ( (
ph  /\  x  e.  A )  ->  x  e.  A )
343fvmpt2 5956 . . . . . 6  |-  ( ( x  e.  A  /\  B  e.  W )  ->  ( ( x  e.  A  |->  B ) `  x )  =  B )
3533, 1, 34syl2anc 661 . . . . 5  |-  ( (
ph  /\  x  e.  A )  ->  (
( x  e.  A  |->  B ) `  x
)  =  B )
3611fvmpt2 5956 . . . . . 6  |-  ( ( x  e.  A  /\  C  e.  X )  ->  ( ( x  e.  A  |->  C ) `  x )  =  C )
3733, 9, 36syl2anc 661 . . . . 5  |-  ( (
ph  /\  x  e.  A )  ->  (
( x  e.  A  |->  C ) `  x
)  =  C )
3835, 37oveq12d 6301 . . . 4  |-  ( (
ph  /\  x  e.  A )  ->  (
( ( x  e.  A  |->  B ) `  x ) R ( ( x  e.  A  |->  C ) `  x
) )  =  ( B R C ) )
3938mpteq2dva 4533 . . 3  |-  ( ph  ->  ( x  e.  A  |->  ( ( ( x  e.  A  |->  B ) `
 x ) R ( ( x  e.  A  |->  C ) `  x ) ) )  =  ( x  e.  A  |->  ( B R C ) ) )
4032, 39syl5eq 2520 . 2  |-  ( ph  ->  ( y  e.  A  |->  ( ( ( x  e.  A  |->  B ) `
 y ) R ( ( x  e.  A  |->  C ) `  y ) ) )  =  ( x  e.  A  |->  ( B R C ) ) )
4123, 40eqtrd 2508 1  |-  ( ph  ->  ( F  oF R G )  =  ( x  e.  A  |->  ( B R C ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1379    e. wcel 1767   A.wral 2814    |-> cmpt 4505    Fn wfn 5582   ` cfv 5587  (class class class)co 6283    oFcof 6521
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4558  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-reu 2821  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-iun 4327  df-br 4448  df-opab 4506  df-mpt 4507  df-id 4795  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5550  df-fun 5589  df-fn 5590  df-f 5591  df-f1 5592  df-fo 5593  df-f1o 5594  df-fv 5595  df-ov 6286  df-oprab 6287  df-mpt2 6288  df-of 6523
This theorem is referenced by:  ofmpteq  6541  ofc12  6548  caofinvl  6550  caofcom  6555  caofass  6557  caofdi  6559  caofdir  6560  caonncan  6561  offval22  6862  o1add2  13408  o1mul2  13409  o1sub2  13410  o1dif  13414  fsumo1  13588  pwsplusgval  14744  pwsmulrval  14745  pwsvscafval  14748  pwsco1mhm  15817  pwsco2mhm  15818  pwssub  15990  gsumzaddlem  16734  gsumzaddlemOLD  16736  gsummptfsadd  16740  gsummptfsaddOLD  16741  gsummptfidmadd2  16743  gsumzsplit  16744  gsumzsplitOLD  16745  gsumsub  16774  gsumsubOLD  16775  gsummptfssub  16776  dprdfadd  16859  dprdfsub  16860  dprdfeq0  16861  dprdf11  16862  dprdfaddOLD  16866  dprdfsubOLD  16867  dprdfeq0OLD  16868  dprdf11OLD  16869  lmhmvsca  17486  rrgsupp  17726  rrgsuppOLD  17727  psrbagaddcl  17807  psrbagaddclOLD  17808  psrass1lem  17816  psrlinv  17837  psrass1  17847  psrdi  17848  psrdir  17849  psrass23l  17850  psrcom  17851  psrass23  17852  mplsubrglem  17887  mplsubrglemOLD  17888  mplmonmul  17913  mplcoe1  17914  mplcoe3  17915  mplcoe3OLD  17916  mplcoe5  17918  mplcoe2OLD  17920  mplmon2  17945  evlslem1  17971  coe1sclmul  18110  coe1sclmul2  18112  uvcresum  18607  grpvrinv  18681  mhmvlin  18682  mamudi  18688  mamudir  18689  mdetunilem9  18905  tsmssub  20402  tgptsmscls  20403  tsmssplit  20405  tsmsxplem2  20407  ovolctb  21652  mbfmulc2re  21806  mbfneg  21808  mbfadd  21819  mbfsub  21820  mbfmulc2  21821  mbfmul  21884  itg2const  21898  itg2mulclem  21904  itg2mulc  21905  itg2splitlem  21906  itg2monolem1  21908  i1fibl  21965  itgitg1  21966  ibladdlem  21977  ibladd  21978  itgaddlem1  21980  iblabslem  21985  iblabs  21986  iblmulc2  21988  itgmulc2lem1  21989  bddmulibl  21996  dvmulf  22097  dvcmulf  22099  dvcof  22102  dvexp  22107  dvmptadd  22114  dvmptmul  22115  dvmptco  22126  dvef  22132  dv11cn  22153  itgsubstlem  22200  mdegmullem  22229  plypf1  22360  plyaddlem1  22361  plymullem1  22362  plyco  22389  dgrcolem1  22420  dgrcolem2  22421  plydiveu  22444  plyremlem  22450  elqaalem3  22467  iaa  22471  taylply2  22513  ulmdvlem1  22545  iblulm  22552  jensenlem2  23061  amgmlem  23063  ftalem7  23096  basellem8  23105  basellem9  23106  dchrmulid2  23271  dchrinvcl  23272  dchrfi  23274  lgseisenlem3  23370  lgseisenlem4  23371  chtppilimlem2  23403  chebbnd2  23406  chto1lb  23407  chpchtlim  23408  chpo1ub  23409  vmadivsum  23411  rpvmasumlem  23416  mudivsum  23459  selberglem1  23474  selberglem2  23475  selberg2lem  23479  selberg2  23480  pntrsumo1  23494  selbergr  23497  ofoprabco  27193  pl1cn  27589  esumadd  27720  ofccat  28153  ofs1  28155  itg2addnclem  29659  itg2addnclem3  29661  ibladdnclem  29664  itgaddnclem1  29666  iblabsnclem  29671  iblabsnc  29672  iblmulc2nc  29673  itgmulc2nclem1  29674  itgmulc2nclem2  29675  itgmulc2nc  29676  itgabsnc  29677  ftc1anclem3  29685  ftc1anclem4  29686  ftc1anclem5  29687  ftc1anclem6  29688  ftc1anclem7  29689  ftc1anclem8  29690  mendlmod  30763  mendassa  30764  expgrowthi  30854  expgrowth  30856  mulcncff  31222  subcncff  31234  addcncff  31239  divcncff  31246  dvsubf  31258  dvdivf  31268  fourierdlem16  31439  fourierdlem21  31444  fourierdlem22  31445  fourierdlem58  31481  fourierdlem59  31482  fourierdlem72  31495  fourierdlem83  31506  offvalfv  32016
  Copyright terms: Public domain W3C validator