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

Theorem rmsuppss 39748
 Description: The support of a mapping of a multiplication of a constant with a function into a ring is a subset of the support of the function. (Contributed by AV, 11-Apr-2019.)
Hypothesis
Ref Expression
rmsuppss.r
Assertion
Ref Expression
rmsuppss supp supp
Distinct variable groups:   ,   ,   ,   ,   ,   ,

Proof of Theorem rmsuppss
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 oveq2 6257 . . . . . . 7
2 simpll1 1044 . . . . . . . 8
3 simpll3 1046 . . . . . . . 8
4 rmsuppss.r . . . . . . . . 9
5 eqid 2428 . . . . . . . . 9
6 eqid 2428 . . . . . . . . 9
74, 5, 6ringrz 17761 . . . . . . . 8
82, 3, 7syl2anc 665 . . . . . . 7
91, 8sylan9eqr 2484 . . . . . 6
109ex 435 . . . . 5
1110necon3d 2622 . . . 4
1211ss2rabdv 3485 . . 3
13 elmapi 7448 . . . . . 6
14 fdm 5693 . . . . . 6
1513, 14syl 17 . . . . 5
1615adantl 467 . . . 4
17 rabeq 3015 . . . 4
1816, 17syl 17 . . 3
1912, 18sseqtr4d 3444 . 2
20 fveq2 5825 . . . . 5
2120oveq2d 6265 . . . 4
2221cbvmptv 4459 . . 3
23 simpl2 1009 . . 3
24 fvex 5835 . . . 4
2524a1i 11 . . 3
26 ovex 6277 . . . 4
2726a1i 11 . . 3
2822, 23, 25, 27mptsuppd 6893 . 2 supp
29 elmapfun 7450 . . . 4