Metamath Proof Explorer

Theorem domnmsuppn0

Description: The support of a mapping of a multiplication of a nonzero constant with a function into a (ring theoretic) domain equals the support of the function. (Contributed by AV, 11-Apr-2019)

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

Proof

Step Hyp Ref Expression
1 rmsuppss.r 
 |-  R = ( Base ` M )
2 elmapi 
 |-  ( A e. ( R ^m V ) -> A : V --> R )
3 fdm 
 |-  ( A : V --> R -> dom A = V )
4 3 eqcomd 
 |-  ( A : V --> R -> V = dom A )
5 2 4 syl 
 |-  ( A e. ( R ^m V ) -> V = dom A )
6 5 3ad2ant3 
 |-  ( ( ( M e. Domn /\ V e. X ) /\ ( C e. R /\ C =/= ( 0g ` M ) ) /\ A e. ( R ^m V ) ) -> V = dom A )
7 oveq2 
 |-  ( ( A ` w ) = ( 0g ` M ) -> ( C ( .r ` M ) ( A ` w ) ) = ( C ( .r ` M ) ( 0g ` M ) ) )
8 domnring 
 |-  ( M e. Domn -> M e. Ring )
9 8 adantr 
 |-  ( ( M e. Domn /\ V e. X ) -> M e. Ring )
10 simpl 
 |-  ( ( C e. R /\ C =/= ( 0g ` M ) ) -> C e. R )
11 9 10 anim12i 
 |-  ( ( ( M e. Domn /\ V e. X ) /\ ( C e. R /\ C =/= ( 0g ` M ) ) ) -> ( M e. Ring /\ C e. R ) )
12 11 3adant3 
 |-  ( ( ( M e. Domn /\ V e. X ) /\ ( C e. R /\ C =/= ( 0g ` M ) ) /\ A e. ( R ^m V ) ) -> ( M e. Ring /\ C e. R ) )
13 eqid 
 |-  ( .r ` M ) = ( .r ` M )
14 eqid 
 |-  ( 0g ` M ) = ( 0g ` M )
15 1 13 14 ringrz 
 |-  ( ( M e. Ring /\ C e. R ) -> ( C ( .r ` M ) ( 0g ` M ) ) = ( 0g ` M ) )
16 12 15 syl 
 |-  ( ( ( M e. Domn /\ V e. X ) /\ ( C e. R /\ C =/= ( 0g ` M ) ) /\ A e. ( R ^m V ) ) -> ( C ( .r ` M ) ( 0g ` M ) ) = ( 0g ` M ) )
17 16 adantr 
 |-  ( ( ( ( M e. Domn /\ V e. X ) /\ ( C e. R /\ C =/= ( 0g ` M ) ) /\ A e. ( R ^m V ) ) /\ w e. V ) -> ( C ( .r ` M ) ( 0g ` M ) ) = ( 0g ` M ) )
18 7 17 sylan9eqr 
 |-  ( ( ( ( ( M e. Domn /\ V e. X ) /\ ( C e. R /\ C =/= ( 0g ` M ) ) /\ A e. ( R ^m V ) ) /\ w e. V ) /\ ( A ` w ) = ( 0g ` M ) ) -> ( C ( .r ` M ) ( A ` w ) ) = ( 0g ` M ) )
19 18 ex 
 |-  ( ( ( ( M e. Domn /\ V e. X ) /\ ( C e. R /\ C =/= ( 0g ` M ) ) /\ A e. ( R ^m V ) ) /\ w e. V ) -> ( ( A ` w ) = ( 0g ` M ) -> ( C ( .r ` M ) ( A ` w ) ) = ( 0g ` M ) ) )
20 19 necon3d 
 |-  ( ( ( ( M e. Domn /\ V e. X ) /\ ( C e. R /\ C =/= ( 0g ` M ) ) /\ A e. ( R ^m V ) ) /\ w e. V ) -> ( ( C ( .r ` M ) ( A ` w ) ) =/= ( 0g ` M ) -> ( A ` w ) =/= ( 0g ` M ) ) )
21 simpl1l 
 |-  ( ( ( ( M e. Domn /\ V e. X ) /\ ( C e. R /\ C =/= ( 0g ` M ) ) /\ A e. ( R ^m V ) ) /\ w e. V ) -> M e. Domn )
22 21 adantr 
 |-  ( ( ( ( ( M e. Domn /\ V e. X ) /\ ( C e. R /\ C =/= ( 0g ` M ) ) /\ A e. ( R ^m V ) ) /\ w e. V ) /\ ( A ` w ) =/= ( 0g ` M ) ) -> M e. Domn )
23 simpll2 
 |-  ( ( ( ( ( M e. Domn /\ V e. X ) /\ ( C e. R /\ C =/= ( 0g ` M ) ) /\ A e. ( R ^m V ) ) /\ w e. V ) /\ ( A ` w ) =/= ( 0g ` M ) ) -> ( C e. R /\ C =/= ( 0g ` M ) ) )
24 ffvelrn 
 |-  ( ( A : V --> R /\ w e. V ) -> ( A ` w ) e. R )
25 24 ex 
 |-  ( A : V --> R -> ( w e. V -> ( A ` w ) e. R ) )
26 2 25 syl 
 |-  ( A e. ( R ^m V ) -> ( w e. V -> ( A ` w ) e. R ) )
27 26 3ad2ant3 
 |-  ( ( ( M e. Domn /\ V e. X ) /\ ( C e. R /\ C =/= ( 0g ` M ) ) /\ A e. ( R ^m V ) ) -> ( w e. V -> ( A ` w ) e. R ) )
28 27 imp 
 |-  ( ( ( ( M e. Domn /\ V e. X ) /\ ( C e. R /\ C =/= ( 0g ` M ) ) /\ A e. ( R ^m V ) ) /\ w e. V ) -> ( A ` w ) e. R )
29 28 adantr 
 |-  ( ( ( ( ( M e. Domn /\ V e. X ) /\ ( C e. R /\ C =/= ( 0g ` M ) ) /\ A e. ( R ^m V ) ) /\ w e. V ) /\ ( A ` w ) =/= ( 0g ` M ) ) -> ( A ` w ) e. R )
30 simpr 
 |-  ( ( ( ( ( M e. Domn /\ V e. X ) /\ ( C e. R /\ C =/= ( 0g ` M ) ) /\ A e. ( R ^m V ) ) /\ w e. V ) /\ ( A ` w ) =/= ( 0g ` M ) ) -> ( A ` w ) =/= ( 0g ` M ) )
31 1 13 14 domnmuln0 
 |-  ( ( M e. Domn /\ ( C e. R /\ C =/= ( 0g ` M ) ) /\ ( ( A ` w ) e. R /\ ( A ` w ) =/= ( 0g ` M ) ) ) -> ( C ( .r ` M ) ( A ` w ) ) =/= ( 0g ` M ) )
32 22 23 29 30 31 syl112anc 
 |-  ( ( ( ( ( M e. Domn /\ V e. X ) /\ ( C e. R /\ C =/= ( 0g ` M ) ) /\ A e. ( R ^m V ) ) /\ w e. V ) /\ ( A ` w ) =/= ( 0g ` M ) ) -> ( C ( .r ` M ) ( A ` w ) ) =/= ( 0g ` M ) )
33 32 ex 
 |-  ( ( ( ( M e. Domn /\ V e. X ) /\ ( C e. R /\ C =/= ( 0g ` M ) ) /\ A e. ( R ^m V ) ) /\ w e. V ) -> ( ( A ` w ) =/= ( 0g ` M ) -> ( C ( .r ` M ) ( A ` w ) ) =/= ( 0g ` M ) ) )
34 20 33 impbid 
 |-  ( ( ( ( M e. Domn /\ V e. X ) /\ ( C e. R /\ C =/= ( 0g ` M ) ) /\ A e. ( R ^m V ) ) /\ w e. V ) -> ( ( C ( .r ` M ) ( A ` w ) ) =/= ( 0g ` M ) <-> ( A ` w ) =/= ( 0g ` M ) ) )
35 6 34 rabeqbidva 
 |-  ( ( ( M e. Domn /\ V e. X ) /\ ( C e. R /\ C =/= ( 0g ` M ) ) /\ A e. ( R ^m V ) ) -> { w e. V | ( C ( .r ` M ) ( A ` w ) ) =/= ( 0g ` M ) } = { w e. dom A | ( A ` w ) =/= ( 0g ` M ) } )
36 fveq2 
 |-  ( v = w -> ( A ` v ) = ( A ` w ) )
37 36 oveq2d 
 |-  ( v = w -> ( C ( .r ` M ) ( A ` v ) ) = ( C ( .r ` M ) ( A ` w ) ) )
38 37 cbvmptv 
 |-  ( v e. V |-> ( C ( .r ` M ) ( A ` v ) ) ) = ( w e. V |-> ( C ( .r ` M ) ( A ` w ) ) )
39 simp1r 
 |-  ( ( ( M e. Domn /\ V e. X ) /\ ( C e. R /\ C =/= ( 0g ` M ) ) /\ A e. ( R ^m V ) ) -> V e. X )
