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

Theorem offval2 6325
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 2791 . . . . 5  |-  ( ph  ->  A. x  e.  A  B  e.  W )
3 eqid 2438 . . . . . 6  |-  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  B )
43fnmpt 5574 . . . . 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 5539 . . . 4  |-  ( ph  ->  ( F  Fn  A  <->  ( x  e.  A  |->  B )  Fn  A ) )
85, 7mpbird 225 . . 3  |-  ( ph  ->  F  Fn  A )
9 offval2.3 . . . . . 6  |-  ( (
ph  /\  x  e.  A )  ->  C  e.  X )
109ralrimiva 2791 . . . . 5  |-  ( ph  ->  A. x  e.  A  C  e.  X )
11 eqid 2438 . . . . . 6  |-  ( x  e.  A  |->  C )  =  ( x  e.  A  |->  C )
1211fnmpt 5574 . . . . 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 5539 . . . 4  |-  ( ph  ->  ( G  Fn  A  <->  ( x  e.  A  |->  C )  Fn  A ) )
1613, 15mpbird 225 . . 3  |-  ( ph  ->  G  Fn  A )
17 offval2.1 . . 3  |-  ( ph  ->  A  e.  V )
18 inidm 3552 . . 3  |-  ( A  i^i  A )  =  A
196adantr 453 . . . 4  |-  ( (
ph  /\  y  e.  A )  ->  F  =  ( x  e.  A  |->  B ) )
2019fveq1d 5733 . . 3  |-  ( (
ph  /\  y  e.  A )  ->  ( F `  y )  =  ( ( x  e.  A  |->  B ) `
 y ) )
2114adantr 453 . . . 4  |-  ( (
ph  /\  y  e.  A )  ->  G  =  ( x  e.  A  |->  C ) )
2221fveq1d 5733 . . 3  |-  ( (
ph  /\  y  e.  A )  ->  ( G `  y )  =  ( ( x  e.  A  |->  C ) `
 y ) )
238, 16, 17, 17, 18, 20, 22offval 6315 . 2  |-  ( ph  ->  ( F  o F R G )  =  ( y  e.  A  |->  ( ( ( x  e.  A  |->  B ) `
 y ) R ( ( x  e.  A  |->  C ) `  y ) ) ) )
24 nffvmpt1 5739 . . . . 5  |-  F/_ x
( ( x  e.  A  |->  B ) `  y )
25 nfcv 2574 . . . . 5  |-  F/_ x R
26 nffvmpt1 5739 . . . . 5  |-  F/_ x
( ( x  e.  A  |->  C ) `  y )
2724, 25, 26nfov 6107 . . . 4  |-  F/_ x
( ( ( x  e.  A  |->  B ) `
 y ) R ( ( x  e.  A  |->  C ) `  y ) )
28 nfcv 2574 . . . 4  |-  F/_ y
( ( ( x  e.  A  |->  B ) `
 x ) R ( ( x  e.  A  |->  C ) `  x ) )
29 fveq2 5731 . . . . 5  |-  ( y  =  x  ->  (
( x  e.  A  |->  B ) `  y
)  =  ( ( x  e.  A  |->  B ) `  x ) )
30 fveq2 5731 . . . . 5  |-  ( y  =  x  ->  (
( x  e.  A  |->  C ) `  y
)  =  ( ( x  e.  A  |->  C ) `  x ) )
3129, 30oveq12d 6102 . . . 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 4302 . . 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 449 . . . . . 6  |-  ( (
ph  /\  x  e.  A )  ->  x  e.  A )
343fvmpt2 5815 . . . . . 6  |-  ( ( x  e.  A  /\  B  e.  W )  ->  ( ( x  e.  A  |->  B ) `  x )  =  B )
3533, 1, 34syl2anc 644 . . . . 5  |-  ( (
ph  /\  x  e.  A )  ->  (
( x  e.  A  |->  B ) `  x
)  =  B )
3611fvmpt2 5815 . . . . . 6  |-  ( ( x  e.  A  /\  C  e.  X )  ->  ( ( x  e.  A  |->  C ) `  x )  =  C )
3733, 9, 36syl2anc 644 . . . . 5  |-  ( (
ph  /\  x  e.  A )  ->  (
( x  e.  A  |->  C ) `  x
)  =  C )
3835, 37oveq12d 6102 . . . 4  |-  ( (
ph  /\  x  e.  A )  ->  (
( ( x  e.  A  |->  B ) `  x ) R ( ( x  e.  A  |->  C ) `  x
) )  =  ( B R C ) )
3938mpteq2dva 4298 . . 3  |-  ( ph  ->  ( x  e.  A  |->  ( ( ( x  e.  A  |->  B ) `
 x ) R ( ( x  e.  A  |->  C ) `  x ) ) )  =  ( x  e.  A  |->  ( B R C ) ) )
