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

Theorem offval2 6331
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 2794 . . . . 5  |-  ( ph  ->  A. x  e.  A  B  e.  W )
3 eqid 2438 . . . . . 6  |-  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  B )
43fnmpt 5532 . . . . 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 5496 . . . 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 2794 . . . . 5  |-  ( ph  ->  A. x  e.  A  C  e.  X )
11 eqid 2438 . . . . . 6  |-  ( x  e.  A  |->  C )  =  ( x  e.  A  |->  C )
1211fnmpt 5532 . . . . 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 5496 . . . 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 3554 . . 3  |-  ( A  i^i  A )  =  A
196adantr 465 . . . 4  |-  ( (
ph  /\  y  e.  A )  ->  F  =  ( x  e.  A  |->  B ) )
2019fveq1d 5688 . . 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 5688 . . 3  |-  ( (
ph  /\  y  e.  A )  ->  ( G `  y )  =  ( ( x  e.  A  |->  C ) `
 y ) )
238, 16, 17, 17, 18, 20, 22offval 6322 . 2  |-  ( ph  ->  ( F  oF R G )  =  ( y  e.  A  |->  ( ( ( x  e.  A  |->  B ) `
 y ) R ( ( x  e.  A  |->  C ) `  y ) ) ) )
24 nffvmpt1 5694 . . . . 5  |-  F/_ x
( ( x  e.  A  |->  B ) `  y )
25 nfcv 2574 . . . . 5  |-  F/_ x R
26 nffvmpt1 5694 . . . . 5  |-  F/_ x
( ( x  e.  A  |->  C ) `  y )
2724, 25, 26nfov 6109 . . . 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 5686 . . . . 5  |-  ( y  =  x  ->  (
( x  e.  A  |->  B ) `  y
)  =  ( ( x  e.  A  |->  B ) `  x ) )
30 fveq2 5686 . . . . 5  |-  ( y  =  x  ->  (
( x  e.  A  |->  C ) `  y
)  =  ( ( x  e.  A  |->  C ) `  x ) )
3129, 30oveq12d 6104 . . . 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 4377 . . 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 5776 . . . . . 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 5776 . . . . . 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 6104 . . . 4  |-  ( (
ph  /\  x  e.  A )  ->  (
( ( x  e.  A  |->  B ) `  x ) R ( ( x  e.  A  |->  C ) `  x
) )  =  ( B R C ) )
3938mpteq2dva 4373 . . 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  oF R G )  =  ( x  e.  A  |->  ( B R C ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1369    e. wcel 1756   A.wral 2710    e. cmpt 4345    Fn wfn 5408   ` cfv 5413  (class class class)co 6086    oFcof 6313
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-rep 4398  ax-sep 4408  ax-nul 4416  ax-pow 4465  ax-pr 4526
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-reu 2717  df-rab 2719  df-v 2969  df-sbc 3182  df-csb 3284  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-iun 4168  df-br 4288  df-opab 4346  df-mpt 4347  df-id 4631  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5376  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-ov 6089  df-oprab 6090  df-mpt2 6091  df-of 6315
This theorem is referenced by:  ofmpteq  6333  ofc12  6340  caofinvl  6342  caofcom  6347  caofass  6349  caofdi  6351  caofdir  6352  caonncan  6353  offval22  6647  o1add2  13093  o1mul2  13094  o1sub2  13095  o1dif  13099  fsumo1  13267  pwsplusgval  14420  pwsmulrval  14421  pwsvscafval  14424  pwsco1mhm  15489  pwsco2mhm  15490  pwssub  15659  gsumzaddlem  16399  gsumzaddlemOLD  16401  gsummptfsadd  16405  gsummptfsaddOLD  16406  gsummptfidmadd2  16408  gsumzsplit  16409  gsumzsplitOLD  16410  gsumsub  16437  gsumsubOLD  16438  dprdfadd  16498  dprdfsub  16499  dprdfeq0  16500  dprdf11  16501  dprdfaddOLD  16505  dprdfsubOLD  16506  dprdfeq0OLD  16507  dprdf11OLD  16508  lmhmvsca  17103  rrgsupp  17339  rrgsuppOLD  17340  psrbagaddcl  17415  psrbagaddclOLD  17416  psrass1lem  17424  psrlinv  17445  psrass1  17455  psrdi  17456  psrdir  17457  psrcom  17458  psrass23  17459  mplsubrglem  17494  mplsubrglemOLD  17495  mplmonmul  17520  mplcoe1  17521  mplcoe3  17522  mplcoe3OLD  17523  mplcoe2  17524  mplcoe2OLD  17525  mplmon2  17550  evlslem1  17576  coe1sclmul  17710  coe1sclmul2  17712  uvcresum  18193  grpvrinv  18271  mhmvlin  18272  mamudi  18282  mamudir  18283  mdetunilem9  18401  tsmssub  19698  tgptsmscls  19699  tsmssplit  19701  tsmsxplem2  19703  ovolctb  20948  mbfmulc2re  21101  mbfneg  21103  mbfadd  21114  mbfsub  21115  mbfmulc2  21116  mbfmul  21179  itg2const  21193  itg2mulclem  21199  itg2mulc  21200  itg2splitlem  21201  itg2monolem1  21203  i1fibl  21260  itgitg1  21261  ibladdlem  21272  ibladd  21273  itgaddlem1  21275  iblabslem  21280  iblabs  21281  iblmulc2  21283  itgmulc2lem1  21284  bddmulibl  21291  dvmulf  21392  dvcmulf  21394  dvcof  21397  dvexp  21402  dvmptadd  21409  dvmptmul  21410  dvmptco  21421  dvef  21427  dv11cn  21448  itgsubstlem  21495  mdegmullem  21524  plypf1  21655  plyaddlem1  21656  plymullem1  21657  plyco  21684  dgrcolem1  21715  dgrcolem2  21716  plydiveu  21739  plyremlem  21745  elqaalem3  21762  iaa  21766  taylply2  21808  ulmdvlem1  21840  iblulm  21847  jensenlem2  22356  amgmlem  22358  ftalem7  22391  basellem8  22400  basellem9  22401  dchrmulid2  22566  dchrinvcl  22567  dchrfi  22569  lgseisenlem3  22665  lgseisenlem4  22666  chtppilimlem2  22698  chebbnd2  22701  chto1lb  22702  chpchtlim  22703  chpo1ub  22704  vmadivsum  22706  rpvmasumlem  22711  mudivsum  22754  selberglem1  22769  selberglem2  22770  selberg2lem  22774  selberg2  22775  pntrsumo1  22789  selbergr  22792  ofoprabco  25933  pl1cn  26337  esumadd  26459  ofccat  26893  ofs1  26895  itg2addnclem  28396  itg2addnclem3  28398  ibladdnclem  28401  itgaddnclem1  28403  iblabsnclem  28408  iblabsnc  28409  iblmulc2nc  28410  itgmulc2nclem1  28411  itgmulc2nclem2  28412  itgmulc2nc  28413  itgabsnc  28414  ftc1anclem3  28422  ftc1anclem4  28423  ftc1anclem5  28424  ftc1anclem6  28425  ftc1anclem7  28426  ftc1anclem8  28427  mendlmod  29503  mendassa  29504  expgrowthi  29560  expgrowth  29562  offvalfv  30685  psrass23l  30763
  Copyright terms: Public domain W3C validator