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

Theorem offval2 6095
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  o F 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 2626 . . . . 5  |-  ( ph  ->  A. x  e.  A  B  e.  W )
3 eqid 2283 . . . . . 6  |-  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  B )
43fnmpt 5370 . . . . 5  |-  ( A. x  e.  A  B  e.  W  ->  ( x  e.  A  |->  B )  Fn  A )
52, 4syl 15 . . . 4  |-  ( ph  ->  ( x  e.  A  |->  B )  Fn  A
)
6 offval2.4 . . . . 5  |-  ( ph  ->  F  =  ( x  e.  A  |->  B ) )
76fneq1d 5335 . . . 4  |-  ( ph  ->  ( F  Fn  A  <->  ( x  e.  A  |->  B )  Fn  A ) )
85, 7mpbird 223 . . 3  |-  ( ph  ->  F  Fn  A )
9 offval2.3 . . . . . 6  |-  ( (
ph  /\  x  e.  A )  ->  C  e.  X )
109ralrimiva 2626 . . . . 5  |-  ( ph  ->  A. x  e.  A  C  e.  X )
11 eqid 2283 . . . . . 6  |-  ( x  e.  A  |->  C )  =  ( x  e.  A  |->  C )
1211fnmpt 5370 . . . . 5  |-  ( A. x  e.  A  C  e.  X  ->  ( x  e.  A  |->  C )  Fn  A )
1310, 12syl 15 . . . 4  |-  ( ph  ->  ( x  e.  A  |->  C )  Fn  A
)
14 offval2.5 . . . . 5  |-  ( ph  ->  G  =  ( x  e.  A  |->  C ) )
1514fneq1d 5335 . . . 4  |-  ( ph  ->  ( G  Fn  A  <->  ( x  e.  A  |->  C )  Fn  A ) )
1613, 15mpbird 223 . . 3  |-  ( ph  ->  G  Fn  A )
17 offval2.1 . . 3  |-  ( ph  ->  A  e.  V )
18 inidm 3378 . . 3  |-  ( A  i^i  A )  =  A
196adantr 451 . . . 4  |-  ( (
ph  /\  y  e.  A )  ->  F  =  ( x  e.  A  |->  B ) )
2019fveq1d 5527 . . 3  |-  ( (
ph  /\  y  e.  A )  ->  ( F `  y )  =  ( ( x  e.  A  |->  B ) `
 y ) )
2114adantr 451 . . . 4  |-  ( (
ph  /\  y  e.  A )  ->  G  =  ( x  e.  A  |->  C ) )
2221fveq1d 5527 . . 3  |-  ( (
ph  /\  y  e.  A )  ->  ( G `  y )  =  ( ( x  e.  A  |->  C ) `
 y ) )
238, 16, 17, 17, 18, 20, 22offval 6085 . 2  |-  ( ph  ->  ( F  o F R G )  =  ( y  e.  A  |->  ( ( ( x  e.  A  |->  B ) `
 y ) R ( ( x  e.  A  |->  C ) `  y ) ) ) )
24 nfmpt1 4109 . . . . . 6  |-  F/_ x
( x  e.  A  |->  B )
25 nfcv 2419 . . . . . 6  |-  F/_ x
y
2624, 25nffv 5532 . . . . 5  |-  F/_ x
( ( x  e.  A  |->  B ) `  y )
27 nfcv 2419 . . . . 5  |-  F/_ x R
28 nfmpt1 4109 . . . . . 6  |-  F/_ x
( x  e.  A  |->  C )
2928, 25nffv 5532 . . . . 5  |-  F/_ x
( ( x  e.  A  |->  C ) `  y )
3026, 27, 29nfov 5881 . . . 4  |-  F/_ x
( ( ( x  e.  A  |->  B ) `
 y ) R ( ( x  e.  A  |->  C ) `  y ) )
31 nfcv 2419 . . . 4  |-  F/_ y
( ( ( x  e.  A  |->  B ) `
 x ) R ( ( x  e.  A  |->  C ) `  x ) )
32 fveq2 5525 . . . . 5  |-  ( y  =  x  ->  (
( x  e.  A  |->  B ) `  y
)  =  ( ( x  e.  A  |->  B ) `  x ) )
33 fveq2 5525 . . . . 5  |-  ( y  =  x  ->  (
( x  e.  A  |->  C ) `  y
)  =  ( ( x  e.  A  |->  C ) `  x ) )
3432, 33oveq12d 5876 . . . 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
) ) )
3530, 31, 34cbvmpt 4110 . . 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
) ) )
36 simpr 447 . . . . . 6  |-  ( (
ph  /\  x  e.  A )  ->  x  e.  A )
373fvmpt2 5608 . . . . . 6  |-  ( ( x  e.  A  /\  B  e.  W )  ->  ( ( x  e.  A  |->  B ) `  x )  =  B )
3836, 1, 37syl2anc 642 . . . . 5  |-  ( (
ph  /\  x  e.  A )  ->  (
( x  e.  A  |->  B ) `  x
)  =  B )
3911fvmpt2 5608 . . . . . 6  |-  ( ( x  e.  A  /\  C  e.  X )  ->  ( ( x  e.  A  |->  C ) `  x )  =  C )
4036, 9, 39syl2anc 642 . . . . 5  |-  ( (
ph  /\  x  e.  A )  ->  (
( x  e.  A  |->  C ) `  x
)  =  C )
4138, 40oveq12d 5876 . . . 4  |-  ( (
ph  /\  x  e.  A )  ->  (
( ( x  e.  A  |->  B ) `  x ) R ( ( x  e.  A  |->  C ) `  x
) )  =  ( B R C ) )
4241mpteq2dva 4106 . . 3  |-  ( ph  ->  ( x  e.  A  |->  ( ( ( x  e.  A  |->  B ) `
 x ) R ( ( x  e.  A  |->  C ) `  x ) ) )  =  ( x  e.  A  |->  ( B R C ) ) )
