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

Theorem suppssr 7564
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 3786 . 2 (𝑋 ∈ (𝐴𝑊) ↔ (𝑋𝐴 ∧ ¬ 𝑋𝑊))
2 fvex 6424 . . . . . 6 (𝐹𝑋) ∈ V
3 eldifsn 4515 . . . . . 6 ((𝐹𝑋) ∈ (V ∖ {𝑍}) ↔ ((𝐹𝑋) ∈ V ∧ (𝐹𝑋) ≠ 𝑍))
42, 3mpbiran 691 . . . . 5 ((𝐹𝑋) ∈ (V ∖ {𝑍}) ↔ (𝐹𝑋) ≠ 𝑍)
5 suppssr.f . . . . . . . . . 10 (𝜑𝐹:𝐴𝐵)
65ffnd 6260 . . . . . . . . 9 (𝜑𝐹 Fn 𝐴)
7 suppssr.a . . . . . . . . 9 (𝜑𝐴𝑉)
8 suppssr.z . . . . . . . . 9 (𝜑𝑍𝑈)
9 elsuppfn 7540 . . . . . . . . 9 ((𝐹 Fn 𝐴𝐴𝑉𝑍𝑈) → (𝑋 ∈ (𝐹 supp 𝑍) ↔ (𝑋𝐴 ∧ (𝐹𝑋) ≠ 𝑍)))
106, 7, 8, 9syl3anc 1483 . . . . . . . 8 (𝜑 → (𝑋 ∈ (𝐹 supp 𝑍) ↔ (𝑋𝐴 ∧ (𝐹𝑋) ≠ 𝑍)))
11 ibar 520 . . . . . . . . . . 11 ((𝐹𝑋) ∈ V → ((𝐹𝑋) ≠ 𝑍 ↔ ((𝐹𝑋) ∈ V ∧ (𝐹𝑋) ≠ 𝑍)))
122, 11mp1i 13 . . . . . . . . . 10 ((𝜑𝑋𝐴) → ((𝐹𝑋) ≠ 𝑍 ↔ ((𝐹𝑋) ∈ V ∧ (𝐹𝑋) ≠ 𝑍)))
1312, 3syl6bbr 280 . . . . . . . . 9 ((𝜑𝑋𝐴) → ((𝐹𝑋) ≠ 𝑍 ↔ (𝐹𝑋) ∈ (V ∖ {𝑍})))
1413pm5.32da 570 . . . . . . . 8 (𝜑 → ((𝑋𝐴 ∧ (𝐹𝑋) ≠ 𝑍) ↔ (𝑋𝐴 ∧ (𝐹𝑋) ∈ (V ∖ {𝑍}))))
1510, 14bitrd 270 . . . . . . 7 (𝜑 → (𝑋 ∈ (𝐹 supp 𝑍) ↔ (𝑋𝐴 ∧ (𝐹𝑋) ∈ (V ∖ {𝑍}))))
16 suppssr.n . . . . . . . 8 (𝜑 → (𝐹 supp 𝑍) ⊆ 𝑊)
1716sseld 3804 . . . . . . 7 (𝜑 → (𝑋 ∈ (𝐹 supp 𝑍) → 𝑋𝑊))
1815, 17sylbird 251 . . . . . 6 (𝜑 → ((𝑋𝐴 ∧ (𝐹𝑋) ∈ (V ∖ {𝑍})) → 𝑋𝑊))
1918expdimp 442 . . . . 5 ((𝜑𝑋𝐴) → ((𝐹𝑋) ∈ (V ∖ {𝑍}) → 𝑋𝑊))
204, 19syl5bir 234 . . . 4 ((𝜑𝑋𝐴) → ((𝐹𝑋) ≠ 𝑍𝑋𝑊))
2120necon1bd 3003 . . 3 ((𝜑𝑋𝐴) → (¬ 𝑋𝑊 → (𝐹𝑋) = 𝑍))
2221impr 444 . 2 ((𝜑 ∧ (𝑋𝐴 ∧ ¬ 𝑋𝑊)) → (𝐹𝑋) = 𝑍)
231, 22sylan2b 583 1 ((𝜑𝑋 ∈ (𝐴𝑊)) → (𝐹𝑋) = 𝑍)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384   = wceq 1637  wcel 2157  wne 2985  Vcvv 3398  cdif 3773  wss 3776  {csn 4377   Fn wfn 6099  wf 6100  cfv 6104  (class class class)co 6877   supp csupp 7532
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791  ax-rep 4971  ax-sep 4982  ax-nul 4990  ax-pr 5103  ax-un 7182
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2638  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-ne 2986  df-ral 3108  df-rex 3109  df-reu 3110  df-rab 3112  df-v 3400  df-sbc 3641  df-csb 3736  df-dif 3779  df-un 3781  df-in 3783  df-ss 3790  df-nul 4124  df-if 4287  df-sn 4378  df-pr 4380  df-op 4384  df-uni 4638  df-iun 4721  df-br 4852  df-opab 4914  df-mpt 4931  df-id 5226  df-xp 5324  df-rel 5325  df-cnv 5326  df-co 5327  df-dm 5328  df-rn 5329  df-res 5330  df-ima 5331  df-iota 6067  df-fun 6106  df-fn 6107  df-f 6108  df-f1 6109  df-fo 6110  df-f1o 6111  df-fv 6112  df-ov 6880  df-oprab 6881  df-mpt2 6882  df-supp 7533
This theorem is referenced by:  fsuppmptif  8547  fsuppco2  8550  fsuppcor  8551  cantnfp1lem1  8825  cantnfp1lem3  8827  cantnflem1  8836  cnfcom2lem  8848  gsumval3  18512  gsumcllem  18513  gsumzaddlem  18525  gsumzmhm  18541  gsumpt  18565  gsum2dlem1  18573  gsum2dlem2  18574  gsum2d  18575  dprdfinv  18623  dprdfadd  18624  dmdprdsplitlem  18641  dpjidcl  18662  gsumdixp  18814  lcomfsupp  19110  psrbaglesupp  19580  psrbagaddcl  19582  psrbaglefi  19584  mplsubglem  19646  mpllsslem  19647  mplsubrglem  19651  mplmonmul  19676  mplcoe1  19677  mplcoe5  19680  mplbas2  19682  evlslem4  19719  evlslem2  19723  uvcresum  20346  frlmsslsp  20349  rrxcph  23398  rrxmval  23406  rrxmetlem  23408  rrxmet  23409  rrxdstprj1  23410  deg1mul3le  24096  eulerpartlemb  30761
  Copyright terms: Public domain W3C validator