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

Theorem offval2 6222
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 2711 . . . . 5  |-  ( ph  ->  A. x  e.  A  B  e.  W )
3 eqid 2366 . . . . . 6  |-  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  B )
43fnmpt 5475 . . . . 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 5440 . . . 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 2711 . . . . 5  |-  ( ph  ->  A. x  e.  A  C  e.  X )
11 eqid 2366 . . . . . 6  |-  ( x  e.  A  |->  C )  =  ( x  e.  A  |->  C )
1211fnmpt 5475 . . . . 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 5440 . . . 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 3466 . . 3  |-  ( A  i^i  A )  =  A
196adantr 451 . . . 4  |-  ( (
ph  /\  y  e.  A )  ->  F  =  ( x  e.  A  |->  B ) )
2019fveq1d 5634 . . 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 5634 . . 3  |-  ( (
ph  /\  y  e.  A )  ->  ( G `  y )  =  ( ( x  e.  A  |->  C ) `
 y ) )
238, 16, 17, 17, 18, 20, 22offval 6212 . 2  |-  ( ph  ->  ( F  o F R G )  =  ( y  e.  A  |->  ( ( ( x  e.  A  |->  B ) `
 y ) R ( ( x  e.  A  |->  C ) `  y ) ) ) )
24 nfmpt1 4211 . . . . . 6  |-  F/_ x
( x  e.  A  |->  B )
25 nfcv 2502 . . . . . 6  |-  F/_ x
y
2624, 25nffv 5639 . . . . 5  |-  F/_ x
( ( x  e.  A  |->  B ) `  y )
27 nfcv 2502 . . . . 5  |-  F/_ x R
28 nfmpt1 4211 . . . . . 6  |-  F/_ x
( x  e.  A  |->  C )
2928, 25nffv 5639 . . . . 5  |-  F/_ x
( ( x  e.  A  |->  C ) `  y )
3026, 27, 29nfov 6004 . . . 4  |-  F/_ x
( ( ( x  e.  A  |->  B ) `
 y ) R ( ( x  e.  A  |->  C ) `  y ) )
31 nfcv 2502 . . . 4  |-  F/_ y
( ( ( x  e.  A  |->  B ) `
 x ) R ( ( x  e.  A  |->  C ) `  x ) )
32 fveq2 5632 . . . . 5  |-  ( y  =  x  ->  (
( x  e.  A  |->  B ) `  y
)  =  ( ( x  e.  A  |->  B ) `  x ) )
33 fveq2 5632 . . . . 5  |-  ( y  =  x  ->  (
( x  e.  A  |->  C ) `  y
)  =  ( ( x  e.  A  |->  C ) `  x ) )
3432, 33oveq12d 5999 . . . 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 4212 . . 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 5715 . . . . . 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 5715 . . . . . 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 5999 . . . 4  |-  ( (
ph  /\  x  e.  A )  ->  (
( ( x  e.  A  |->  B ) `  x ) R ( ( x  e.  A  |->  C ) `  x
) )  =  ( B R C ) )
4241mpteq2dva 4208 . . 3  |-  ( ph  ->  ( x  e.  A  |->  ( ( ( x  e.  A  |->  B ) `
 x ) R ( ( x  e.  A  |->  C ) `  x ) ) )  =  ( x  e.  A  |->  ( B R C ) ) )
4335, 42syl5eq 2410 . 2  |-  ( ph  ->  ( y  e.  A  |->  ( ( ( x  e.  A  |->  B ) `
 y ) R ( ( x  e.  A  |->  C ) `  y ) ) )  =  ( x  e.  A  |->  ( B R C ) ) )
