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

Theorem rmsuppss 31911
 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 6283 . . . . . . 7
2 simpll1 1030 . . . . . . . 8
3 simpll3 1032 . . . . . . . 8
4 rmsuppss.r . . . . . . . . 9
5 eqid 2460 . . . . . . . . 9
6 eqid 2460 . . . . . . . . 9
74, 5, 6rngrz 17016 . . . . . . . 8
82, 3, 7syl2anc 661 . . . . . . 7
91, 8sylan9eqr 2523 . . . . . 6
109ex 434 . . . . 5
1110necon3d 2684 . . . 4
1211ss2rabdv 3574 . . 3
13 elmapi 7430 . . . . . 6
14 fdm 5726 . . . . . 6
1513, 14syl 16 . . . . 5
1615adantl 466 . . . 4
17 rabeq 3100 . . . 4
1816, 17syl 16 . . 3
1912, 18sseqtr4d 3534 . 2
20 fveq2 5857 . . . . 5
2120oveq2d 6291 . . . 4
2221cbvmptv 4531 . . 3
23 simpl2 995 . . 3
24 fvex 5867 . . . 4
2524a1i 11 . . 3
26 ovex 6300 . . . 4
2726a1i 11 . . 3
2822, 23, 25, 27mptsuppd 6913 . 2 supp
29 ffun 5724 . . . . 5
3013, 29syl 16 . . . 4