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

Theorem suppssr 5797
Description: A function is zero outside its support. (Contributed by Mario Carneiro, 19-Dec-2014.)
Hypotheses
Ref Expression
suppssr.f  |-  ( ph  ->  F : A --> B )
suppssr.n  |-  ( ph  ->  ( `' F "
( _V  \  { Z } ) )  C_  W )
Assertion
Ref Expression
suppssr  |-  ( (
ph  /\  X  e.  ( A  \  W ) )  ->  ( F `  X )  =  Z )

Proof of Theorem suppssr
StepHypRef Expression
1 eldif 3267 . 2  |-  ( X  e.  ( A  \  W )  <->  ( X  e.  A  /\  -.  X  e.  W ) )
2 fvex 5676 . . . . . 6  |-  ( F `
 X )  e. 
_V
3 eldifsn 3864 . . . . . 6  |-  ( ( F `  X )  e.  ( _V  \  { Z } )  <->  ( ( F `  X )  e.  _V  /\  ( F `
 X )  =/= 
Z ) )
42, 3mpbiran 885 . . . . 5  |-  ( ( F `  X )  e.  ( _V  \  { Z } )  <->  ( F `  X )  =/=  Z
)
5 suppssr.f . . . . . . . 8  |-  ( ph  ->  F : A --> B )
6 ffn 5525 . . . . . . . 8  |-  ( F : A --> B  ->  F  Fn  A )
7 elpreima 5783 . . . . . . . 8  |-  ( F  Fn  A  ->  ( X  e.  ( `' F " ( _V  \  { Z } ) )  <-> 
( X  e.  A  /\  ( F `  X
)  e.  ( _V 
\  { Z }
) ) ) )
85, 6, 73syl 19 . . . . . . 7  |-  ( ph  ->  ( X  e.  ( `' F " ( _V 
\  { Z }
) )  <->  ( X  e.  A  /\  ( F `  X )  e.  ( _V  \  { Z } ) ) ) )
9 suppssr.n . . . . . . . 8  |-  ( ph  ->  ( `' F "
( _V  \  { Z } ) )  C_  W )
109sseld 3284 . . . . . . 7  |-  ( ph  ->  ( X  e.  ( `' F " ( _V 
\  { Z }
) )  ->  X  e.  W ) )
118, 10sylbird 227 . . . . . 6  |-  ( ph  ->  ( ( X  e.  A  /\  ( F `
 X )  e.  ( _V  \  { Z } ) )  ->  X  e.  W )
)
1211expdimp 427 . . . . 5  |-  ( (
ph  /\  X  e.  A )  ->  (
( F `  X
)  e.  ( _V 
\  { Z }
)  ->  X  e.  W ) )
134, 12syl5bir 210 . . . 4  |-  ( (
ph  /\  X  e.  A )  ->  (
( F `  X
)  =/=  Z  ->  X  e.  W )
)
1413necon1bd 2612 . . 3  |-  ( (
ph  /\  X  e.  A )  ->  ( -.  X  e.  W  ->  ( F `  X
)  =  Z ) )
1514impr 603 . 2  |-  ( (
ph  /\  ( X  e.  A  /\  -.  X  e.  W ) )  -> 
( F `  X
)  =  Z )
161, 15sylan2b 462 1  |-  ( (
ph  /\  X  e.  ( A  \  W ) )  ->  ( F `  X )  =  Z )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    /\ wa 359    = wceq 1649    e. wcel 1717    =/= wne 2544   _Vcvv 2893    \ cdif 3254    C_ wss 3257   {csn 3751   `'ccnv 4811   "cima 4815    Fn wfn 5383   -->wf 5384   ` cfv 5388
This theorem is referenced by:  cantnfp1lem1  7561  cantnfp1lem3  7563  cantnflem1d  7571  cantnflem1  7572  cnfcom2lem  7585  gsumval3  15435  gsumcllem  15437  gsumzaddlem  15447  gsumzsplit  15450  gsumzmhm  15454  gsumzinv  15461  gsumsub  15463  gsumpt  15466  gsum2d  15467  dprdfinv  15498  dprdfadd  15499  dmdprdsplitlem  15516  dpjidcl  15537  gsumdixp  15636  psrbaglesupp  16354  psrbagaddcl  16356  psrbaglefi  16358  mplsubglem  16419  mpllsslem  16420  mplsubrglem  16423  mplmonmul  16448  mplcoe1  16449  mplcoe2  16451  mplbas2  16452  evlslem4  16485  evlslem2  16489  deg1mul3le  19900  lcomfsup  26432  uvcresum  26905  frlmsslsp  26911  frlmup1  26913
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2362  ax-sep 4265  ax-nul 4273  ax-pr 4338
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2236  df-mo 2237  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2506  df-ne 2546  df-ral 2648  df-rex 2649  df-rab 2652  df-v 2895  df-sbc 3099  df-dif 3260  df-un 3262  df-in 3264  df-ss 3271  df-nul 3566  df-if 3677  df-sn 3757  df-pr 3758  df-op 3760  df-uni 3952  df-br 4148  df-opab 4202  df-id 4433  df-xp 4818  df-rel 4819  df-cnv 4820  df-co 4821  df-dm 4822  df-rn 4823  df-res 4824  df-ima 4825  df-iota 5352  df-fun 5390  df-fn 5391  df-f 5392  df-fv 5396
  Copyright terms: Public domain W3C validator