Metamath Proof Explorer

Theorem rmsupp0

Description: The support of a mapping of a multiplication of zero with a function into a ring is empty. (Contributed by AV, 10-Apr-2019)

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

Proof

Step Hyp Ref Expression
1 rmsuppss.r 
 |-  R = ( Base ` M )
2 fveq2 
 |-  ( v = w -> ( A ` v ) = ( A ` w ) )
3 2 oveq2d 
 |-  ( v = w -> ( C ( .r ` M ) ( A ` v ) ) = ( C ( .r ` M ) ( A ` w ) ) )
4 3 cbvmptv 
 |-  ( v e. V |-> ( C ( .r ` M ) ( A ` v ) ) ) = ( w e. V |-> ( C ( .r ` M ) ( A ` w ) ) )
5 simpl2 
 |-  ( ( ( M e. Ring /\ V e. X /\ C = ( 0g ` M ) ) /\ A e. ( R ^m V ) ) -> V e. X )
6 fvexd 
 |-  ( ( ( M e. Ring /\ V e. X /\ C = ( 0g ` M ) ) /\ A e. ( R ^m V ) ) -> ( 0g ` M ) e. _V )
7 ovexd 
 |-  ( ( ( ( M e. Ring /\ V e. X /\ C = ( 0g ` M ) ) /\ A e. ( R ^m V ) ) /\ w e. V ) -> ( C ( .r ` M ) ( A ` w ) ) e. _V )
8 4 5 6 7 mptsuppd 
 |-  ( ( ( M e. Ring /\ V e. X /\ C = ( 0g ` M ) ) /\ 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 ) } )
9 simpll3 
 |-  ( ( ( ( M e. Ring /\ V e. X /\ C = ( 0g ` M ) ) /\ A e. ( R ^m V ) ) /\ w e. V ) -> C = ( 0g ` M ) )
10 9 oveq1d 
 |-  ( ( ( ( M e. Ring /\ V e. X /\ C = ( 0g ` M ) ) /\ A e. ( R ^m V ) ) /\ w e. V ) -> ( C ( .r ` M ) ( A ` w ) ) = ( ( 0g ` M ) ( .r ` M ) ( A ` w ) ) )
11 simpll1 
 |-  ( ( ( ( M e. Ring /\ V e. X /\ C = ( 0g ` M ) ) /\ A e. ( R ^m V ) ) /\ w e. V ) -> M e. Ring )
12 elmapi 
 |-  ( A e. ( R ^m V ) -> A : V --> R )
13 ffvelrn 
 |-  ( ( A : V --> R /\ w e. V ) -> ( A ` w ) e. R )
14 13 1 eleqtrdi 
 |-  ( ( A : V --> R /\ w e. V ) -> ( A ` w ) e. ( Base ` M ) )
15 14 ex 
 |-  ( A : V --> R -> ( w e. V -> ( A ` w ) e. ( Base ` M ) ) )
16 12 15 syl 
 |-  ( A e. ( R ^m V ) -> ( w e. V -> ( A ` w ) e. ( Base ` M ) ) )
17 16 adantl 
 |-  ( ( ( M e. Ring /\ V e. X /\ C = ( 0g ` M ) ) /\ A e. ( R ^m V ) ) -> ( w e. V -> ( A ` w ) e. ( Base ` M ) ) )
18 17 imp 
 |-  ( ( ( ( M e. Ring /\ V e. X /\ C = ( 0g ` M ) ) /\ A e. ( R ^m V ) ) /\ w e. V ) -> ( A ` w ) e. ( Base ` M ) )
19 eqid 
 |-  ( Base ` M ) = ( Base ` M )
20 eqid 
 |-  ( .r ` M ) = ( .r ` M )
21 eqid 
 |-  ( 0g ` M ) = ( 0g ` M )
22 19 20 21 ringlz 
 |-  ( ( M e. Ring /\ ( A ` w ) e. ( Base ` M ) ) -> ( ( 0g ` M ) ( .r ` M ) ( A ` w ) ) = ( 0g ` M ) )
23 11 18 22 syl2anc 
 |-  ( ( ( ( M e. Ring /\ V e. X /\ C = ( 0g ` M ) ) /\ A e. ( R ^m V ) ) /\ w e. V ) -> ( ( 0g ` M ) ( .r ` M ) ( A ` w ) ) = ( 0g ` M ) )
24 10 23 eqtrd 
 |-  ( ( ( ( M e. Ring /\ V e. X /\ C = ( 0g ` M ) ) /\ A e. ( R ^m V ) ) /\ w e. V ) -> ( C ( .r ` M ) ( A ` w ) ) = ( 0g ` M ) )
25 24 neeq1d 
 |-  ( ( ( ( M e. Ring /\ V e. X /\ C = ( 0g ` M ) ) /\ A e. ( R ^m V ) ) /\ w e. V ) -> ( ( C ( .r ` M ) ( A ` w ) ) =/= ( 0g ` M ) <-> ( 0g ` M ) =/= ( 0g ` M ) ) )
26 25 rabbidva 
 |-  ( ( ( M e. Ring /\ V e. X /\ C = ( 0g ` M ) ) /\ A e. ( R ^m V ) ) -> { w e. V | ( C ( .r ` M ) ( A ` w ) ) =/= ( 0g ` M ) } = { w e. V | ( 0g ` M ) =/= ( 0g ` M ) } )
27 neirr 
 |-  -. ( 0g ` M ) =/= ( 0g ` M )
28 27 a1i 
 |-  ( ( ( M e. Ring /\ V e. X /\ C = ( 0g ` M ) ) /\ A e. ( R ^m V ) ) -> -. ( 0g ` M ) =/= ( 0g ` M ) )
29 28 ralrimivw 
 |-  ( ( ( M e. Ring /\ V e. X /\ C = ( 0g ` M ) ) /\ A e. ( R ^m V ) ) -> A. w e. V -. ( 0g ` M ) =/= ( 0g ` M ) )
30 rabeq0 
 |-  ( { w e. V | ( 0g ` M ) =/= ( 0g ` M ) } = (/) <-> A. w e. V -. ( 0g ` M ) =/= ( 0g ` M ) )
31 29 30 sylibr 
 |-  ( ( ( M e. Ring /\ V e. X /\ C = ( 0g ` M ) ) /\ A e. ( R ^m V ) ) -> { w e. V | ( 0g ` M ) =/= ( 0g ` M ) } = (/) )
32 8 26 31 3eqtrd 
 |-  ( ( ( M e. Ring /\ V e. X /\ C = ( 0g ` M ) ) /\ A e. ( R ^m V ) ) -> ( ( v e. V |-> ( C ( .r ` M ) ( A ` v ) ) ) supp ( 0g ` M ) ) = (/) )