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 8138

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 3900	. 2 ⊢ (𝑋 ∈ (𝐴 ∖ 𝑊) ↔ (𝑋 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝑊))
2		fvex 6847	. . . . . 6 ⊢ (𝐹‘𝑋) ∈ V
3		eldifsn 4730	. . . . . 6 ⊢ ((𝐹‘𝑋) ∈ (V ∖ {𝑍}) ↔ ((𝐹‘𝑋) ∈ V ∧ (𝐹‘𝑋) ≠ 𝑍))
4	2, 3	mpbiran 710	. . . . 5 ⊢ ((𝐹‘𝑋) ∈ (V ∖ {𝑍}) ↔ (𝐹‘𝑋) ≠ 𝑍)
5		suppssr.f	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
6	5	ffnd 6663	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 Fn 𝐴)
7		suppssr.a	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
8		suppssr.z	. . . . . . . . 9 ⊢ (𝜑 → 𝑍 ∈ 𝑈)
9		elsuppfn 8113	. . . . . . . . 9 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉 ∧ 𝑍 ∈ 𝑈) → (𝑋 ∈ (𝐹 supp 𝑍) ↔ (𝑋 ∈ 𝐴 ∧ (𝐹‘𝑋) ≠ 𝑍)))
10	6, 7, 8, 9	syl3anc 1374	. . . . . . . 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 3921	. . . . . . 7 ⊢ (𝜑 → (𝑋 ∈ (𝐹 supp 𝑍) → 𝑋 ∈ 𝑊))
18	15, 17	sylbird 260	. . . . . 6 ⊢ (𝜑 → ((𝑋 ∈ 𝐴 ∧ (𝐹‘𝑋) ∈ (V ∖ {𝑍})) → 𝑋 ∈ 𝑊))
19	18	expdimp 452	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → ((𝐹‘𝑋) ∈ (V ∖ {𝑍}) → 𝑋 ∈ 𝑊))
20	4, 19	biimtrrid 243	. . . 4 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → ((𝐹‘𝑋) ≠ 𝑍 → 𝑋 ∈ 𝑊))
21	20	necon1bd 2951	. . 3 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → (¬ 𝑋 ∈ 𝑊 → (𝐹‘𝑋) = 𝑍))
22	21	impr 454	. 2 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝑊)) → (𝐹‘𝑋) = 𝑍)
23	1, 22	sylan2b 595	1 ⊢ ((𝜑 ∧ 𝑋 ∈ (𝐴 ∖ 𝑊)) → (𝐹‘𝑋) = 𝑍)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1542 ∈ wcel 2114 ≠ wne 2933 Vcvv 3430 ∖ cdif 3887 ⊆ wss 3890 {csn 4568 Fn wfn 6487 ⟶wf 6488 ‘cfv 6492 (class class class)co 7360 supp csupp 8103

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5212 ax-sep 5231 ax-nul 5241 ax-pr 5370 ax-un 7682

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-ral 3053 df-rex 3063 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-iun 4936 df-br 5087 df-opab 5149 df-mpt 5168 df-id 5519 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-ov 7363 df-oprab 7364 df-mpo 7365 df-supp 8104

This theorem is referenced by: fsuppmptif 9305 fsuppco2 9309 fsuppcor 9310 cantnfp1lem1 9590 cantnfp1lem3 9592 cantnflem1 9601 cnfcom2lem 9613 gsumval3 19873 gsumcllem 19874 gsumzaddlem 19887 gsumzmhm 19903 gsumpt 19928 gsum2dlem1 19936 gsum2dlem2 19937 gsum2d 19938 gsumxp2 19946 dprdfinv 19987 dprdfadd 19988 dmdprdsplitlem 20005 dpjidcl 20026 gsumdixp 20289 lcomfsupp 20888 uvcresum 21783 frlmsslsp 21786 mplsubglem 21987 mpllsslem 21988 mplsubrglem 21992 mplmonmul 22024 mplcoe1 22025 mplcoe5 22028 mplbas2 22030 evlslem4 22064 evlslem2 22067 evlsvvvallem 22079 evlsvvval 22081 rrxcph 25369 rrxmval 25382 rrxmetlem 25384 rrxmet 25385 rrxdstprj1 25386 deg1mul3le 26092 suppovss 32769 elrspunidl 33503 psrmonmul 33709 fedgmullem1 33789 eulerpartlemb 34528 evlselv 43034 fsuppssindlem1 43038 evlsmhpvvval 43042

W3C validator