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

Theorem offval2 6541
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  oF 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 2857 . . . . 5  |-  ( ph  ->  A. x  e.  A  B  e.  W )
3 eqid 2443 . . . . . 6  |-  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  B )
43fnmpt 5697 . . . . 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 5661 . . . 4  |-  ( ph  ->  ( F  Fn  A  <->  ( x  e.  A  |->  B )  Fn  A ) )
85, 7mpbird 232 . . 3  |-  ( ph  ->  F  Fn  A )
9 offval2.3 . . . . . 6  |-  ( (
ph  /\  x  e.  A )  ->  C  e.  X )
109ralrimiva 2857 . . . . 5  |-  ( ph  ->  A. x  e.  A  C  e.  X )
11 eqid 2443 . . . . . 6  |-  ( x  e.  A  |->  C )  =  ( x  e.  A  |->  C )
1211fnmpt 5697 . . . . 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 5661 . . . 4  |-  ( ph  ->  ( G  Fn  A  <->  ( x  e.  A  |->  C )  Fn  A ) )
1613, 15mpbird 232 . . 3  |-  ( ph  ->  G  Fn  A )
17 offval2.1 . . 3  |-  ( ph  ->  A  e.  V )
18 inidm 3692 . . 3  |-  ( A  i^i  A )  =  A
196adantr 465 . . . 4  |-  ( (
ph  /\  y  e.  A )  ->  F  =  ( x  e.  A  |->  B ) )
2019fveq1d 5858 . . 3  |-  ( (
ph  /\  y  e.  A )  ->  ( F `  y )  =  ( ( x  e.  A  |->  B ) `
 y ) )
2114adantr 465 . . . 4  |-  ( (
ph  /\  y  e.  A )  ->  G  =  ( x  e.  A  |->  C ) )
2221fveq1d 5858 . . 3  |-  ( (
ph  /\  y  e.  A )  ->  ( G `  y )  =  ( ( x  e.  A  |->  C ) `
 y ) )
238, 16, 17, 17, 18, 20, 22offval 6532 . 2  |-  ( ph  ->  ( F  oF R G )  =  ( y  e.  A  |->  ( ( ( x  e.  A  |->  B ) `
 y ) R ( ( x  e.  A  |->  C ) `  y ) ) ) )
24 nffvmpt1 5864 . . . . 5  |-  F/_ x
( ( x  e.  A  |->  B ) `  y )
25 nfcv 2605 . . . . 5  |-  F/_ x R
26 nffvmpt1 5864 . . . . 5  |-  F/_ x
( ( x  e.  A  |->  C ) `  y )
2724, 25, 26nfov 6307 . . . 4  |-  F/_ x
( ( ( x  e.  A  |->  B ) `
 y ) R ( ( x  e.  A  |->  C ) `  y ) )
28 nfcv 2605 . . . 4  |-  F/_ y
( ( ( x  e.  A  |->  B ) `
 x ) R ( ( x  e.  A  |->  C ) `  x ) )
29 fveq2 5856 . . . . 5  |-  ( y  =  x  ->  (
( x  e.  A  |->  B ) `  y
)  =  ( ( x  e.  A  |->  B ) `  x ) )
30 fveq2 5856 . . . . 5  |-  ( y  =  x  ->  (
( x  e.  A  |->  C ) `  y
)  =  ( ( x  e.  A  |->  C ) `  x ) )
3129, 30oveq12d 6299 . . . 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 4527 . . 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 461 . . . . . 6  |-  ( (
ph  /\  x  e.  A )  ->  x  e.  A )
343fvmpt2 5948 . . . . . 6  |-  ( ( x  e.  A  /\  B  e.  W )  ->  ( ( x  e.  A  |->  B ) `  x )  =  B )
3533, 1, 34syl2anc 661 . . . . 5  |-  ( (
ph  /\  x  e.  A )  ->  (
( x  e.  A  |->  B ) `  x
)  =  B )
3611fvmpt2 5948 . . . . . 6  |-  ( ( x  e.  A  /\  C  e.  X )  ->  ( ( x  e.  A  |->  C ) `  x )  =  C )
3733, 9, 36syl2anc 661 . . . . 5  |-  ( (
ph  /\  x  e.  A )  ->  (
( x  e.  A  |->  C ) `  x
)  =  C )
3835, 37oveq12d 6299 . . . 4  |-  ( (
ph  /\  x  e.  A )  ->  (
( ( x  e.  A  |->  B ) `  x ) R ( ( x  e.  A  |->  C ) `  x
) )  =  ( B R C ) )
3938mpteq2dva 4523 . . 3  |-  ( ph  ->  ( x  e.  A  |->  ( ( ( x  e.  A  |->  B ) `
 x ) R ( ( x  e.  A  |->  C ) `  x ) ) )  =  ( x  e.  A  |->  ( B R C ) ) )
4032, 39syl5eq 2496 . 2  |-  ( ph  ->  ( y  e.  A  |->  ( ( ( x  e.  A  |->  B ) `
 y ) R ( ( x  e.  A  |->  C ) `  y ) ) )  =  ( x  e.  A  |->  ( B R C ) ) )
