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

Theorem offval2 6322
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 2789 . . . . 5  |-  ( ph  ->  A. x  e.  A  B  e.  W )
3 eqid 2436 . . . . . 6  |-  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  B )
43fnmpt 5571 . . . . 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 5536 . . . 4  |-  ( ph  ->  ( F  Fn  A  <->  ( x  e.  A  |->  B )  Fn  A ) )
85, 7mpbird 224 . . 3  |-  ( ph  ->  F  Fn  A )
9 offval2.3 . . . . . 6  |-  ( (
ph  /\  x  e.  A )  ->  C  e.  X )
109ralrimiva 2789 . . . . 5  |-  ( ph  ->  A. x  e.  A  C  e.  X )
11 eqid 2436 . . . . . 6  |-  ( x  e.  A  |->  C )  =  ( x  e.  A  |->  C )
1211fnmpt 5571 . . . . 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 5536 . . . 4  |-  ( ph  ->  ( G  Fn  A  <->  ( x  e.  A  |->  C )  Fn  A ) )
1613, 15mpbird 224 . . 3  |-  ( ph  ->  G  Fn  A )
17 offval2.1 . . 3  |-  ( ph  ->  A  e.  V )
18 inidm 3550 . . 3  |-  ( A  i^i  A )  =  A
196adantr 452 . . . 4  |-  ( (
ph  /\  y  e.  A )  ->  F  =  ( x  e.  A  |->  B ) )
2019fveq1d 5730 . . 3  |-  ( (
ph  /\  y  e.  A )  ->  ( F `  y )  =  ( ( x  e.  A  |->  B ) `
 y ) )
2114adantr 452 . . . 4  |-  ( (
ph  /\  y  e.  A )  ->  G  =  ( x  e.  A  |->  C ) )
2221fveq1d 5730 . . 3  |-  ( (
ph  /\  y  e.  A )  ->  ( G `  y )  =  ( ( x  e.  A  |->  C ) `
 y ) )
238, 16, 17, 17, 18, 20, 22offval 6312 . 2  |-  ( ph  ->  ( F  o F R G )  =  ( y  e.  A  |->  ( ( ( x  e.  A  |->  B ) `
 y ) R ( ( x  e.  A  |->  C ) `  y ) ) ) )
24 nffvmpt1 5736 . . . . 5  |-  F/_ x
( ( x  e.  A  |->  B ) `  y )
25 nfcv 2572 . . . . 5  |-  F/_ x R
26 nffvmpt1 5736 . . . . 5  |-  F/_ x
( ( x  e.  A  |->  C ) `  y )
2724, 25, 26nfov 6104 . . . 4  |-  F/_ x
( ( ( x  e.  A  |->  B ) `
 y ) R ( ( x  e.  A  |->  C ) `  y ) )
28 nfcv 2572 . . . 4  |-  F/_ y
( ( ( x  e.  A  |->  B ) `
 x ) R ( ( x  e.  A  |->  C ) `  x ) )
29 fveq2 5728 . . . . 5  |-  ( y  =  x  ->  (
( x  e.  A  |->  B ) `  y
)  =  ( ( x  e.  A  |->  B ) `  x ) )
30 fveq2 5728 . . . . 5  |-  ( y  =  x  ->  (
( x  e.  A  |->  C ) `  y
)  =  ( ( x  e.  A  |->  C ) `  x ) )
3129, 30oveq12d 6099 . . . 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 4299 . . 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 448 . . . . . 6  |-  ( (
ph  /\  x  e.  A )  ->  x  e.  A )
343fvmpt2 5812 . . . . . 6  |-  ( ( x  e.  A  /\  B  e.  W )  ->  ( ( x  e.  A  |->  B ) `  x )  =  B )
3533, 1, 34syl2anc 643 . . . . 5  |-  ( (
ph  /\  x  e.  A )  ->  (
( x  e.  A  |->  B ) `  x
)  =  B )
3611fvmpt2 5812 . . . . . 6  |-  ( ( x  e.  A  /\  C  e.  X )  ->  ( ( x  e.  A  |->  C ) `  x )  =  C )
3733, 9, 36syl2anc 643 . . . . 5  |-  ( (
ph  /\  x  e.  A )  ->  (
( x  e.  A  |->  C ) `  x
)  =  C )
3835, 37oveq12d 6099 . . . 4  |-  ( (
ph  /\  x  e.  A )  ->  (
( ( x  e.  A  |->  B ) `  x ) R ( ( x  e.  A  |->  C ) `  x
) )  =  ( B R C ) )
3938mpteq2dva 4295 . . 3  |-  ( ph  ->  ( x  e.  A  |->  ( ( ( x  e.  A  |->  B ) `
 x ) R ( ( x  e.  A  |->  C ) `  x ) ) )  =  ( x  e.  A  |->  ( B R C ) ) )
4032, 39syl5eq 2480 . 2  |-  ( ph  ->  ( y  e.  A  |->  ( ( ( x  e.  A  |->  B ) `
 y ) R ( ( x  e.  A  |->  C ) `  y ) ) )  =  ( x  e.  A  |->  ( B R C ) ) )
