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  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 2789 . . . . 5  |-  ( ph  ->  A. x  e.  A  B  e.  W )
3 eqid 2433 . . . . . 6  |-  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  B )
43fnmpt 5525 . . . . 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 5489 . . . 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 2789 . . . . 5  |-  ( ph  ->  A. x  e.  A  C  e.  X )
11 eqid 2433 . . . . . 6  |-  ( x  e.  A  |->  C )  =  ( x  e.  A  |->  C )
1211fnmpt 5525 . . . . 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 5489 . . . 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 3547 . . 3  |-  ( A  i^i  A )  =  A
196adantr 462 . . . 4  |-  ( (
ph  /\  y  e.  A )  ->  F  =  ( x  e.  A  |->  B ) )
2019fveq1d 5681 . . 3  |-  ( (
ph  /\  y  e.  A )  ->  ( F `  y )  =  ( ( x  e.  A  |->  B ) `
 y ) )
2114adantr 462 . . . 4  |-  ( (
ph  /\  y  e.  A )  ->  G  =  ( x  e.  A  |->  C ) )
2221fveq1d 5681 . . 3  |-  ( (
ph  /\  y  e.  A )  ->  ( G `  y )  =  ( ( x  e.  A  |->  C ) `
 y ) )
238, 16, 17, 17, 18, 20, 22offval 6316 . 2  |-  ( ph  ->  ( F  oF R G )  =  ( y  e.  A  |->  ( ( ( x  e.  A  |->  B ) `
 y ) R ( ( x  e.  A  |->  C ) `  y ) ) ) )
24 nffvmpt1 5687 . . . . 5  |-  F/_ x
( ( x  e.  A  |->  B ) `  y )
25 nfcv 2569 . . . . 5  |-  F/_ x R
26 nffvmpt1 5687 . . . . 5  |-  F/_ x
( ( x  e.  A  |->  C ) `  y )
2724, 25, 26nfov 6103 . . . 4  |-  F/_ x
( ( ( x  e.  A  |->  B ) `
 y ) R ( ( x  e.  A  |->  C ) `  y ) )
28 nfcv 2569 . . . 4  |-  F/_ y
( ( ( x  e.  A  |->  B ) `
 x ) R ( ( x  e.  A  |->  C ) `  x ) )
29 fveq2 5679 . . . . 5  |-  ( y  =  x  ->  (
( x  e.  A  |->  B ) `  y
)  =  ( ( x  e.  A  |->  B ) `  x ) )
30 fveq2 5679 . . . . 5  |-  ( y  =  x  ->  (
( x  e.  A  |->  C ) `  y
)  =  ( ( x  e.  A  |->  C ) `  x ) )
3129, 30oveq12d 6098 . . . 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 4370 . . 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 458 . . . . . 6  |-  ( (
ph  /\  x  e.  A )  ->  x  e.  A )
343fvmpt2 5769 . . . . . 6  |-  ( ( x  e.  A  /\  B  e.  W )  ->  ( ( x  e.  A  |->  B ) `  x )  =  B )
3533, 1, 34syl2anc 654 . . . . 5  |-  ( (
ph  /\  x  e.  A )  ->  (
( x  e.  A  |->  B ) `  x
)  =  B )
3611fvmpt2 5769 . . . . . 6  |-  ( ( x  e.  A  /\  C  e.  X )  ->  ( ( x  e.  A  |->  C ) `  x )  =  C )
3733, 9, 36syl2anc 654 . . . . 5  |-  ( (
ph  /\  x  e.  A )  ->  (
( x  e.  A  |->  C ) `  x
)  =  C )
3835, 37oveq12d 6098 . . . 4  |-  ( (
ph  /\  x  e.  A )  ->  (
( ( x  e.  A  |->  B ) `  x ) R ( ( x  e.  A  |->  C ) `  x
) )  =  ( B R C ) )
3938mpteq2dva 4366 . . 3  |-  ( ph  ->  ( x  e.  A  |->  ( ( ( x  e.  A  |->  B ) `
 x ) R ( ( x  e.  A  |->  C ) `  x ) ) )  =  ( x  e.  A  |->  ( B R C ) ) )
4032, 39syl5eq 2477 . 2  |-  ( ph  ->  ( y  e.  A  |->  ( ( ( x  e.  A  |->  B ) `
 y ) R ( ( x  e.  A  |->  C ) `  y ) ) )  =  ( x  e.  A  |->  ( B R C ) ) )