40 fvexd 
 |-  ( ( ( M e. Domn /\ V e. X ) /\ ( C e. R /\ C =/= ( 0g ` M ) ) /\ A e. ( R ^m V ) ) -> ( 0g ` M ) e. _V )
41 ovexd 
 |-  ( ( ( ( M e. Domn /\ V e. X ) /\ ( C e. R /\ C =/= ( 0g ` M ) ) /\ A e. ( R ^m V ) ) /\ w e. V ) -> ( C ( .r ` M ) ( A ` w ) ) e. _V )
42 38 39 40 41 mptsuppd 
 |-  ( ( ( M e. Domn /\ V e. X ) /\ ( C e. R /\ 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 ) } )
43 elmapfun 
 |-  ( A e. ( R ^m V ) -> Fun A )
44 43 3ad2ant3 
 |-  ( ( ( M e. Domn /\ V e. X ) /\ ( C e. R /\ C =/= ( 0g ` M ) ) /\ A e. ( R ^m V ) ) -> Fun A )
45 simp3 
 |-  ( ( ( M e. Domn /\ V e. X ) /\ ( C e. R /\ C =/= ( 0g ` M ) ) /\ A e. ( R ^m V ) ) -> A e. ( R ^m V ) )
46 suppval1 
 |-  ( ( Fun A /\ A e. ( R ^m V ) /\ ( 0g ` M ) e. _V ) -> ( A supp ( 0g ` M ) ) = { w e. dom A | ( A ` w ) =/= ( 0g ` M ) } )
47 44 45 40 46 syl3anc 
 |-  ( ( ( M e. Domn /\ V e. X ) /\ ( C e. R /\ C =/= ( 0g ` M ) ) /\ A e. ( R ^m V ) ) -> ( A supp ( 0g ` M ) ) = { w e. dom A | ( A ` w ) =/= ( 0g ` M ) } )
48 35 42 47 3eqtr4d 
 |-  ( ( ( M e. Domn /\ V e. X ) /\ ( C e. R /\ C =/= ( 0g ` M ) ) /\ A e. ( R ^m V ) ) -> ( ( v e. V |-> ( C ( .r ` M ) ( A ` v ) ) ) supp ( 0g ` M ) ) = ( A supp ( 0g ` M ) ) )