Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  mndpsuppss Structured version   Unicode version

Theorem mndpsuppss 32037
 Description: The support of a mapping of a scalar multiplication with a function of scalars is a subset of the support of the function of scalars. (Contributed by AV, 5-Apr-2019.)
Hypothesis
Ref Expression
mndpsuppss.r
Assertion
Ref Expression
mndpsuppss supp supp supp

Proof of Theorem mndpsuppss
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ioran 490 . . . . . 6
2 nne 2668 . . . . . . 7
3 nne 2668 . . . . . . 7
42, 3anbi12i 697 . . . . . 6
51, 4bitri 249 . . . . 5
6 elmapfn 7438 . . . . . . . . . . . 12
76ad2antrl 727 . . . . . . . . . . 11
87adantr 465 . . . . . . . . . 10
9 elmapfn 7438 . . . . . . . . . . . 12
109ad2antll 728 . . . . . . . . . . 11
1110adantr 465 . . . . . . . . . 10
12 simpr 461 . . . . . . . . . . . 12
1312adantr 465 . . . . . . . . . . 11
1413adantr 465 . . . . . . . . . 10
15 inidm 3707 . . . . . . . . . 10
16 simplrl 759 . . . . . . . . . 10
17 simplrr 760 . . . . . . . . . 10
188, 11, 14, 14, 15, 16, 17ofval 6531 . . . . . . . . 9
1918an32s 802 . . . . . . . 8
20 eqid 2467 . . . . . . . . . . . 12
21 eqid 2467 . . . . . . . . . . . 12
2220, 21mndidcl 15752 . . . . . . . . . . 11
2322ancli 551 . . . . . . . . . 10
2423ad4antr 731 . . . . . . . . 9
25 eqid 2467 . . . . . . . . . 10
2620, 25, 21mndlid 15754 . . . . . . . . 9
2724, 26syl 16 . . . . . . . 8
2819, 27eqtrd 2508 . . . . . . 7
29 nne 2668 . . . . . . 7
3028, 29sylibr 212 . . . . . 6
3130ex 434 . . . . 5
325, 31syl5bi 217 . . . 4
3332con4d 105 . . 3
3433ss2rabdv 3581 . 2
357, 10, 13, 13, 15offn 6533 . . . . 5
36 fnfun 5676 . . . . 5
3735, 36syl 16 . . . 4
38 ovex 6307 . . . . 5
3938a1i 11 . . . 4
40 fvex 5874 . . . . 5
4140a1i 11 . . . 4
42 suppval1 6904 . . . 4 supp
4337, 39, 41, 42syl3anc 1228 . . 3 supp
4413, 7, 10offvalfv 31996 . . . . . 6
4544dmeqd 5203 . . . . 5
46 ovex 6307 . . . . . 6
47 eqid 2467 . . . . . 6
4846, 47dmmpti 5708 . . . . 5
4945, 48syl6eq 2524 . . . 4
50 rabeq 3107 . . . 4
5149, 50syl 16 . . 3
5243, 51eqtrd 2508 . 2 supp
53 elmapi 7437 . . . . . . . 8
54 ffun 5731 . . . . . . . 8
5553, 54syl 16 . . . . . . 7
56 id 22 . . . . . . 7
5740a1i 11 . . . . . . 7
58 suppval1 6904 . . . . . . 7 supp
5955, 56, 57, 58syl3anc 1228 . . . . . 6 supp
60 fdm 5733 . . . . . . 7
61 rabeq 3107 . . . . . . 7
6253, 60, 613syl 20 . . . . . 6
6359, 62eqtrd 2508 . . . . 5 supp
6463ad2antrl 727 . . . 4 supp
65 elmapi 7437 . . . . . . . 8
66 ffun 5731 . . . . . . . 8
6765, 66syl 16 . . . . . . 7
6867ad2antll 728 . . . . . 6
69 simprr 756 . . . . . 6
70 suppval1 6904 . . . . . 6 supp
7168, 69, 41, 70syl3anc 1228 . . . . 5 supp
72 fdm 5733 . . . . . . . 8
7365, 72syl 16 . . . . . . 7
7473ad2antll 728 . . . . . 6
75 rabeq 3107 . . . . . 6
7674, 75syl 16 . . . . 5
7771, 76eqtrd 2508 . . . 4 supp
7864, 77uneq12d 3659 . . 3 supp supp
79 unrab 3769 . . 3
8078, 79syl6eq 2524 . 2 supp supp
8134, 52, 803sstr4d 3547 1 supp supp supp
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wo 368   wa 369   wceq 1379   wcel 1767   wne 2662  crab 2818  cvv 3113   cun 3474   wss 3476   cmpt 4505   cdm 4999   wfun 5580   wfn 5581  wf 5582  cfv 5586  (class class class)co 6282   cof 6520   supp csupp 6898   cmap 7417  cbs 14486   cplusg 14551  c0g 14691  cmnd 15722 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4558  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6574 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-reu 2821  df-rmo 2822  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-iun 4327  df-br 4448  df-opab 4506  df-mpt 4507  df-id 4795  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5549  df-fun 5588  df-fn 5589  df-f 5590  df-f1 5591  df-fo 5592  df-f1o 5593  df-fv 5594  df-riota 6243  df-ov 6285  df-oprab 6286  df-mpt2 6287  df-of 6522  df-1st 6781  df-2nd 6782  df-supp 6899  df-map 7419  df-0g 14693  df-mnd 15728 This theorem is referenced by:  mndpsuppfi  32041
 Copyright terms: Public domain W3C validator