4423, 43eqtrd 2398 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 1647    e. wcel 1715   A.wral 2628    e. cmpt 4179    Fn wfn 5353   ` cfv 5358  (class class class)co 5981    o Fcof 6203
This theorem is referenced by:  ofc12  6229  caofinvl  6231  caofcom  6236  caofass  6238  caofdi  6240  caofdir  6241  caonncan  6242  o1add2  12304  o1mul2  12305  o1sub2  12306  o1dif  12310  fsumo1  12478  pwsplusgval  13599  pwsmulrval  13600  pwsvscafval  13603  pwsco1mhm  14656  pwsco2mhm  14657  pwssub  14818  gsumzaddlem  15413  gsumzsplit  15416  gsumsub  15429  dprdfadd  15465  dprdfsub  15466  dprdfeq0  15467  dprdf11  15468  lmhmvsca  16012  rrgsupp  16242  psrbagaddcl  16326  psrass1lem  16333  psrlinv  16352  psrass1  16360  psrdi  16361  psrdir  16362  psrcom  16363  psrass23  16364  mplsubrglem  16393  mplmonmul  16418  mplcoe1  16419  mplcoe3  16420  mplcoe2  16421  mplmon2  16444  coe1sclmul  16568  coe1sclmul2  16570  tsmssub  18044  tgptsmscls  18045  tsmssplit  18047  tsmsxplem2  18049  ovolctb  19064  mbfmulc2re  19218  mbfneg  19220  mbfadd  19231  mbfsub  19232  mbfmulc2  19233  mbfmul  19296  itg2const  19310  itg2mulclem  19316  itg2mulc  19317  itg2splitlem  19318  itg2monolem1  19320  i1fibl  19377  itgitg1  19378  ibladdlem  19389  ibladd  19390  itgaddlem1  19392  iblabslem  19397  iblabs  19398  iblmulc2  19400  itgmulc2lem1  19401  bddmulibl  19408  dvmulf  19507  dvcmulf  19509  dvcof  19512  dvexp  19517  dvmptadd  19524  dvmptmul  19525  dvmptco  19536  dvef  19542  dv11cn  19563  itgsubstlem  19610  evlslem1  19614  mdegmullem  19679  plypf1  19809  plyaddlem1  19810  plymullem1  19811  plyco  19838  dgrcolem1  19869  dgrcolem2  19870  plydiveu  19893  plyremlem  19899  elqaalem3  19916  iaa  19920  taylply2  19962  ulmdvlem1  19994  iblulm  20001  jensenlem2  20504  amgmlem  20506  ftalem7  20539  basellem8  20548  basellem9  20549  dchrmulid2  20714  dchrinvcl  20715  dchrfi  20717  lgseisenlem3  20813  lgseisenlem4  20814  chtppilimlem2  20846  chebbnd2  20849  chto1lb  20850  chpchtlim  20851  chpo1ub  20852  vmadivsum  20854  rpvmasumlem  20859  mudivsum  20902  selberglem1  20917  selberglem2  20918  selberg2lem  20922  selberg2  20923  pntrsumo1  20937  selbergr  20940  ofoprabco  23603  esumadd  24034  itg2addnclem  25760  itg2addnc  25762  ibladdnclem  25764  itgaddnclem1  25766  iblabsnclem  25771  iblabsnc  25772  iblmulc2nc  25773  itgmulc2nclem1  25774  itgmulc2nclem2  25775  itgmulc2nc  25776  itgabsnc  25777  ofmpteq  26388  uvcresum  26833  grpvrinv  27042  mhmvlin  27043  mamudi  27052  mamudir  27053  mendlmod  27092  mendassa  27093  expgrowthi  27141  expgrowth  27143
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-13 1717  ax-14 1719  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347  ax-rep 4233  ax-sep 4243  ax-nul 4251  ax-pow 4290  ax-pr 4316
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 937  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-eu 2221  df-mo 2222  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-ne 2531  df-ral 2633  df-rex 2634  df-reu 2635  df-rab 2637  df-v 2875  df-sbc 3078  df-csb 3168  df-dif 3241  df-un 3243  df-in 3245  df-ss 3252  df-nul 3544  df-if 3655  df-sn 3735  df-pr 3736  df-op 3738  df-uni 3930  df-iun 4009  df-br 4126  df-opab 4180  df-mpt 4181  df-id 4412  df-xp 4798  df-rel 4799  df-cnv 4800  df-co 4801  df-dm 4802  df-rn 4803  df-res 4804  df-ima 4805  df-iota 5322  df-fun 5360  df-fn 5361  df-f 5362  df-f1 5363  df-fo 5364  df-f1o 5365  df-fv 5366  df-ov 5984  df-oprab 5985  df-mpt2 5986  df-of 6205
  Copyright terms: Public domain W3C validator