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

Theorem offval2 6289
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 2757 . . . . 5  |-  ( ph  ->  A. x  e.  A  B  e.  W )
3 eqid 2412 . . . . . 6  |-  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  B )
43fnmpt 5538 . . . . 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 5503 . . . 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 2757 . . . . 5  |-  ( ph  ->  A. x  e.  A  C  e.  X )
11 eqid 2412 . . . . . 6  |-  ( x  e.  A  |->  C )  =  ( x  e.  A  |->  C )
1211fnmpt 5538 . . . . 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 5503 . . . 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 3518 . . 3  |-  ( A  i^i  A )  =  A
196adantr 452 . . . 4  |-  ( (
ph  /\  y  e.  A )  ->  F  =  ( x  e.  A  |->  B ) )
2019fveq1d 5697 . . 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 5697 . . 3  |-  ( (
ph  /\  y  e.  A )  ->  ( G `  y )  =  ( ( x  e.  A  |->  C ) `
 y ) )
238, 16, 17, 17, 18, 20, 22offval 6279 . 2  |-  ( ph  ->  ( F  o F R G )  =  ( y  e.  A  |->  ( ( ( x  e.  A  |->  B ) `
 y ) R ( ( x  e.  A  |->  C ) `  y ) ) ) )
24 nffvmpt1 5703 . . . . 5  |-  F/_ x
( ( x  e.  A  |->  B ) `  y )
25 nfcv 2548 . . . . 5  |-  F/_ x R
26 nffvmpt1 5703 . . . . 5  |-  F/_ x
( ( x  e.  A  |->  C ) `  y )
2724, 25, 26nfov 6071 . . . 4  |-  F/_ x
( ( ( x  e.  A  |->  B ) `
 y ) R ( ( x  e.  A  |->  C ) `  y ) )
28 nfcv 2548 . . . 4  |-  F/_ y
( ( ( x  e.  A  |->  B ) `
 x ) R ( ( x  e.  A  |->  C ) `  x ) )
29 fveq2 5695 . . . . 5  |-  ( y  =  x  ->  (
( x  e.  A  |->  B ) `  y
)  =  ( ( x  e.  A  |->  B ) `  x ) )
30 fveq2 5695 . . . . 5  |-  ( y  =  x  ->  (
( x  e.  A  |->  C ) `  y
)  =  ( ( x  e.  A  |->  C ) `  x ) )
3129, 30oveq12d 6066 . . . 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 4267 . . 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 5779 . . . . . 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 5779 . . . . . 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 6066 . . . 4  |-  ( (
ph  /\  x  e.  A )  ->  (
( ( x  e.  A  |->  B ) `  x ) R ( ( x  e.  A  |->  C ) `  x
) )  =  ( B R C ) )
3938mpteq2dva 4263 . . 3  |-  ( ph  ->  ( x  e.  A  |->  ( ( ( x  e.  A  |->  B ) `
 x ) R ( ( x  e.  A  |->  C ) `  x ) ) )  =  ( x  e.  A  |->  ( B R C ) ) )
4032, 39syl5eq 2456 . 2  |-  ( ph  ->  ( y  e.  A  |->  ( ( ( x  e.  A  |->  B ) `
 y ) R ( ( x  e.  A  |->  C ) `  y ) ) )  =  ( x  e.  A  |->  ( B R C ) ) )
