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

Theorem suppssr 7661
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 3838 . 2 (𝑋 ∈ (𝐴𝑊) ↔ (𝑋𝐴 ∧ ¬ 𝑋𝑊))
2 fvex 6510 . . . . . 6 (𝐹𝑋) ∈ V
3 eldifsn 4591 . . . . . 6 ((𝐹𝑋) ∈ (V ∖ {𝑍}) ↔ ((𝐹𝑋) ∈ V ∧ (𝐹𝑋) ≠ 𝑍))
42, 3mpbiran 696 . . . . 5 ((𝐹𝑋) ∈ (V ∖ {𝑍}) ↔ (𝐹𝑋) ≠ 𝑍)
5 suppssr.f . . . . . . . . . 10 (𝜑𝐹:𝐴𝐵)
65ffnd 6343 . . . . . . . . 9 (𝜑𝐹 Fn 𝐴)
7 suppssr.a . . . . . . . . 9 (𝜑𝐴𝑉)
8 suppssr.z . . . . . . . . 9 (𝜑𝑍𝑈)
9 elsuppfn 7638 . . . . . . . . 9 ((𝐹 Fn 𝐴𝐴𝑉𝑍𝑈) → (𝑋 ∈ (𝐹 supp 𝑍) ↔ (𝑋𝐴 ∧ (𝐹𝑋) ≠ 𝑍)))
106, 7, 8, 9syl3anc 1351 . . . . . . . 8 (𝜑 → (𝑋 ∈ (𝐹 supp 𝑍) ↔ (𝑋𝐴 ∧ (𝐹𝑋) ≠ 𝑍)))
11 ibar 521 . . . . . . . . . . 11 ((𝐹𝑋) ∈ V → ((𝐹𝑋) ≠ 𝑍 ↔ ((𝐹𝑋) ∈ V ∧ (𝐹𝑋) ≠ 𝑍)))
122, 11mp1i 13 . . . . . . . . . 10 ((𝜑𝑋𝐴) → ((𝐹𝑋) ≠ 𝑍 ↔ ((𝐹𝑋) ∈ V ∧ (𝐹𝑋) ≠ 𝑍)))
1312, 3syl6bbr 281 . . . . . . . . 9 ((𝜑𝑋𝐴) → ((𝐹𝑋) ≠ 𝑍 ↔ (𝐹𝑋) ∈ (V ∖ {𝑍})))
1413pm5.32da 571 . . . . . . . 8 (𝜑 → ((𝑋𝐴 ∧ (𝐹𝑋) ≠ 𝑍) ↔ (𝑋𝐴 ∧ (𝐹𝑋) ∈ (V ∖ {𝑍}))))
1510, 14bitrd 271 . . . . . . 7 (𝜑 → (𝑋 ∈ (𝐹 supp 𝑍) ↔ (𝑋𝐴 ∧ (𝐹𝑋) ∈ (V ∖ {𝑍}))))
16 suppssr.n . . . . . . . 8 (𝜑 → (𝐹 supp 𝑍) ⊆ 𝑊)
1716sseld 3856 . . . . . . 7 (𝜑 → (𝑋 ∈ (𝐹 supp 𝑍) → 𝑋𝑊))
1815, 17sylbird 252 . . . . . 6 (𝜑 → ((𝑋𝐴 ∧ (𝐹𝑋) ∈ (V ∖ {𝑍})) → 𝑋𝑊))
1918expdimp 445 . . . . 5 ((𝜑𝑋𝐴) → ((𝐹𝑋) ∈ (V ∖ {𝑍}) → 𝑋𝑊))
204, 19syl5bir 235 . . . 4 ((𝜑𝑋𝐴) → ((𝐹𝑋) ≠ 𝑍𝑋𝑊))
2120necon1bd 2982 . . 3 ((𝜑𝑋𝐴) → (¬ 𝑋𝑊 → (𝐹𝑋) = 𝑍))
2221impr 447 . 2 ((𝜑 ∧ (𝑋𝐴 ∧ ¬ 𝑋𝑊)) → (𝐹𝑋) = 𝑍)
231, 22sylan2b 584 1 ((𝜑𝑋 ∈ (𝐴𝑊)) → (𝐹𝑋) = 𝑍)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 387   = wceq 1507  wcel 2048  wne 2964  Vcvv 3412  cdif 3825  wss 3828  {csn 4439   Fn wfn 6181  wf 6182  cfv 6186  (class class class)co 6974   supp csupp 7630
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-13 2299  ax-ext 2747  ax-rep 5047  ax-sep 5058  ax-nul 5065  ax-pr 5184  ax-un 7277
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-mo 2544  df-eu 2580  df-clab 2756  df-cleq 2768  df-clel 2843  df-nfc 2915  df-ne 2965  df-ral 3090  df-rex 3091  df-reu 3092  df-rab 3094  df-v 3414  df-sbc 3681  df-csb 3786  df-dif 3831  df-un 3833  df-in 3835  df-ss 3842  df-nul 4178  df-if 4349  df-sn 4440  df-pr 4442  df-op 4446  df-uni 4711  df-iun 4792  df-br 4928  df-opab 4990  df-mpt 5007  df-id 5309  df-xp 5410  df-rel 5411  df-cnv 5412  df-co 5413  df-dm 5414  df-rn 5415  df-res 5416  df-ima 5417  df-iota 6150  df-fun 6188  df-fn 6189  df-f 6190  df-f1 6191  df-fo 6192  df-f1o 6193  df-fv 6194  df-ov 6977  df-oprab 6978  df-mpo 6979  df-supp 7631
This theorem is referenced by:  fsuppmptif  8654  fsuppco2  8657  fsuppcor  8658  cantnfp1lem1  8931  cantnfp1lem3  8933  cantnflem1  8942  cnfcom2lem  8954  gsumval3  18775  gsumcllem  18776  gsumzaddlem  18788  gsumzmhm  18804  gsumpt  18829  gsum2dlem1  18837  gsum2dlem2  18838  gsum2d  18839  dprdfinv  18885  dprdfadd  18886  dmdprdsplitlem  18903  dpjidcl  18924  gsumdixp  19076  lcomfsupp  19390  psrbaglesupp  19856  psrbagaddcl  19858  psrbaglefi  19860  mplsubglem  19922  mpllsslem  19923  mplsubrglem  19927  mplmonmul  19952  mplcoe1  19953  mplcoe5  19956  mplbas2  19958  evlslem4  19995  evlslem2  19999  uvcresum  20633  frlmsslsp  20636  rrxcph  23692  rrxmval  23705  rrxmetlem  23707  rrxmet  23708  rrxdstprj1  23709  deg1mul3le  24407  suppovss  30181  fedgmullem1  30645  eulerpartlemb  31262
  Copyright terms: Public domain W3C validator