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

Theorem offval2 6314
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 2781 . . . . 5  |-  ( ph  ->  A. x  e.  A  B  e.  W )
3 eqid 2435 . . . . . 6  |-  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  B )
43fnmpt 5563 . . . . 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 5528 . . . 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 2781 . . . . 5  |-  ( ph  ->  A. x  e.  A  C  e.  X )
11 eqid 2435 . . . . . 6  |-  ( x  e.  A  |->  C )  =  ( x  e.  A  |->  C )
1211fnmpt 5563 . . . . 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 5528 . . . 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 3542 . . 3  |-  ( A  i^i  A )  =  A
196adantr 452 . . . 4  |-  ( (
ph  /\  y  e.  A )  ->  F  =  ( x  e.  A  |->  B ) )
2019fveq1d 5722 . . 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 5722 . . 3  |-  ( (
ph  /\  y  e.  A )  ->  ( G `  y )  =  ( ( x  e.  A  |->  C ) `
 y ) )
238, 16, 17, 17, 18, 20, 22offval 6304 . 2  |-  ( ph  ->  ( F  o F R G )  =  ( y  e.  A  |->  ( ( ( x  e.  A  |->  B ) `
 y ) R ( ( x  e.  A  |->  C ) `  y ) ) ) )
24 nffvmpt1 5728 . . . . 5  |-  F/_ x
( ( x  e.  A  |->  B ) `  y )
25 nfcv 2571 . . . . 5  |-  F/_ x R
26 nffvmpt1 5728 . . . . 5  |-  F/_ x
( ( x  e.  A  |->  C ) `  y )
2724, 25, 26nfov 6096 . . . 4  |-  F/_ x
( ( ( x  e.  A  |->  B ) `
 y ) R ( ( x  e.  A  |->  C ) `  y ) )
28 nfcv 2571 . . . 4  |-  F/_ y
( ( ( x  e.  A  |->  B ) `
 x ) R ( ( x  e.  A  |->  C ) `  x ) )
29 fveq2 5720 . . . . 5  |-  ( y  =  x  ->  (
( x  e.  A  |->  B ) `  y
)  =  ( ( x  e.  A  |->  B ) `  x ) )
30 fveq2 5720 . . . . 5  |-  ( y  =  x  ->  (
( x  e.  A  |->  C ) `  y
)  =  ( ( x  e.  A  |->  C ) `  x ) )
3129, 30oveq12d 6091 . . . 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 4291 . . 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 5804 . . . . . 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 5804 . . . . . 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 6091 . . . 4  |-  ( (
ph  /\  x  e.  A )  ->  (
( ( x  e.  A  |->  B ) `  x ) R ( ( x  e.  A  |->  C ) `  x
) )  =  ( B R C ) )
3938mpteq2dva 4287 . . 3  |-  ( ph  ->  ( x  e.  A  |->  ( ( ( x  e.  A  |->  B ) `
 x ) R ( ( x  e.  A  |->  C ) `  x ) ) )  =  ( x  e.  A  |->  ( B R C ) ) )
4032, 39syl5eq 2479 . 2  |-  ( ph  ->  ( y  e.  A  |->  ( ( ( x  e.  A  |->  B ) `
 y ) R ( ( x  e.  A  |->  C ) `  y ) ) )  =  ( x  e.  A  |->  ( B R C ) ) )
4123, 40eqtrd 2467 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 2697    e. cmpt 4258    Fn wfn 5441   ` cfv 5446  (class class class)co 6073    o Fcof 6295
This theorem is referenced by:  ofc12  6321  caofinvl  6323  caofcom  6328  caofass  6330  caofdi  6332  caofdir  6333  caonncan  6334  o1add2  12409  o1mul2  12410  o1sub2  12411  o1dif  12415  fsumo1  12583  pwsplusgval  13704  pwsmulrval  13705  pwsvscafval  13708  pwsco1mhm  14761  pwsco2mhm  14762  pwssub  14923  gsumzaddlem  15518  gsumzsplit  15521  gsumsub  15534  dprdfadd  15570  dprdfsub  15571  dprdfeq0  15572  dprdf11  15573  lmhmvsca  16113  rrgsupp  16343  psrbagaddcl  16427  psrass1lem  16434  psrlinv  16453  psrass1  16461  psrdi  16462  psrdir  16463  psrcom  16464  psrass23  16465  mplsubrglem  16494  mplmonmul  16519  mplcoe1  16520  mplcoe3  16521  mplcoe2  16522  mplmon2  16545  coe1sclmul  16666  coe1sclmul2  16668  tsmssub  18170  tgptsmscls  18171  tsmssplit  18173  tsmsxplem2  18175  ovolctb  19378  mbfmulc2re  19532  mbfneg  19534  mbfadd  19545  mbfsub  19546  mbfmulc2  19547  mbfmul  19610  itg2const  19624  itg2mulclem  19630  itg2mulc  19631  itg2splitlem  19632  itg2monolem1  19634  i1fibl  19691  itgitg1  19692  ibladdlem  19703  ibladd  19704  itgaddlem1  19706  iblabslem  19711  iblabs  19712  iblmulc2  19714  itgmulc2lem1  19715  bddmulibl  19722  dvmulf  19821  dvcmulf  19823  dvcof  19826  dvexp  19831  dvmptadd  19838  dvmptmul  19839  dvmptco  19850  dvef  19856  dv11cn  19877  itgsubstlem  19924  evlslem1  19928  mdegmullem  19993  plypf1  20123  plyaddlem1  20124  plymullem1  20125  plyco  20152  dgrcolem1  20183  dgrcolem2  20184  plydiveu  20207  plyremlem  20213  elqaalem3  20230  iaa  20234  taylply2  20276  ulmdvlem1  20308  iblulm  20315  jensenlem2  20818  amgmlem  20820  ftalem7  20853  basellem8  20862  basellem9  20863  dchrmulid2  21028  dchrinvcl  21029  dchrfi  21031  lgseisenlem3  21127  lgseisenlem4  21128  chtppilimlem2  21160  chebbnd2  21163  chto1lb  21164  chpchtlim  21165  chpo1ub  21166  vmadivsum  21168  rpvmasumlem  21173  mudivsum  21216  selberglem1  21231  selberglem2  21232  selberg2lem  21236  selberg2  21237  pntrsumo1  21251  selbergr  21254  ofoprabco  24071  esumadd  24440  itg2addnclem  26246  itg2addnclem3  26248  ibladdnclem  26251  itgaddnclem1  26253  iblabsnclem  26258  iblabsnc  26259  iblmulc2nc  26260  itgmulc2nclem1  26261  itgmulc2nclem2  26262  itgmulc2nc  26263  itgabsnc  26264  ofmpteq  26757  uvcresum  27200  grpvrinv  27409  mhmvlin  27410  mamudi  27419  mamudir  27420  mendlmod  27459  mendassa  27460  expgrowthi  27508  expgrowth  27510
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 2416  ax-rep 4312  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395
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 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-reu 2704  df-rab 2706  df-v 2950  df-sbc 3154  df-csb 3244  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-uni 4008  df-iun 4087  df-br 4205  df-opab 4259  df-mpt 4260  df-id 4490  df-xp 4876  df-rel 4877  df-cnv 4878  df-co 4879  df-dm 4880  df-rn 4881  df-res 4882  df-ima 4883  df-iota 5410  df-fun 5448  df-fn 5449  df-f 5450  df-f1 5451  df-fo 5452  df-f1o 5453  df-fv 5454  df-ov 6076  df-oprab 6077  df-mpt2 6078  df-of 6297
  Copyright terms: Public domain W3C validator