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

Theorem offval2 6449
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 2830 . . . . 5  |-  ( ph  ->  A. x  e.  A  B  e.  W )
3 eqid 2454 . . . . . 6  |-  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  B )
43fnmpt 5648 . . . . 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 5612 . . . 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 2830 . . . . 5  |-  ( ph  ->  A. x  e.  A  C  e.  X )
11 eqid 2454 . . . . . 6  |-  ( x  e.  A  |->  C )  =  ( x  e.  A  |->  C )
1211fnmpt 5648 . . . . 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 5612 . . . 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 3670 . . 3  |-  ( A  i^i  A )  =  A
196adantr 465 . . . 4  |-  ( (
ph  /\  y  e.  A )  ->  F  =  ( x  e.  A  |->  B ) )
2019fveq1d 5804 . . 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 5804 . . 3  |-  ( (
ph  /\  y  e.  A )  ->  ( G `  y )  =  ( ( x  e.  A  |->  C ) `
 y ) )
238, 16, 17, 17, 18, 20, 22offval 6440 . 2  |-  ( ph  ->  ( F  oF R G )  =  ( y  e.  A  |->  ( ( ( x  e.  A  |->  B ) `
 y ) R ( ( x  e.  A  |->  C ) `  y ) ) ) )
24 nffvmpt1 5810 . . . . 5  |-  F/_ x
( ( x  e.  A  |->  B ) `  y )
25 nfcv 2616 . . . . 5  |-  F/_ x R
26 nffvmpt1 5810 . . . . 5  |-  F/_ x
( ( x  e.  A  |->  C ) `  y )
2724, 25, 26nfov 6226 . . . 4  |-  F/_ x
( ( ( x  e.  A  |->  B ) `
 y ) R ( ( x  e.  A  |->  C ) `  y ) )
28 nfcv 2616 . . . 4  |-  F/_ y
( ( ( x  e.  A  |->  B ) `
 x ) R ( ( x  e.  A  |->  C ) `  x ) )
29 fveq2 5802 . . . . 5  |-  ( y  =  x  ->  (
( x  e.  A  |->  B ) `  y
)  =  ( ( x  e.  A  |->  B ) `  x ) )
30 fveq2 5802 . . . . 5  |-  ( y  =  x  ->  (
( x  e.  A  |->  C ) `  y
)  =  ( ( x  e.  A  |->  C ) `  x ) )
3129, 30oveq12d 6221 . . . 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 4493 . . 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 5893 . . . . . 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 5893 . . . . . 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 6221 . . . 4  |-  ( (
ph  /\  x  e.  A )  ->  (
( ( x  e.  A  |->  B ) `  x ) R ( ( x  e.  A  |->  C ) `  x
) )  =  ( B R C ) )
3938mpteq2dva 4489 . . 3  |-  ( ph  ->  ( x  e.  A  |->  ( ( ( x  e.  A  |->  B ) `
 x ) R ( ( x  e.  A  |->  C ) `  x ) ) )  =  ( x  e.  A  |->  ( B R C ) ) )
4032, 39syl5eq 2507 . 2  |-  ( ph  ->  ( y  e.  A  |->  ( ( ( x  e.  A  |->  B ) `
 y ) R ( ( x  e.  A  |->  C ) `  y ) ) )  =  ( x  e.  A  |->  ( B R C ) ) )
