Metamath Proof Explorer

Theorem rmsuppss

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)

Ref Expression
Hypothesis rmsuppss.r 
|- R = ( Base ` M )
Assertion rmsuppss 
|- ( ( ( M e. Ring /\ V e. X /\ C e. R ) /\ A e. ( R ^m V ) ) -> ( ( v e. V |-> ( C ( .r ` M ) ( A ` v ) ) ) supp ( 0g ` M ) ) C_ ( A supp ( 0g ` M ) ) )

Proof

Step Hyp Ref Expression
1 rmsuppss.r 
 |-  R = ( Base ` M )
2 oveq2 
 |-  ( ( A ` w ) = ( 0g ` M ) -> ( C ( .r ` M ) ( A ` w ) ) = ( C ( .r ` M ) ( 0g ` M ) ) )
3 simpll1 
 |-  ( ( ( ( M e. Ring /\ V e. X /\ C e. R ) /\ A e. ( R ^m V ) ) /\ w e. V ) -> M e. Ring )
4 simpll3 
 |-  ( ( ( ( M e. Ring /\ V e. X /\ C e. R ) /\ A e. ( R ^m V ) ) /\ w e. V ) -> C e. R )
5 eqid 
 |-  ( .r ` M ) = ( .r ` M )
6 eqid 
 |-  ( 0g ` M ) = ( 0g ` M )
7 1 5 6 ringrz 
 |-  ( ( M e. Ring /\ C e. R ) -> ( C ( .r ` M ) ( 0g ` M ) ) = ( 0g ` M ) )
8 3 4 7 syl2anc 
 |-  ( ( ( ( M e. Ring /\ V e. X /\ C e. R ) /\ A e. ( R ^m V ) ) /\ w e. V ) -> ( C ( .r ` M ) ( 0g ` M ) ) = ( 0g ` M ) )
9 2 8 sylan9eqr 
 |-  ( ( ( ( ( M e. Ring /\ V e. X /\ C e. R ) /\ A e. ( R ^m V ) ) /\ w e. V ) /\ ( A ` w ) = ( 0g ` M ) ) -> ( C ( .r ` M ) ( A ` w ) ) = ( 0g ` M ) )
10 9 ex 
 |-  ( ( ( ( M e. Ring /\ V e. X /\ C e. R ) /\ A e. ( R ^m V ) ) /\ w e. V ) -> ( ( A ` w ) = ( 0g ` M ) -> ( C ( .r ` M ) ( A ` w ) ) = ( 0g ` M ) ) )
11 10 necon3d 
 |-  ( ( ( ( M e. Ring /\ V e. X /\ C e. R ) /\ A e. ( R ^m V ) ) /\ w e. V ) -> ( ( C ( .r ` M ) ( A ` w ) ) =/= ( 0g ` M ) -> ( A ` w ) =/= ( 0g ` M ) ) )
12 11 ss2rabdv 
 |-  ( ( ( M e. Ring /\ V e. X /\ C e. R ) /\ A e. ( R ^m V ) ) -> { w e. V | ( C ( .r ` M ) ( A ` w ) ) =/= ( 0g ` M ) } C_ { w e. V | ( A ` w ) =/= ( 0g ` M ) } )
13 elmapi 
 |-  ( A e. ( R ^m V ) -> A : V --> R )
14 13 fdmd 
 |-  ( A e. ( R ^m V ) -> dom A = V )
15 14 adantl 
 |-  ( ( ( M e. Ring /\ V e. X /\ C e. R ) /\ A e. ( R ^m V ) ) -> dom A = V )
16 rabeq 
 |-  ( dom A = V -> { w e. dom A | ( A ` w ) =/= ( 0g ` M ) } = { w e. V | ( A ` w ) =/= ( 0g ` M ) } )
17 15 16 syl 
 |-  ( ( ( M e. Ring /\ V e. X /\ C e. R ) /\ A e. ( R ^m V ) ) -> { w e. dom A | ( A ` w ) =/= ( 0g ` M ) } = { w e. V | ( A ` w ) =/= ( 0g ` M ) } )
18 12 17 sseqtrrd 
 |-  ( ( ( M e. Ring /\ V e. X /\ C e. R ) /\ A e. ( R ^m V ) ) -> { w e. V | ( C ( .r ` M ) ( A ` w ) ) =/= ( 0g ` M ) } C_ { w e. dom A | ( A ` w ) =/= ( 0g ` M ) } )
19 fveq2 
 |-  ( v = w -> ( A ` v ) = ( A ` w ) )
20 19 oveq2d 
 |-  ( v = w -> ( C ( .r ` M ) ( A ` v ) ) = ( C ( .r ` M ) ( A ` w ) ) )
21 20 cbvmptv 
 |-  ( v e. V |-> ( C ( .r ` M ) ( A ` v ) ) ) = ( w e. V |-> ( C ( .r ` M ) ( A ` w ) ) )
22 simpl2 
 |-  ( ( ( M e. Ring /\ V e. X /\ C e. R ) /\ A e. ( R ^m V ) ) -> V e. X )
23 fvexd 
 |-  ( ( ( M e. Ring /\ V e. X /\ C e. R ) /\ A e. ( R ^m V ) ) -> ( 0g ` M ) e. _V )
24 ovexd 
 |-  ( ( ( ( M e. Ring /\ V e. X /\ C e. R ) /\ A e. ( R ^m V ) ) /\ w e. V ) -> ( C ( .r ` M ) ( A ` w ) ) e. _V )
25 21 22 23 24 mptsuppd 
 |-  ( ( ( M e. Ring /\ V e. X /\ C e. R ) /\ A e. ( R ^m V ) ) -> ( ( v e. V |-> ( C ( .r ` M ) ( A ` v ) ) ) supp ( 0g ` M ) ) = { w e. V | ( C ( .r ` M ) ( A ` w ) ) =/= ( 0g ` M ) } )
26 elmapfun 
 |-  ( A e. ( R ^m V ) -> Fun A )
27 26 adantl 
 |-  ( ( ( M e. Ring /\ V e. X /\ C e. R ) /\ A e. ( R ^m V ) ) -> Fun A )
28 simpr 
 |-  ( ( ( M e. Ring /\ V e. X /\ C e. R ) /\ A e. ( R ^m V ) ) -> A e. ( R ^m V ) )
29 suppval1 
 |-  ( ( Fun A /\ A e. ( R ^m V ) /\ ( 0g ` M ) e. _V ) -> ( A supp ( 0g ` M ) ) = { w e. dom A | ( A ` w ) =/= ( 0g ` M ) } )
30 27 28 23 29 syl3anc 
 |-  ( ( ( M e. Ring /\ V e. X /\ C e. R ) /\ A e. ( R ^m V ) ) -> ( A supp ( 0g ` M ) ) = { w e. dom A | ( A ` w ) =/= ( 0g ` M ) } )
31 18 25 30 3sstr4d 
 |-  ( ( ( M e. Ring /\ V e. X /\ C e. R ) /\ A e. ( R ^m V ) ) -> ( ( v e. V |-> ( C ( .r ` M ) ( A ` v ) ) ) supp ( 0g ` M ) ) C_ ( A supp ( 0g ` M ) ) )