4123, 40eqtrd 2484 1  |-  ( ph  ->  ( F  oF R G )  =  ( x  e.  A  |->  ( B R C ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1383    e. wcel 1804   A.wral 2793    |-> cmpt 4495    Fn wfn 5573   ` cfv 5578  (class class class)co 6281    oFcof 6523
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-rep 4548  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-reu 2800  df-rab 2802  df-v 3097  df-sbc 3314  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-iun 4317  df-br 4438  df-opab 4496  df-mpt 4497  df-id 4785  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002  df-iota 5541  df-fun 5580  df-fn 5581  df-f 5582  df-f1 5583  df-fo 5584  df-f1o 5585  df-fv 5586  df-ov 6284  df-oprab 6285  df-mpt2 6286  df-of 6525
This theorem is referenced by:  ofmpteq  6543  ofc12  6550  caofinvl  6552  caofcom  6557  caofass  6559  caofdi  6561  caofdir  6562  caonncan  6563  offval22  6864  o1add2  13428  o1mul2  13429  o1sub2  13430  o1dif  13434  fsumo1  13608  pwsplusgval  14869  pwsmulrval  14870  pwsvscafval  14873  pwsco1mhm  15980  pwsco2mhm  15981  pwssub  16162  gsumzaddlem  16913  gsumzaddlemOLD  16915  gsummptfsadd  16919  gsummptfsaddOLD  16920  gsummptfidmadd2  16922  gsumzsplit  16923  gsumzsplitOLD  16924  gsumsub  16953  gsumsubOLD  16954  gsummptfssub  16955  dprdfadd  17039  dprdfsub  17040  dprdfeq0  17041  dprdf11  17042  dprdfaddOLD  17046  dprdfsubOLD  17047  dprdfeq0OLD  17048  dprdf11OLD  17049  lmhmvsca  17670  rrgsupp  17918  rrgsuppOLD  17919  psrbagaddcl  17999  psrbagaddclOLD  18000  psrass1lem  18008  psrlinv  18029  psrass1  18039  psrdi  18040  psrdir  18041  psrass23l  18042  psrcom  18043  psrass23  18044  mplsubrglem  18079  mplsubrglemOLD  18080  mplmonmul  18105  mplcoe1  18106  mplcoe3  18107  mplcoe3OLD  18108  mplcoe5  18110  mplcoe2OLD  18112  mplmon2  18137  evlslem1  18163  coe1sclmul  18302  coe1sclmul2  18304  uvcresum  18802  grpvrinv  18876  mhmvlin  18877  mamudi  18883  mamudir  18884  mdetunilem9  19100  tsmssub  20629  tgptsmscls  20630  tsmssplit  20632  tsmsxplem2  20634  ovolctb  21879  mbfmulc2re  22033  mbfneg  22035  mbfadd  22046  mbfsub  22047  mbfmulc2  22048  mbfmul  22111  itg2const  22125  itg2mulclem  22131  itg2mulc  22132  itg2splitlem  22133  itg2monolem1  22135  i1fibl  22192  itgitg1  22193  ibladdlem  22204  ibladd  22205  itgaddlem1  22207  iblabslem  22212  iblabs  22213  iblmulc2  22215  itgmulc2lem1  22216  bddmulibl  22223  dvmulf  22324  dvcmulf  22326  dvcof  22329  dvexp  22334  dvmptadd  22341  dvmptmul  22342  dvmptco  22353  dvef  22359  dv11cn  22380  itgsubstlem  22427  mdegmullem  22456  plypf1  22587  plyaddlem1  22588  plymullem1  22589  plyco  22616  dgrcolem1  22648  dgrcolem2  22649  plydiveu  22672  plyremlem  22678  elqaalem3  22695  iaa  22699  taylply2  22741  ulmdvlem1  22773  iblulm  22780  jensenlem2  23295  amgmlem  23297  ftalem7  23330  basellem8  23339  basellem9  23340  dchrmulid2  23505  dchrinvcl  23506  dchrfi  23508  lgseisenlem3  23604  lgseisenlem4  23605  chtppilimlem2  23637  chebbnd2  23640  chto1lb  23641  chpchtlim  23642  chpo1ub  23643  vmadivsum  23645  rpvmasumlem  23650  mudivsum  23693  selberglem1  23708  selberglem2  23709  selberg2lem  23713  selberg2  23714  pntrsumo1  23728  selbergr  23731  ofoprabco  27483  pl1cn  27915  esumadd  28042  ofccat  28475  ofs1  28477  itg2addnclem  30042  itg2addnclem3  30044  ibladdnclem  30047  itgaddnclem1  30049  iblabsnclem  30054  iblabsnc  30055  iblmulc2nc  30056  itgmulc2nclem1  30057  itgmulc2nclem2  30058  itgmulc2nc  30059  itgabsnc  30060  ftc1anclem3  30068  ftc1anclem4  30069  ftc1anclem5  30070  ftc1anclem6  30071  ftc1anclem7  30072  ftc1anclem8  30073  mendlmod  31118  mendassa  31119  expgrowthi  31214  expgrowth  31216  mulcncff  31624  subcncff  31636  addcncff  31641  divcncff  31648  dvsubf  31663  dvdivf  31673  fourierdlem16  31859  fourierdlem21  31864  fourierdlem22  31865  fourierdlem58  31901  fourierdlem59  31902  fourierdlem72  31915  fourierdlem83  31926  offvalfv  32800
  Copyright terms: Public domain W3C validator