4032, 39syl5eq 2482 . 2  |-  ( ph  ->  ( y  e.  A  |->  ( ( ( x  e.  A  |->  B ) `
 y ) R ( ( x  e.  A  |->  C ) `  y ) ) )  =  ( x  e.  A  |->  ( B R C ) ) )
4123, 40eqtrd 2470 1  |-  ( ph  ->  ( F  o F R G )  =  ( x  e.  A  |->  ( B R C ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    = wceq 1653    e. wcel 1726   A.wral 2707    e. cmpt 4269    Fn wfn 5452   ` cfv 5457  (class class class)co 6084    o Fcof 6306
This theorem is referenced by:  ofc12  6332  caofinvl  6334  caofcom  6339  caofass  6341  caofdi  6343  caofdir  6344  caonncan  6345  o1add2  12422  o1mul2  12423  o1sub2  12424  o1dif  12428  fsumo1  12596  pwsplusgval  13717  pwsmulrval  13718  pwsvscafval  13721  pwsco1mhm  14774  pwsco2mhm  14775  pwssub  14936  gsumzaddlem  15531  gsumzsplit  15534  gsumsub  15547  dprdfadd  15583  dprdfsub  15584  dprdfeq0  15585  dprdf11  15586  lmhmvsca  16126  rrgsupp  16356  psrbagaddcl  16440  psrass1lem  16447  psrlinv  16466  psrass1  16474  psrdi  16475  psrdir  16476  psrcom  16477  psrass23  16478  mplsubrglem  16507  mplmonmul  16532  mplcoe1  16533  mplcoe3  16534  mplcoe2  16535  mplmon2  16558  coe1sclmul  16679  coe1sclmul2  16681  tsmssub  18183  tgptsmscls  18184  tsmssplit  18186  tsmsxplem2  18188  ovolctb  19391  mbfmulc2re  19543  mbfneg  19545  mbfadd  19556  mbfsub  19557  mbfmulc2  19558  mbfmul  19621  itg2const  19635  itg2mulclem  19641  itg2mulc  19642  itg2splitlem  19643  itg2monolem1  19645  i1fibl  19702  itgitg1  19703  ibladdlem  19714  ibladd  19715  itgaddlem1  19717  iblabslem  19722  iblabs  19723  iblmulc2  19725  itgmulc2lem1  19726  bddmulibl  19733  dvmulf  19834  dvcmulf  19836  dvcof  19839  dvexp  19844  dvmptadd  19851  dvmptmul  19852  dvmptco  19863  dvef  19869  dv11cn  19890  itgsubstlem  19937  evlslem1  19941  mdegmullem  20006  plypf1  20136  plyaddlem1  20137  plymullem1  20138  plyco  20165  dgrcolem1  20196  dgrcolem2  20197  plydiveu  20220  plyremlem  20226  elqaalem3  20243  iaa  20247  taylply2  20289  ulmdvlem1  20321  iblulm  20328  jensenlem2  20831  amgmlem  20833  ftalem7  20866  basellem8  20875  basellem9  20876  dchrmulid2  21041  dchrinvcl  21042  dchrfi  21044  lgseisenlem3  21140  lgseisenlem4  21141  chtppilimlem2  21173  chebbnd2  21176  chto1lb  21177  chpchtlim  21178  chpo1ub  21179  vmadivsum  21181  rpvmasumlem  21186  mudivsum  21229  selberglem1  21244  selberglem2  21245  selberg2lem  21249  selberg2  21250  pntrsumo1  21264  selbergr  21267  ofoprabco  24084  esumadd  24453  itg2addnclem  26270  itg2addnclem3  26272  ibladdnclem  26275  itgaddnclem1  26277  iblabsnclem  26282  iblabsnc  26283  iblmulc2nc  26284  itgmulc2nclem1  26285  itgmulc2nclem2  26286  itgmulc2nc  26287  itgabsnc  26288  ftc1anclem3  26296  ftc1anclem4  26297  ftc1anclem5  26298  ftc1anclem6  26299  ftc1anclem7  26300  ftc1anclem8  26301  ofmpteq  26790  uvcresum  27233  grpvrinv  27442  mhmvlin  27443  mamudi  27452  mamudir  27453  mendlmod  27492  mendassa  27493  expgrowthi  27541  expgrowth  27543
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-rep 4323  ax-sep 4333  ax-nul 4341  ax-pow 4380  ax-pr 4406
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-reu 2714  df-rab 2716  df-v 2960  df-sbc 3164  df-csb 3254  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-iun 4097  df-br 4216  df-opab 4270  df-mpt 4271  df-id 4501  df-xp 4887  df-rel 4888  df-cnv 4889  df-co 4890  df-dm 4891  df-rn 4892  df-res 4893  df-ima 4894  df-iota 5421  df-fun 5459  df-fn 5460  df-f 5461  df-f1 5462  df-fo 5463  df-f1o 5464  df-fv 5465  df-ov 6087  df-oprab 6088  df-mpt2 6089  df-of 6308
  Copyright terms: Public domain W3C validator