![]() |
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 3924 | . 2 ⊢ (𝑋 ∈ (𝐴 ∖ 𝑊) ↔ (𝑋 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝑊)) | |
2 | fvex 6859 | . . . . . 6 ⊢ (𝐹‘𝑋) ∈ V | |
3 | eldifsn 4751 | . . . . . 6 ⊢ ((𝐹‘𝑋) ∈ (V ∖ {𝑍}) ↔ ((𝐹‘𝑋) ∈ V ∧ (𝐹‘𝑋) ≠ 𝑍)) | |
4 | 2, 3 | mpbiran 708 | . . . . 5 ⊢ ((𝐹‘𝑋) ∈ (V ∖ {𝑍}) ↔ (𝐹‘𝑋) ≠ 𝑍) |
5 | suppssr.f | . . . . . . . . . 10 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) | |
6 | 5 | ffnd 6673 | . . . . . . . . 9 ⊢ (𝜑 → 𝐹 Fn 𝐴) |
7 | suppssr.a | . . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ 𝑉) | |
8 | suppssr.z | . . . . . . . . 9 ⊢ (𝜑 → 𝑍 ∈ 𝑈) | |
9 | elsuppfn 8106 | . . . . . . . . 9 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉 ∧ 𝑍 ∈ 𝑈) → (𝑋 ∈ (𝐹 supp 𝑍) ↔ (𝑋 ∈ 𝐴 ∧ (𝐹‘𝑋) ≠ 𝑍))) | |
10 | 6, 7, 8, 9 | syl3anc 1372 | . . . . . . . 8 ⊢ (𝜑 → (𝑋 ∈ (𝐹 supp 𝑍) ↔ (𝑋 ∈ 𝐴 ∧ (𝐹‘𝑋) ≠ 𝑍))) |
11 | ibar 530 | . . . . . . . . . . 11 ⊢ ((𝐹‘𝑋) ∈ V → ((𝐹‘𝑋) ≠ 𝑍 ↔ ((𝐹‘𝑋) ∈ V ∧ (𝐹‘𝑋) ≠ 𝑍))) | |
12 | 2, 11 | mp1i 13 | . . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → ((𝐹‘𝑋) ≠ 𝑍 ↔ ((𝐹‘𝑋) ∈ V ∧ (𝐹‘𝑋) ≠ 𝑍))) |
13 | 12, 3 | bitr4di 289 | . . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → ((𝐹‘𝑋) ≠ 𝑍 ↔ (𝐹‘𝑋) ∈ (V ∖ {𝑍}))) |
14 | 13 | pm5.32da 580 | . . . . . . . 8 ⊢ (𝜑 → ((𝑋 ∈ 𝐴 ∧ (𝐹‘𝑋) ≠ 𝑍) ↔ (𝑋 ∈ 𝐴 ∧ (𝐹‘𝑋) ∈ (V ∖ {𝑍})))) |
15 | 10, 14 | bitrd 279 | . . . . . . 7 ⊢ (𝜑 → (𝑋 ∈ (𝐹 supp 𝑍) ↔ (𝑋 ∈ 𝐴 ∧ (𝐹‘𝑋) ∈ (V ∖ {𝑍})))) |
16 | suppssr.n | . . . . . . . 8 ⊢ (𝜑 → (𝐹 supp 𝑍) ⊆ 𝑊) | |
17 | 16 | sseld 3947 | . . . . . . 7 ⊢ (𝜑 → (𝑋 ∈ (𝐹 supp 𝑍) → 𝑋 ∈ 𝑊)) |
18 | 15, 17 | sylbird 260 | . . . . . 6 ⊢ (𝜑 → ((𝑋 ∈ 𝐴 ∧ (𝐹‘𝑋) ∈ (V ∖ {𝑍})) → 𝑋 ∈ 𝑊)) |
19 | 18 | expdimp 454 | . . . . 5 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → ((𝐹‘𝑋) ∈ (V ∖ {𝑍}) → 𝑋 ∈ 𝑊)) |
20 | 4, 19 | biimtrrid 242 | . . . 4 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → ((𝐹‘𝑋) ≠ 𝑍 → 𝑋 ∈ 𝑊)) |
21 | 20 | necon1bd 2958 | . . 3 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → (¬ 𝑋 ∈ 𝑊 → (𝐹‘𝑋) = 𝑍)) |
22 | 21 | impr 456 | . 2 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝑊)) → (𝐹‘𝑋) = 𝑍) |
23 | 1, 22 | sylan2b 595 | 1 ⊢ ((𝜑 ∧ 𝑋 ∈ (𝐴 ∖ 𝑊)) → (𝐹‘𝑋) = 𝑍) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 397 = wceq 1542 ∈ wcel 2107 ≠ wne 2940 Vcvv 3447 ∖ cdif 3911 ⊆ wss 3914 {csn 4590 Fn wfn 6495 ⟶wf 6496 ‘cfv 6500 (class class class)co 7361 supp csupp 8096 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-rep 5246 ax-sep 5260 ax-nul 5267 ax-pr 5388 ax-un 7676 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2941 df-ral 3062 df-rex 3071 df-reu 3353 df-rab 3407 df-v 3449 df-sbc 3744 df-csb 3860 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-nul 4287 df-if 4491 df-sn 4591 df-pr 4593 df-op 4597 df-uni 4870 df-iun 4960 df-br 5110 df-opab 5172 df-mpt 5193 df-id 5535 df-xp 5643 df-rel 5644 df-cnv 5645 df-co 5646 df-dm 5647 df-rn 5648 df-res 5649 df-ima 5650 df-iota 6452 df-fun 6502 df-fn 6503 df-f 6504 df-f1 6505 df-fo 6506 df-f1o 6507 df-fv 6508 df-ov 7364 df-oprab 7365 df-mpo 7366 df-supp 8097 |
This theorem is referenced by: fsuppmptif 9343 fsuppco2 9347 fsuppcor 9348 cantnfp1lem1 9622 cantnfp1lem3 9624 cantnflem1 9633 cnfcom2lem 9645 gsumval3 19692 gsumcllem 19693 gsumzaddlem 19706 gsumzmhm 19722 gsumpt 19747 gsum2dlem1 19755 gsum2dlem2 19756 gsum2d 19757 gsumxp2 19765 dprdfinv 19806 dprdfadd 19807 dmdprdsplitlem 19824 dpjidcl 19845 gsumdixp 20041 lcomfsupp 20406 uvcresum 21222 frlmsslsp 21225 psrbaglesuppOLD 21350 psrbagaddclOLD 21354 psrbaglefiOLD 21358 mplsubglem 21428 mpllsslem 21429 mplsubrglem 21433 mplmonmul 21460 mplcoe1 21461 mplcoe5 21464 mplbas2 21466 evlslem4 21507 evlslem2 21512 mhpmulcl 21562 mhpvscacl 21567 rrxcph 24779 rrxmval 24792 rrxmetlem 24794 rrxmet 24795 rrxdstprj1 24796 deg1mul3le 25504 suppovss 31651 elrspunidl 32258 fedgmullem1 32388 eulerpartlemb 33032 evlsbagval 40795 fsuppssindlem1 40813 |
Copyright terms: Public domain | W3C validator |