4335, 42syl5eq 2327 . 2  |-  ( ph  ->  ( y  e.  A  |->  ( ( ( x  e.  A  |->  B ) `
 y ) R ( ( x  e.  A  |->  C ) `  y ) ) )  =  ( x  e.  A  |->  ( B R C ) ) )
4423, 43eqtrd 2315 1  |-  ( ph  ->  ( F  o F R G )  =  ( x  e.  A  |->  ( B R C ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1623    e. wcel 1684   A.wral 2543    e. cmpt 4077    Fn wfn 5250   ` cfv 5255  (class class class)co 5858    o Fcof 6076
This theorem is referenced by:  ofc12  6102  caofinvl  6104  caofcom  6109  caofass  6111  caofdi  6113  caofdir  6114  caonncan  6115  o1add2  12097  o1mul2  12098  o1sub2  12099  o1dif  12103  fsumo1  12270  pwsplusgval  13389  pwsmulrval  13390  pwsvscafval  13393  pwsco1mhm  14446  pwsco2mhm  14447  pwssub  14608  gsumzaddlem  15203  gsumzsplit  15206  gsumsub  15219  dprdfadd  15255  dprdfsub  15256  dprdfeq0  15257  dprdf11  15258  lmhmvsca  15802  rrgsupp  16032  psrbagaddcl  16116  psrass1lem  16123  psrlinv  16142  psrass1  16150  psrdi  16151  psrdir  16152  psrcom  16153  psrass23  16154  mplsubrglem  16183  mplmonmul  16208  mplcoe1  16209  mplcoe3  16210  mplcoe2  16211  mplmon2  16234  coe1sclmul  16358  coe1sclmul2  16360  tsmssub  17831  tgptsmscls  17832  tsmssplit  17834  tsmsxplem2  17836  ovolctb  18849  mbfmulc2re  19003  mbfneg  19005  mbfadd  19016  mbfsub  19017  mbfmulc2  19018  mbfmul  19081  itg2const  19095  itg2mulclem  19101  itg2mulc  19102  itg2splitlem  19103  itg2monolem1  19105  i1fibl  19162  itgitg1  19163  ibladdlem  19174  ibladd  19175  itgaddlem1  19177  iblabslem  19182  iblabs  19183  iblmulc2  19185  itgmulc2lem1  19186  bddmulibl  19193  dvmulf  19292  dvcmulf  19294  dvcof  19297  dvexp  19302  dvmptadd  19309  dvmptmul  19310  dvmptco  19321  dvef  19327  dv11cn  19348  itgsubstlem  19395  evlslem1  19399  mdegmullem  19464  plypf1  19594  plyaddlem1  19595  plymullem1  19596  plyco  19623  dgrcolem1  19654  dgrcolem2  19655  plydiveu  19678  plyremlem  19684  elqaalem3  19701  iaa  19705  taylply2  19747  ulmdvlem1  19777  iblulm  19783  jensenlem2  20282  amgmlem  20284  ftalem7  20316  basellem8  20325  basellem9  20326  dchrmulid2  20491  dchrinvcl  20492  dchrfi  20494  lgseisenlem3  20590  lgseisenlem4  20591  chtppilimlem2  20623  chebbnd2  20626  chto1lb  20627  chpchtlim  20628  chpo1ub  20629  vmadivsum  20631  rpvmasumlem  20636  mudivsum  20679  selberglem1  20694  selberglem2  20695  selberg2lem  20699  selberg2  20700  pntrsumo1  20714  selbergr  20717  ofoprabco  23232  esumadd  23432  ofmpteq  26797  uvcresum  27242  grpvrinv  27451  mhmvlin  27452  mamudi  27461  mamudir  27462  mendlmod  27501  mendassa  27502  expgrowthi  27550  expgrowth  27552
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-rep 4131  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-reu 2550  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-iun 3907  df-br 4024  df-opab 4078  df-mpt 4079  df-id 4309  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263  df-ov 5861  df-oprab 5862  df-mpt2 5863  df-of 6078
  Copyright terms: Public domain W3C validator