4123, 40eqtrd 2465 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 1362    e. wcel 1755   A.wral 2705    e. cmpt 4338    Fn wfn 5401   ` cfv 5406  (class class class)co 6080    oFcof 6307
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-rep 4391  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-reu 2712  df-rab 2714  df-v 2964  df-sbc 3176  df-csb 3277  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-iun 4161  df-br 4281  df-opab 4339  df-mpt 4340  df-id 4623  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-iota 5369  df-fun 5408  df-fn 5409  df-f 5410  df-f1 5411  df-fo 5412  df-f1o 5413  df-fv 5414  df-ov 6083  df-oprab 6084  df-mpt2 6085  df-of 6309
This theorem is referenced by:  ofmpteq  6327  ofc12  6334  caofinvl  6336  caofcom  6341  caofass  6343  caofdi  6345  caofdir  6346  caonncan  6347  offval22  6641  o1add2  13084  o1mul2  13085  o1sub2  13086  o1dif  13090  fsumo1  13257  pwsplusgval  14410  pwsmulrval  14411  pwsvscafval  14414  pwsco1mhm  15479  pwsco2mhm  15480  pwssub  15647  gsumzaddlem  16387  gsumzaddlemOLD  16389  gsummptfsadd  16393  gsummptfsaddOLD  16394  gsummptfidmadd2  16396  gsumzsplit  16397  gsumzsplitOLD  16398  gsumsub  16422  gsumsubOLD  16423  dprdfadd  16483  dprdfsub  16484  dprdfeq0  16485  dprdf11  16486  dprdfaddOLD  16490  dprdfsubOLD  16491  dprdfeq0OLD  16492  dprdf11OLD  16493  lmhmvsca  17047  rrgsupp  17283  rrgsuppOLD  17284  psrbagaddcl  17371  psrbagaddclOLD  17372  psrass1lem  17380  psrlinv  17401  psrass1  17411  psrdi  17412  psrdir  17413  psrcom  17414  psrass23  17415  mplsubrglem  17450  mplsubrglemOLD  17451  mplmonmul  17476  mplcoe1  17477  mplcoe3  17478  mplcoe3OLD  17479  mplcoe2  17480  mplcoe2OLD  17481  mplmon2  17506  coe1sclmul  17632  coe1sclmul2  17634  uvcresum  18059  grpvrinv  18137  mhmvlin  18138  mamudi  18148  mamudir  18149  mdetunilem9  18267  tsmssub  19564  tgptsmscls  19565  tsmssplit  19567  tsmsxplem2  19569  ovolctb  20814  mbfmulc2re  20967  mbfneg  20969  mbfadd  20980  mbfsub  20981  mbfmulc2  20982  mbfmul  21045  itg2const  21059  itg2mulclem  21065  itg2mulc  21066  itg2splitlem  21067  itg2monolem1  21069  i1fibl  21126  itgitg1  21127  ibladdlem  21138  ibladd  21139  itgaddlem1  21141  iblabslem  21146  iblabs  21147  iblmulc2  21149  itgmulc2lem1  21150  bddmulibl  21157  dvmulf  21258  dvcmulf  21260  dvcof  21263  dvexp  21268  dvmptadd  21275  dvmptmul  21276  dvmptco  21287  dvef  21293  dv11cn  21314  itgsubstlem  21361  evlslem1  21366  mdegmullem  21433  plypf1  21564  plyaddlem1  21565  plymullem1  21566  plyco  21593  dgrcolem1  21624  dgrcolem2  21625  plydiveu  21648  plyremlem  21654  elqaalem3  21671  iaa  21675  taylply2  21717  ulmdvlem1  21749  iblulm  21756  jensenlem2  22265  amgmlem  22267  ftalem7  22300  basellem8  22309  basellem9  22310  dchrmulid2  22475  dchrinvcl  22476  dchrfi  22478  lgseisenlem3  22574  lgseisenlem4  22575  chtppilimlem2  22607  chebbnd2  22610  chto1lb  22611  chpchtlim  22612  chpo1ub  22613  vmadivsum  22615  rpvmasumlem  22620  mudivsum  22663  selberglem1  22678  selberglem2  22679  selberg2lem  22683  selberg2  22684  pntrsumo1  22698  selbergr  22701  ofoprabco  25805  pl1cn  26238  esumadd  26360  ofccat  26788  ofs1  26790  itg2addnclem  28284  itg2addnclem3  28286  ibladdnclem  28289  itgaddnclem1  28291  iblabsnclem  28296  iblabsnc  28297  iblmulc2nc  28298  itgmulc2nclem1  28299  itgmulc2nclem2  28300  itgmulc2nc  28301  itgabsnc  28302  ftc1anclem3  28310  ftc1anclem4  28311  ftc1anclem5  28312  ftc1anclem6  28313  ftc1anclem7  28314  ftc1anclem8  28315  mendlmod  29392  mendassa  29393  expgrowthi  29449  expgrowth  29451  offvalfv  30574
  Copyright terms: Public domain W3C validator