4123, 40eqtrd 2444 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 1649    e. wcel 1721   A.wral 2674    e. cmpt 4234    Fn wfn 5416   ` cfv 5421  (class class class)co 6048    o Fcof 6270
This theorem is referenced by:  ofc12  6296  caofinvl  6298  caofcom  6303  caofass  6305  caofdi  6307  caofdir  6308  caonncan  6309  o1add2  12380  o1mul2  12381  o1sub2  12382  o1dif  12386  fsumo1  12554  pwsplusgval  13675  pwsmulrval  13676  pwsvscafval  13679  pwsco1mhm  14732  pwsco2mhm  14733  pwssub  14894  gsumzaddlem  15489  gsumzsplit  15492  gsumsub  15505  dprdfadd  15541  dprdfsub  15542  dprdfeq0  15543  dprdf11  15544  lmhmvsca  16084  rrgsupp  16314  psrbagaddcl  16398  psrass1lem  16405  psrlinv  16424  psrass1  16432  psrdi  16433  psrdir  16434  psrcom  16435  psrass23  16436  mplsubrglem  16465  mplmonmul  16490  mplcoe1  16491  mplcoe3  16492  mplcoe2  16493  mplmon2  16516  coe1sclmul  16637  coe1sclmul2  16639  tsmssub  18139  tgptsmscls  18140  tsmssplit  18142  tsmsxplem2  18144  ovolctb  19347  mbfmulc2re  19501  mbfneg  19503  mbfadd  19514  mbfsub  19515  mbfmulc2  19516  mbfmul  19579  itg2const  19593  itg2mulclem  19599  itg2mulc  19600  itg2splitlem  19601  itg2monolem1  19603  i1fibl  19660  itgitg1  19661  ibladdlem  19672  ibladd  19673  itgaddlem1  19675  iblabslem  19680  iblabs  19681  iblmulc2  19683  itgmulc2lem1  19684  bddmulibl  19691  dvmulf  19790  dvcmulf  19792  dvcof  19795  dvexp  19800  dvmptadd  19807  dvmptmul  19808  dvmptco  19819  dvef  19825  dv11cn  19846  itgsubstlem  19893  evlslem1  19897  mdegmullem  19962  plypf1  20092  plyaddlem1  20093  plymullem1  20094  plyco  20121  dgrcolem1  20152  dgrcolem2  20153  plydiveu  20176  plyremlem  20182  elqaalem3  20199  iaa  20203  taylply2  20245  ulmdvlem1  20277  iblulm  20284  jensenlem2  20787  amgmlem  20789  ftalem7  20822  basellem8  20831  basellem9  20832  dchrmulid2  20997  dchrinvcl  20998  dchrfi  21000  lgseisenlem3  21096  lgseisenlem4  21097  chtppilimlem2  21129  chebbnd2  21132  chto1lb  21133  chpchtlim  21134  chpo1ub  21135  vmadivsum  21137  rpvmasumlem  21142  mudivsum  21185  selberglem1  21200  selberglem2  21201  selberg2lem  21205  selberg2  21206  pntrsumo1  21220  selbergr  21223  ofoprabco  24040  esumadd  24409  itg2addnclem  26163  itg2addnclem3  26165  ibladdnclem  26168  itgaddnclem1  26170  iblabsnclem  26175  iblabsnc  26176  iblmulc2nc  26177  itgmulc2nclem1  26178  itgmulc2nclem2  26179  itgmulc2nc  26180  itgabsnc  26181  ofmpteq  26674  uvcresum  27118  grpvrinv  27327  mhmvlin  27328  mamudi  27337  mamudir  27338  mendlmod  27377  mendassa  27378  expgrowthi  27426  expgrowth  27428
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393  ax-rep 4288  ax-sep 4298  ax-nul 4306  ax-pow 4345  ax-pr 4371
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2266  df-mo 2267  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-ne 2577  df-ral 2679  df-rex 2680  df-reu 2681  df-rab 2683  df-v 2926  df-sbc 3130  df-csb 3220  df-dif 3291  df-un 3293  df-in 3295  df-ss 3302  df-nul 3597  df-if 3708  df-sn 3788  df-pr 3789  df-op 3791  df-uni 3984  df-iun 4063  df-br 4181  df-opab 4235  df-mpt 4236  df-id 4466  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-iota 5385  df-fun 5423  df-fn 5424  df-f 5425  df-f1 5426  df-fo 5427  df-f1o 5428  df-fv 5429  df-ov 6051  df-oprab 6052  df-mpt2 6053  df-of 6272
  Copyright terms: Public domain W3C validator