suppssr - Metamath Proof Explorer

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

Theorem suppssr 8125

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**
Step	Hyp	Ref	Expression
1		eldif 3912	. 2 ⊢ (𝑋 ∈ (𝐴 ∖ 𝑊) ↔ (𝑋 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝑊))
2		fvex 6835	. . . . . 6 ⊢ (𝐹‘𝑋) ∈ V
3		eldifsn 4738	. . . . . 6 ⊢ ((𝐹‘𝑋) ∈ (V ∖ {𝑍}) ↔ ((𝐹‘𝑋) ∈ V ∧ (𝐹‘𝑋) ≠ 𝑍))
4	2, 3	mpbiran 709	. . . . 5 ⊢ ((𝐹‘𝑋) ∈ (V ∖ {𝑍}) ↔ (𝐹‘𝑋) ≠ 𝑍)
5		suppssr.f	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
6	5	ffnd 6652	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 Fn 𝐴)
7		suppssr.a	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
8		suppssr.z	. . . . . . . . 9 ⊢ (𝜑 → 𝑍 ∈ 𝑈)
9		elsuppfn 8100	. . . . . . . . 9 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉 ∧ 𝑍 ∈ 𝑈) → (𝑋 ∈ (𝐹 supp 𝑍) ↔ (𝑋 ∈ 𝐴 ∧ (𝐹‘𝑋) ≠ 𝑍)))
10	6, 7, 8, 9	syl3anc 1373	. . . . . . . 8 ⊢ (𝜑 → (𝑋 ∈ (𝐹 supp 𝑍) ↔ (𝑋 ∈ 𝐴 ∧ (𝐹‘𝑋) ≠ 𝑍)))
11		ibar 528	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑋) ∈ V → ((𝐹‘𝑋) ≠ 𝑍 ↔ ((𝐹‘𝑋) ∈ V ∧ (𝐹‘𝑋) ≠ 𝑍)))
12	2, 11	mp1i 13	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → ((𝐹‘𝑋) ≠ 𝑍 ↔ ((𝐹‘𝑋) ∈ V ∧ (𝐹‘𝑋) ≠ 𝑍)))
13	12, 3	bitr4di 289	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → ((𝐹‘𝑋) ≠ 𝑍 ↔ (𝐹‘𝑋) ∈ (V ∖ {𝑍})))
14	13	pm5.32da 579	. . . . . . . 8 ⊢ (𝜑 → ((𝑋 ∈ 𝐴 ∧ (𝐹‘𝑋) ≠ 𝑍) ↔ (𝑋 ∈ 𝐴 ∧ (𝐹‘𝑋) ∈ (V ∖ {𝑍}))))
15	10, 14	bitrd 279	. . . . . . 7 ⊢ (𝜑 → (𝑋 ∈ (𝐹 supp 𝑍) ↔ (𝑋 ∈ 𝐴 ∧ (𝐹‘𝑋) ∈ (V ∖ {𝑍}))))
16		suppssr.n	. . . . . . . 8 ⊢ (𝜑 → (𝐹 supp 𝑍) ⊆ 𝑊)
17	16	sseld 3933	. . . . . . 7 ⊢ (𝜑 → (𝑋 ∈ (𝐹 supp 𝑍) → 𝑋 ∈ 𝑊))
18	15, 17	sylbird 260	. . . . . 6 ⊢ (𝜑 → ((𝑋 ∈ 𝐴 ∧ (𝐹‘𝑋) ∈ (V ∖ {𝑍})) → 𝑋 ∈ 𝑊))
19	18	expdimp 452	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → ((𝐹‘𝑋) ∈ (V ∖ {𝑍}) → 𝑋 ∈ 𝑊))
20	4, 19	biimtrrid 243	. . . 4 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → ((𝐹‘𝑋) ≠ 𝑍 → 𝑋 ∈ 𝑊))
21	20	necon1bd 2946	. . 3 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → (¬ 𝑋 ∈ 𝑊 → (𝐹‘𝑋) = 𝑍))
22	21	impr 454	. 2 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝑊)) → (𝐹‘𝑋) = 𝑍)
23	1, 22	sylan2b 594	1 ⊢ ((𝜑 ∧ 𝑋 ∈ (𝐴 ∖ 𝑊)) → (𝐹‘𝑋) = 𝑍)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1541 ∈ wcel 2111 ≠ wne 2928 Vcvv 3436 ∖ cdif 3899 ⊆ wss 3902 {csn 4576 Fn wfn 6476 ⟶wf 6477 ‘cfv 6481 (class class class)co 7346 supp csupp 8090

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-rep 5217 ax-sep 5234 ax-nul 5244 ax-pr 5370 ax-un 7668

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-ral 3048 df-rex 3057 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3742 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-nul 4284 df-if 4476 df-pw 4552 df-sn 4577 df-pr 4579 df-op 4583 df-uni 4860 df-iun 4943 df-br 5092 df-opab 5154 df-mpt 5173 df-id 5511 df-xp 5622 df-rel 5623 df-cnv 5624 df-co 5625 df-dm 5626 df-rn 5627 df-res 5628 df-ima 5629 df-iota 6437 df-fun 6483 df-fn 6484 df-f 6485 df-f1 6486 df-fo 6487 df-f1o 6488 df-fv 6489 df-ov 7349 df-oprab 7350 df-mpo 7351 df-supp 8091

This theorem is referenced by: fsuppmptif 9283 fsuppco2 9287 fsuppcor 9288 cantnfp1lem1 9568 cantnfp1lem3 9570 cantnflem1 9579 cnfcom2lem 9591 gsumval3 19817 gsumcllem 19818 gsumzaddlem 19831 gsumzmhm 19847 gsumpt 19872 gsum2dlem1 19880 gsum2dlem2 19881 gsum2d 19882 gsumxp2 19890 dprdfinv 19931 dprdfadd 19932 dmdprdsplitlem 19949 dpjidcl 19970 gsumdixp 20235 lcomfsupp 20833 uvcresum 21728 frlmsslsp 21731 mplsubglem 21934 mpllsslem 21935 mplsubrglem 21939 mplmonmul 21969 mplcoe1 21970 mplcoe5 21973 mplbas2 21975 evlslem4 22009 evlslem2 22012 rrxcph 25317 rrxmval 25330 rrxmetlem 25332 rrxmet 25333 rrxdstprj1 25334 deg1mul3le 26047 suppovss 32657 elrspunidl 33388 fedgmullem1 33637 eulerpartlemb 34376 evlsvvvallem 42593 evlsvvval 42595 evlselv 42619 fsuppssindlem1 42623 evlsmhpvvval 42627

W3C validator