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

Theorem mndpsuppss 39429
 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 492 . . . . . 6
2 nne 2624 . . . . . . 7
3 nne 2624 . . . . . . 7
42, 3anbi12i 701 . . . . . 6
51, 4bitri 252 . . . . 5
6 elmapfn 7498 . . . . . . . . . . . 12
76ad2antrl 732 . . . . . . . . . . 11
87adantr 466 . . . . . . . . . 10
9 elmapfn 7498 . . . . . . . . . . . 12
109ad2antll 733 . . . . . . . . . . 11
1110adantr 466 . . . . . . . . . 10
12 simplr 760 . . . . . . . . . . 11
1312adantr 466 . . . . . . . . . 10
14 inidm 3671 . . . . . . . . . 10
15 simplrl 768 . . . . . . . . . 10
16 simplrr 769 . . . . . . . . . 10
178, 11, 13, 13, 14, 15, 16ofval 6550 . . . . . . . . 9
1817an32s 811 . . . . . . . 8
19 eqid 2422 . . . . . . . . . . . 12
20 eqid 2422 . . . . . . . . . . . 12
2119, 20mndidcl 16541 . . . . . . . . . . 11
2221ancli 553 . . . . . . . . . 10
2322ad4antr 736 . . . . . . . . 9
24 eqid 2422 . . . . . . . . . 10
2519, 24, 20mndlid 16544 . . . . . . . . 9
2623, 25syl 17 . . . . . . . 8
2718, 26eqtrd 2463 . . . . . . 7
28 nne 2624 . . . . . . 7
2927, 28sylibr 215 . . . . . 6
3029ex 435 . . . . 5
315, 30syl5bi 220 . . . 4
3231con4d 108 . . 3
3332ss2rabdv 3542 . 2
347, 10, 12, 12, 14offn 6552 . . . . 5
35 fnfun 5687 . . . . 5
3634, 35syl 17 . . . 4
37 ovex 6329 . . . . 5
3837a1i 11 . . . 4
39 fvex 5887 . . . . 5
4039a1i 11 . . . 4
41 suppval1 6927 . . . 4 supp
4236, 38, 40, 41syl3anc 1264 . . 3 supp
4312, 7, 10offvalfv 39397 . . . . . 6
4443dmeqd 5052 . . . . 5
45 ovex 6329 . . . . . 6
46 eqid 2422 . . . . . 6
4745, 46dmmpti 5721 . . . . 5
4844, 47syl6eq 2479 . . . 4
49 rabeq 3074 . . . 4
5048, 49syl 17 . . 3
5142, 50eqtrd 2463 . 2 supp
52 elmapfun 7499 . . . . . . 7
53 id 23 . . . . . . 7
5439a1i 11 . . . . . . 7
55 suppval1 6927 . . . . . . 7 supp
5652, 53, 54, 55syl3anc 1264 . . . . . 6 supp
57 elmapi 7497 . . . . . . 7
58 fdm 5746 . . . . . . 7
59 rabeq 3074 . . . . . . 7
6057, 58, 593syl 18 . . . . . 6
6156, 60eqtrd 2463 . . . . 5 supp
6261ad2antrl 732 . . . 4 supp
63 elmapfun 7499 . . . . . . 7
6463ad2antll 733 . . . . . 6
65 simprr 764 . . . . . 6
66 suppval1 6927 . . . . . 6 supp
6764, 65, 40, 66syl3anc 1264 . . . . 5 supp
68 elmapi 7497 . . . . . . . 8
69 fdm 5746 . . . . . . . 8
7068, 69syl 17 . . . . . . 7
7170ad2antll 733 . . . . . 6
72 rabeq 3074 . . . . . 6
7371, 72syl 17 . . . . 5
7467, 73eqtrd 2463 . . . 4 supp
7562, 74uneq12d 3621 . . 3 supp supp
76 unrab 3744 . . 3
7775, 76syl6eq 2479 . 2 supp supp
7833, 51, 773sstr4d 3507 1 supp supp supp
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wo 369   wa 370   wceq 1437   wcel 1868   wne 2618  crab 2779  cvv 3081   cun 3434   wss 3436   cmpt 4479   cdm 4849   wfun 5591   wfn 5592  wf 5593  cfv 5597  (class class class)co 6301   cof 6539   supp csupp 6921   cmap 7476  cbs 15108   cplusg 15177  c0g 15325  cmnd 16522 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-rep 4533  ax-sep 4543  ax-nul 4551  ax-pow 4598  ax-pr 4656  ax-un 6593 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-reu 2782  df-rmo 2783  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-iun 4298  df-br 4421  df-opab 4480  df-mpt 4481  df-id 4764  df-xp 4855  df-rel 4856  df-cnv 4857  df-co 4858  df-dm 4859  df-rn 4860  df-res 4861  df-ima 4862  df-iota 5561  df-fun 5599  df-fn 5600  df-f 5601  df-f1 5602  df-fo 5603  df-f1o 5604  df-fv 5605  df-riota 6263  df-ov 6304  df-oprab 6305  df-mpt2 6306  df-of 6541  df-1st 6803  df-2nd 6804  df-supp 6922  df-map 7478  df-0g 15327  df-mgm 16475  df-sgrp 16514  df-mnd 16524 This theorem is referenced by:  mndpsuppfi  39433
 Copyright terms: Public domain W3C validator