4123, 40eqtrd 2468 1  |-  ( ph  ->  ( F  o F R G )  =  ( x  e.  A  |->  ( B R C ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1652    e. wcel 1725   A.wral 2705    e. cmpt 4266    Fn wfn 5449   ` cfv 5454  (class class class)co 6081    o Fcof 6303
This theorem is referenced by:  ofc12  6329  caofinvl  6331  caofcom  6336  caofass  6338  caofdi  6340  caofdir  6341  caonncan  6342  o1add2  12417  o1mul2  12418  o1sub2  12419  o1dif  12423  fsumo1  12591  pwsplusgval  13712  pwsmulrval  13713  pwsvscafval  13716  pwsco1mhm  14769  pwsco2mhm  14770  pwssub  14931  gsumzaddlem  15526  gsumzsplit  15529  gsumsub  15542  dprdfadd  15578  dprdfsub  15579  dprdfeq0  15580  dprdf11  15581  lmhmvsca  16121  rrgsupp  16351  psrbagaddcl  16435  psrass1lem  16442  psrlinv  16461  psrass1  16469  psrdi  16470  psrdir  16471  psrcom  16472  psrass23  16473  mplsubrglem  16502  mplmonmul  16527  mplcoe1  16528  mplcoe3  16529  mplcoe2  16530  mplmon2  16553  coe1sclmul  16674  coe1sclmul2  16676  tsmssub  18178  tgptsmscls  18179  tsmssplit  18181  tsmsxplem2  18183  ovolctb  19386  mbfmulc2re  19540  mbfneg  19542  mbfadd  19553  mbfsub  19554  mbfmulc2  19555  mbfmul  19618  itg2const  19632  itg2mulclem  19638  itg2mulc  19639  itg2splitlem  19640  itg2monolem1  19642  i1fibl  19699  itgitg1  19700  ibladdlem  19711  ibladd  19712  itgaddlem1  19714  iblabslem  19719  iblabs  19720  iblmulc2  19722  itgmulc2lem1  19723  bddmulibl  19730  dvmulf  19829  dvcmulf  19831  dvcof  19834  dvexp  19839  dvmptadd  19846  dvmptmul  19847  dvmptco  19858  dvef  19864  dv11cn  19885  itgsubstlem  19932  evlslem1  19936  mdegmullem  20001  plypf1  20131  plyaddlem1  20132  plymullem1  20133  plyco  20160  dgrcolem1  20191  dgrcolem2  20192  plydiveu  20215  plyremlem  20221  elqaalem3  20238  iaa  20242  taylply2  20284  ulmdvlem1  20316  iblulm  20323  jensenlem2  20826  amgmlem  20828  ftalem7  20861  basellem8  20870  basellem9  20871  dchrmulid2  21036  dchrinvcl  21037  dchrfi  21039  lgseisenlem3  21135  lgseisenlem4  21136  chtppilimlem2  21168  chebbnd2  21171  chto1lb  21172  chpchtlim  21173  chpo1ub  21174  vmadivsum  21176  rpvmasumlem  21181  mudivsum  21224  selberglem1  21239  selberglem2  21240  selberg2lem  21244  selberg2  21245  pntrsumo1  21259  selbergr  21262  ofoprabco  24079  esumadd  24448  itg2addnclem  26256  itg2addnclem3  26258  ibladdnclem  26261  itgaddnclem1  26263  iblabsnclem  26268  iblabsnc  26269  iblmulc2nc  26270  itgmulc2nclem1  26271  itgmulc2nclem2  26272  itgmulc2nc  26273  itgabsnc  26274  ftc1anclem3  26282  ftc1anclem4  26283  ftc1anclem5  26284  ftc1anclem6  26285  ftc1anclem7  26286  ftc1anclem8  26287  ofmpteq  26776  uvcresum  27219  grpvrinv  27428  mhmvlin  27429  mamudi  27438  mamudir  27439  mendlmod  27478  mendassa  27479  expgrowthi  27527  expgrowth  27529
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417  ax-rep 4320  ax-sep 4330  ax-nul 4338  ax-pow 4377  ax-pr 4403
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2285  df-mo 2286  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ne 2601  df-ral 2710  df-rex 2711  df-reu 2712  df-rab 2714  df-v 2958  df-sbc 3162  df-csb 3252  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-nul 3629  df-if 3740  df-sn 3820  df-pr 3821  df-op 3823  df-uni 4016  df-iun 4095  df-br 4213  df-opab 4267  df-mpt 4268  df-id 4498  df-xp 4884  df-rel 4885  df-cnv 4886  df-co 4887  df-dm 4888  df-rn 4889  df-res 4890  df-ima 4891  df-iota 5418  df-fun 5456  df-fn 5457  df-f 5458  df-f1 5459  df-fo 5460  df-f1o 5461  df-fv 5462  df-ov 6084  df-oprab 6085  df-mpt2 6086  df-of 6305
  Copyright terms: Public domain W3C validator