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

Theorem suppssr 8183
Description: A function is zero outside its support. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by AV, 28-May-2019.)
Hypotheses
Ref Expression
suppssr.f (𝜑𝐹:𝐴𝐵)
suppssr.n (𝜑 → (𝐹 supp 𝑍) ⊆ 𝑊)
suppssr.a (𝜑𝐴𝑉)
suppssr.z (𝜑𝑍𝑈)
Assertion
Ref Expression
suppssr ((𝜑𝑋 ∈ (𝐴𝑊)) → (𝐹𝑋) = 𝑍)

Proof of Theorem suppssr
StepHypRef Expression
1 eldif 3957 . 2 (𝑋 ∈ (𝐴𝑊) ↔ (𝑋𝐴 ∧ ¬ 𝑋𝑊))
2 fvex 6903 . . . . . 6 (𝐹𝑋) ∈ V
3 eldifsn 4789 . . . . . 6 ((𝐹𝑋) ∈ (V ∖ {𝑍}) ↔ ((𝐹𝑋) ∈ V ∧ (𝐹𝑋) ≠ 𝑍))
42, 3mpbiran 705 . . . . 5 ((𝐹𝑋) ∈ (V ∖ {𝑍}) ↔ (𝐹𝑋) ≠ 𝑍)
5 suppssr.f . . . . . . . . . 10 (𝜑𝐹:𝐴𝐵)
65ffnd 6717 . . . . . . . . 9 (𝜑𝐹 Fn 𝐴)
7 suppssr.a . . . . . . . . 9 (𝜑𝐴𝑉)
8 suppssr.z . . . . . . . . 9 (𝜑𝑍𝑈)
9 elsuppfn 8158 . . . . . . . . 9 ((𝐹 Fn 𝐴𝐴𝑉𝑍𝑈) → (𝑋 ∈ (𝐹 supp 𝑍) ↔ (𝑋𝐴 ∧ (𝐹𝑋) ≠ 𝑍)))
106, 7, 8, 9syl3anc 1369 . . . . . . . 8 (𝜑 → (𝑋 ∈ (𝐹 supp 𝑍) ↔ (𝑋𝐴 ∧ (𝐹𝑋) ≠ 𝑍)))
11 ibar 527 . . . . . . . . . . 11 ((𝐹𝑋) ∈ V → ((𝐹𝑋) ≠ 𝑍 ↔ ((𝐹𝑋) ∈ V ∧ (𝐹𝑋) ≠ 𝑍)))
122, 11mp1i 13 . . . . . . . . . 10 ((𝜑𝑋𝐴) → ((𝐹𝑋) ≠ 𝑍 ↔ ((𝐹𝑋) ∈ V ∧ (𝐹𝑋) ≠ 𝑍)))
1312, 3bitr4di 288 . . . . . . . . 9 ((𝜑𝑋𝐴) → ((𝐹𝑋) ≠ 𝑍 ↔ (𝐹𝑋) ∈ (V ∖ {𝑍})))
1413pm5.32da 577 . . . . . . . 8 (𝜑 → ((𝑋𝐴 ∧ (𝐹𝑋) ≠ 𝑍) ↔ (𝑋𝐴 ∧ (𝐹𝑋) ∈ (V ∖ {𝑍}))))
1510, 14bitrd 278 . . . . . . 7 (𝜑 → (𝑋 ∈ (𝐹 supp 𝑍) ↔ (𝑋𝐴 ∧ (𝐹𝑋) ∈ (V ∖ {𝑍}))))
16 suppssr.n . . . . . . . 8 (𝜑 → (𝐹 supp 𝑍) ⊆ 𝑊)
1716sseld 3980 . . . . . . 7 (𝜑 → (𝑋 ∈ (𝐹 supp 𝑍) → 𝑋𝑊))
1815, 17sylbird 259 . . . . . 6 (𝜑 → ((𝑋𝐴 ∧ (𝐹𝑋) ∈ (V ∖ {𝑍})) → 𝑋𝑊))
1918expdimp 451 . . . . 5 ((𝜑𝑋𝐴) → ((𝐹𝑋) ∈ (V ∖ {𝑍}) → 𝑋𝑊))
204, 19biimtrrid 242 . . . 4 ((𝜑𝑋𝐴) → ((𝐹𝑋) ≠ 𝑍𝑋𝑊))
2120necon1bd 2956 . . 3 ((𝜑𝑋𝐴) → (¬ 𝑋𝑊 → (𝐹𝑋) = 𝑍))
2221impr 453 . 2 ((𝜑 ∧ (𝑋𝐴 ∧ ¬ 𝑋𝑊)) → (𝐹𝑋) = 𝑍)
231, 22sylan2b 592 1 ((𝜑𝑋 ∈ (𝐴𝑊)) → (𝐹𝑋) = 𝑍)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 394   = wceq 1539  wcel 2104  wne 2938  Vcvv 3472  cdif 3944  wss 3947  {csn 4627   Fn wfn 6537  wf 6538  cfv 6542  (class class class)co 7411   supp csupp 8148
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pr 5426  ax-un 7727
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-ov 7414  df-oprab 7415  df-mpo 7416  df-supp 8149
This theorem is referenced by:  fsuppmptif  9396  fsuppco2  9400  fsuppcor  9401  cantnfp1lem1  9675  cantnfp1lem3  9677  cantnflem1  9686  cnfcom2lem  9698  gsumval3  19816  gsumcllem  19817  gsumzaddlem  19830  gsumzmhm  19846  gsumpt  19871  gsum2dlem1  19879  gsum2dlem2  19880  gsum2d  19881  gsumxp2  19889  dprdfinv  19930  dprdfadd  19931  dmdprdsplitlem  19948  dpjidcl  19969  gsumdixp  20207  lcomfsupp  20656  uvcresum  21567  frlmsslsp  21570  psrbaglesuppOLD  21697  psrbagaddclOLD  21701  psrbaglefiOLD  21705  mplsubglem  21777  mpllsslem  21778  mplsubrglem  21782  mplmonmul  21810  mplcoe1  21811  mplcoe5  21814  mplbas2  21816  evlslem4  21856  evlslem2  21861  mhpmulcl  21911  mhpvscacl  21916  rrxcph  25140  rrxmval  25153  rrxmetlem  25155  rrxmet  25156  rrxdstprj1  25157  deg1mul3le  25869  suppovss  32173  elrspunidl  32820  fedgmullem1  33002  eulerpartlemb  33665  evlsvvvallem  41435  evlsvvval  41437  evlselv  41461  fsuppssindlem1  41465  evlsmhpvvval  41469
  Copyright terms: Public domain W3C validator