![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > suppssr | Structured version Visualization version GIF version |
Description: A function is zero outside its support. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by AV, 28-May-2019.) |
Ref | Expression |
---|---|
suppssr.f | ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
suppssr.n | ⊢ (𝜑 → (𝐹 supp 𝑍) ⊆ 𝑊) |
suppssr.a | ⊢ (𝜑 → 𝐴 ∈ 𝑉) |
suppssr.z | ⊢ (𝜑 → 𝑍 ∈ 𝑈) |
Ref | Expression |
---|---|
suppssr | ⊢ ((𝜑 ∧ 𝑋 ∈ (𝐴 ∖ 𝑊)) → (𝐹‘𝑋) = 𝑍) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eldif 3838 | . 2 ⊢ (𝑋 ∈ (𝐴 ∖ 𝑊) ↔ (𝑋 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝑊)) | |
2 | fvex 6510 | . . . . . 6 ⊢ (𝐹‘𝑋) ∈ V | |
3 | eldifsn 4591 | . . . . . 6 ⊢ ((𝐹‘𝑋) ∈ (V ∖ {𝑍}) ↔ ((𝐹‘𝑋) ∈ V ∧ (𝐹‘𝑋) ≠ 𝑍)) | |
4 | 2, 3 | mpbiran 696 | . . . . 5 ⊢ ((𝐹‘𝑋) ∈ (V ∖ {𝑍}) ↔ (𝐹‘𝑋) ≠ 𝑍) |
5 | suppssr.f | . . . . . . . . . 10 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) | |
6 | 5 | ffnd 6343 | . . . . . . . . 9 ⊢ (𝜑 → 𝐹 Fn 𝐴) |
7 | suppssr.a | . . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ 𝑉) | |
8 | suppssr.z | . . . . . . . . 9 ⊢ (𝜑 → 𝑍 ∈ 𝑈) | |
9 | elsuppfn 7638 | . . . . . . . . 9 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉 ∧ 𝑍 ∈ 𝑈) → (𝑋 ∈ (𝐹 supp 𝑍) ↔ (𝑋 ∈ 𝐴 ∧ (𝐹‘𝑋) ≠ 𝑍))) | |
10 | 6, 7, 8, 9 | syl3anc 1351 | . . . . . . . 8 ⊢ (𝜑 → (𝑋 ∈ (𝐹 supp 𝑍) ↔ (𝑋 ∈ 𝐴 ∧ (𝐹‘𝑋) ≠ 𝑍))) |
11 | ibar 521 | . . . . . . . . . . 11 ⊢ ((𝐹‘𝑋) ∈ V → ((𝐹‘𝑋) ≠ 𝑍 ↔ ((𝐹‘𝑋) ∈ V ∧ (𝐹‘𝑋) ≠ 𝑍))) | |
12 | 2, 11 | mp1i 13 | . . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → ((𝐹‘𝑋) ≠ 𝑍 ↔ ((𝐹‘𝑋) ∈ V ∧ (𝐹‘𝑋) ≠ 𝑍))) |
13 | 12, 3 | syl6bbr 281 | . . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → ((𝐹‘𝑋) ≠ 𝑍 ↔ (𝐹‘𝑋) ∈ (V ∖ {𝑍}))) |
14 | 13 | pm5.32da 571 | . . . . . . . 8 ⊢ (𝜑 → ((𝑋 ∈ 𝐴 ∧ (𝐹‘𝑋) ≠ 𝑍) ↔ (𝑋 ∈ 𝐴 ∧ (𝐹‘𝑋) ∈ (V ∖ {𝑍})))) |
15 | 10, 14 | bitrd 271 | . . . . . . 7 ⊢ (𝜑 → (𝑋 ∈ (𝐹 supp 𝑍) ↔ (𝑋 ∈ 𝐴 ∧ (𝐹‘𝑋) ∈ (V ∖ {𝑍})))) |
16 | suppssr.n | . . . . . . . 8 ⊢ (𝜑 → (𝐹 supp 𝑍) ⊆ 𝑊) | |
17 | 16 | sseld 3856 | . . . . . . 7 ⊢ (𝜑 → (𝑋 ∈ (𝐹 supp 𝑍) → 𝑋 ∈ 𝑊)) |
18 | 15, 17 | sylbird 252 | . . . . . 6 ⊢ (𝜑 → ((𝑋 ∈ 𝐴 ∧ (𝐹‘𝑋) ∈ (V ∖ {𝑍})) → 𝑋 ∈ 𝑊)) |
19 | 18 | expdimp 445 | . . . . 5 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → ((𝐹‘𝑋) ∈ (V ∖ {𝑍}) → 𝑋 ∈ 𝑊)) |
20 | 4, 19 | syl5bir 235 | . . . 4 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → ((𝐹‘𝑋) ≠ 𝑍 → 𝑋 ∈ 𝑊)) |
21 | 20 | necon1bd 2982 | . . 3 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → (¬ 𝑋 ∈ 𝑊 → (𝐹‘𝑋) = 𝑍)) |
22 | 21 | impr 447 | . 2 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝑊)) → (𝐹‘𝑋) = 𝑍) |
23 | 1, 22 | sylan2b 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 |