4123, 40eqtrd 2495 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 1370    e. wcel 1758   A.wral 2799    |-> cmpt 4461    Fn wfn 5524   ` cfv 5529  (class class class)co 6203    oFcof 6431
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-rep 4514  ax-sep 4524  ax-nul 4532  ax-pow 4581  ax-pr 4642
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-ral 2804  df-rex 2805  df-reu 2806  df-rab 2808  df-v 3080  df-sbc 3295  df-csb 3399  df-dif 3442  df-un 3444  df-in 3446  df-ss 3453  df-nul 3749  df-if 3903  df-sn 3989  df-pr 3991  df-op 3995  df-uni 4203  df-iun 4284  df-br 4404  df-opab 4462  df-mpt 4463  df-id 4747  df-xp 4957  df-rel 4958  df-cnv 4959  df-co 4960  df-dm 4961  df-rn 4962  df-res 4963  df-ima 4964  df-iota 5492  df-fun 5531  df-fn 5532  df-f 5533  df-f1 5534  df-fo 5535  df-f1o 5536  df-fv 5537  df-ov 6206  df-oprab 6207  df-mpt2 6208  df-of 6433
This theorem is referenced by:  ofmpteq  6451  ofc12  6458  caofinvl  6460  caofcom  6465  caofass  6467  caofdi  6469  caofdir  6470  caonncan  6471  offval22  6765  o1add2  13222  o1mul2  13223  o1sub2  13224  o1dif  13228  fsumo1  13396  pwsplusgval  14550  pwsmulrval  14551  pwsvscafval  14554  pwsco1mhm  15620  pwsco2mhm  15621  pwssub  15790  gsumzaddlem  16532  gsumzaddlemOLD  16534  gsummptfsadd  16538  gsummptfsaddOLD  16539  gsummptfidmadd2  16541  gsumzsplit  16542  gsumzsplitOLD  16543  gsumsub  16572  gsumsubOLD  16573  dprdfadd  16635  dprdfsub  16636  dprdfeq0  16637  dprdf11  16638  dprdfaddOLD  16642  dprdfsubOLD  16643  dprdfeq0OLD  16644  dprdf11OLD  16645  lmhmvsca  17252  rrgsupp  17488  rrgsuppOLD  17489  psrbagaddcl  17564  psrbagaddclOLD  17565  psrass1lem  17573  psrlinv  17594  psrass1  17604  psrdi  17605  psrdir  17606  psrass23l  17607  psrcom  17608  psrass23  17609  mplsubrglem  17644  mplsubrglemOLD  17645  mplmonmul  17670  mplcoe1  17671  mplcoe3  17672  mplcoe3OLD  17673  mplcoe5  17675  mplcoe2OLD  17677  mplmon2  17702  evlslem1  17728  coe1sclmul  17862  coe1sclmul2  17864  uvcresum  18346  grpvrinv  18424  mhmvlin  18425  mamudi  18435  mamudir  18436  mdetunilem9  18561  tsmssub  19858  tgptsmscls  19859  tsmssplit  19861  tsmsxplem2  19863  ovolctb  21108  mbfmulc2re  21262  mbfneg  21264  mbfadd  21275  mbfsub  21276  mbfmulc2  21277  mbfmul  21340  itg2const  21354  itg2mulclem  21360  itg2mulc  21361  itg2splitlem  21362  itg2monolem1  21364  i1fibl  21421  itgitg1  21422  ibladdlem  21433  ibladd  21434  itgaddlem1  21436  iblabslem  21441  iblabs  21442  iblmulc2  21444  itgmulc2lem1  21445  bddmulibl  21452  dvmulf  21553  dvcmulf  21555  dvcof  21558  dvexp  21563  dvmptadd  21570  dvmptmul  21571  dvmptco  21582  dvef  21588  dv11cn  21609  itgsubstlem  21656  mdegmullem  21685  plypf1  21816  plyaddlem1  21817  plymullem1  21818  plyco  21845  dgrcolem1  21876  dgrcolem2  21877  plydiveu  21900  plyremlem  21906  elqaalem3  21923  iaa  21927  taylply2  21969  ulmdvlem1  22001  iblulm  22008  jensenlem2  22517  amgmlem  22519  ftalem7  22552  basellem8  22561  basellem9  22562  dchrmulid2  22727  dchrinvcl  22728  dchrfi  22730  lgseisenlem3  22826  lgseisenlem4  22827  chtppilimlem2  22859  chebbnd2  22862  chto1lb  22863  chpchtlim  22864  chpo1ub  22865  vmadivsum  22867  rpvmasumlem  22872  mudivsum  22915  selberglem1  22930  selberglem2  22931  selberg2lem  22935  selberg2  22936  pntrsumo1  22950  selbergr  22953  ofoprabco  26153  pl1cn  26550  esumadd  26672  ofccat  27105  ofs1  27107  itg2addnclem  28611  itg2addnclem3  28613  ibladdnclem  28616  itgaddnclem1  28618  iblabsnclem  28623  iblabsnc  28624  iblmulc2nc  28625  itgmulc2nclem1  28626  itgmulc2nclem2  28627  itgmulc2nc  28628  itgabsnc  28629  ftc1anclem3  28637  ftc1anclem4  28638  ftc1anclem5  28639  ftc1anclem6  28640  ftc1anclem7  28641  ftc1anclem8  28642  mendlmod  29718  mendassa  29719  expgrowthi  29775  expgrowth  29777  offvalfv  30901  gsummptfssub  30973
  Copyright terms: Public domain W3C validator