Metamath Proof Explorer

Theorem scmsuppss

Description: The support of a mapping of a scalar multiplication with a function of scalars is a subset of the support of the function of scalars. (Contributed by AV, 5-Apr-2019)

Ref Expression
Hypotheses scmsuppss.s 
|- S = ( Scalar ` M )
scmsuppss.r 
|- R = ( Base ` S )
Assertion scmsuppss 
|- ( ( M e. LMod /\ V e. ~P ( Base ` M ) /\ A e. ( R ^m V ) ) -> ( ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) supp ( 0g ` M ) ) C_ ( A supp ( 0g ` S ) ) )

Proof

Step Hyp Ref Expression
1 scmsuppss.s 
 |-  S = ( Scalar ` M )
2 scmsuppss.r 
 |-  R = ( Base ` S )
3 elmapi 
 |-  ( A e. ( R ^m V ) -> A : V --> R )
4 fdm 
 |-  ( A : V --> R -> dom A = V )
5 eqidd 
 |-  ( ( ( ( dom A = V /\ A : V --> R ) /\ ( V e. ~P ( Base ` M ) /\ M e. LMod ) ) /\ x e. V ) -> ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) = ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) )
6 fveq2 
 |-  ( v = x -> ( A ` v ) = ( A ` x ) )
7 id 
 |-  ( v = x -> v = x )
8 6 7 oveq12d 
 |-  ( v = x -> ( ( A ` v ) ( .s ` M ) v ) = ( ( A ` x ) ( .s ` M ) x ) )
9 8 adantl 
 |-  ( ( ( ( ( dom A = V /\ A : V --> R ) /\ ( V e. ~P ( Base ` M ) /\ M e. LMod ) ) /\ x e. V ) /\ v = x ) -> ( ( A ` v ) ( .s ` M ) v ) = ( ( A ` x ) ( .s ` M ) x ) )
10 simpr 
 |-  ( ( ( ( dom A = V /\ A : V --> R ) /\ ( V e. ~P ( Base ` M ) /\ M e. LMod ) ) /\ x e. V ) -> x e. V )
11 ovex 
 |-  ( ( A ` x ) ( .s ` M ) x ) e. _V
12 11 a1i 
 |-  ( ( ( ( dom A = V /\ A : V --> R ) /\ ( V e. ~P ( Base ` M ) /\ M e. LMod ) ) /\ x e. V ) -> ( ( A ` x ) ( .s ` M ) x ) e. _V )
13 5 9 10 12 fvmptd 
 |-  ( ( ( ( dom A = V /\ A : V --> R ) /\ ( V e. ~P ( Base ` M ) /\ M e. LMod ) ) /\ x e. V ) -> ( ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) ` x ) = ( ( A ` x ) ( .s ` M ) x ) )
14 13 neeq1d 
 |-  ( ( ( ( dom A = V /\ A : V --> R ) /\ ( V e. ~P ( Base ` M ) /\ M e. LMod ) ) /\ x e. V ) -> ( ( ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) ` x ) =/= ( 0g ` M ) <-> ( ( A ` x ) ( .s ` M ) x ) =/= ( 0g ` M ) ) )
15 oveq1 
 |-  ( ( A ` x ) = ( 0g ` S ) -> ( ( A ` x ) ( .s ` M ) x ) = ( ( 0g ` S ) ( .s ` M ) x ) )
16 simplrr 
 |-  ( ( ( ( dom A = V /\ A : V --> R ) /\ ( V e. ~P ( Base ` M ) /\ M e. LMod ) ) /\ x e. V ) -> M e. LMod )
17 elelpwi 
 |-  ( ( x e. V /\ V e. ~P ( Base ` M ) ) -> x e. ( Base ` M ) )
18 17 expcom 
 |-  ( V e. ~P ( Base ` M ) -> ( x e. V -> x e. ( Base ` M ) ) )
19 18 adantr 
 |-  ( ( V e. ~P ( Base ` M ) /\ M e. LMod ) -> ( x e. V -> x e. ( Base ` M ) ) )
20 19 adantl 
 |-  ( ( ( dom A = V /\ A : V --> R ) /\ ( V e. ~P ( Base ` M ) /\ M e. LMod ) ) -> ( x e. V -> x e. ( Base ` M ) ) )
21 20 imp 
 |-  ( ( ( ( dom A = V /\ A : V --> R ) /\ ( V e. ~P ( Base ` M ) /\ M e. LMod ) ) /\ x e. V ) -> x e. ( Base ` M ) )
22 eqid 
 |-  ( Base ` M ) = ( Base ` M )
23 eqid 
 |-  ( .s ` M ) = ( .s ` M )
24 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
25 eqid 
 |-  ( 0g ` M ) = ( 0g ` M )
26 22 1 23 24 25 lmod0vs 
 |-  ( ( M e. LMod /\ x e. ( Base ` M ) ) -> ( ( 0g ` S ) ( .s ` M ) x ) = ( 0g ` M ) )
27 16 21 26 syl2anc 
 |-  ( ( ( ( dom A = V /\ A : V --> R ) /\ ( V e. ~P ( Base ` M ) /\ M e. LMod ) ) /\ x e. V ) -> ( ( 0g ` S ) ( .s ` M ) x ) = ( 0g ` M ) )
28 15 27 sylan9eqr 
 |-  ( ( ( ( ( dom A = V /\ A : V --> R ) /\ ( V e. ~P ( Base ` M ) /\ M e. LMod ) ) /\ x e. V ) /\ ( A ` x ) = ( 0g ` S ) ) -> ( ( A ` x ) ( .s ` M ) x ) = ( 0g ` M ) )
29 28 ex 
 |-  ( ( ( ( dom A = V /\ A : V --> R ) /\ ( V e. ~P ( Base ` M ) /\ M e. LMod ) ) /\ x e. V ) -> ( ( A ` x ) = ( 0g ` S ) -> ( ( A ` x ) ( .s ` M ) x ) = ( 0g ` M ) ) )
30 29 necon3d 
 |-  ( ( ( ( dom A = V /\ A : V --> R ) /\ ( V e. ~P ( Base ` M ) /\ M e. LMod ) ) /\ x e. V ) -> ( ( ( A ` x ) ( .s ` M ) x ) =/= ( 0g ` M ) -> ( A ` x ) =/= ( 0g ` S ) ) )
31 14 30 sylbid 
 |-  ( ( ( ( dom A = V /\ A : V --> R ) /\ ( V e. ~P ( Base ` M ) /\ M e. LMod ) ) /\ x e. V ) -> ( ( ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) ` x ) =/= ( 0g ` M ) -> ( A ` x ) =/= ( 0g ` S ) ) )
32 31 ss2rabdv 
 |-  ( ( ( dom A = V /\ A : V --> R ) /\ ( V e. ~P ( Base ` M ) /\ M e. LMod ) ) -> { x e. V | ( ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) ` x ) =/= ( 0g ` M ) } C_ { x e. V | ( A ` x ) =/= ( 0g ` S ) } )
33 ovex 
 |-  ( ( A ` v ) ( .s ` M ) v ) e. _V
34 eqid 
 |-  ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) = ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) )
35 33 34 dmmpti 
 |-  dom ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) = V
36 rabeq 
 |-  ( dom ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) = V -> { x e. dom ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) | ( ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) ` x ) =/= ( 0g ` M ) } = { x e. V | ( ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) ` x ) =/= ( 0g ` M ) } )
37 35 36 mp1i 
 |-  ( dom A = V -> { x e. dom ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) | ( ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) ` x ) =/= ( 0g ` M ) } = { x e. V | ( ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) ` x ) =/= ( 0g ` M ) } )
38 rabeq 
 |-  ( dom A = V -> { x e. dom A | ( A ` x ) =/= ( 0g ` S ) } = { x e. V | ( A ` x ) =/= ( 0g ` S ) } )
39 37 38 sseq12d 
 |-  ( dom A = V -> ( { x e. dom ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) | ( ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) ` x ) =/= ( 0g ` M ) } C_ { x e. dom A | ( A ` x ) =/= ( 0g ` S ) } <-> { x e. V | ( ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) ` x ) =/= ( 0g ` M ) } C_ { x e. V | ( A ` x ) =/= ( 0g ` S ) } ) )
40 39 adantr 
 |-  ( ( dom A = V /\ A : V --> R ) -> ( { x e. dom ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) | ( ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) ` x ) =/= ( 0g ` M ) } C_ { x e. dom A | ( A ` x ) =/= ( 0g ` S ) } <-> { x e. V | ( ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) ` x ) =/= ( 0g ` M ) } C_ { x e. V | ( A ` x ) =/= ( 0g ` S ) } ) )
41 40 adantr 
 |-  ( ( ( dom A = V /\ A : V --> R ) /\ ( V e. ~P ( Base ` M ) /\ M e. LMod ) ) -> ( { x e. dom ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) | ( ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) ` x ) =/= ( 0g ` M ) } C_ { x e. dom A | ( A ` x ) =/= ( 0g ` S ) } <-> { x e. V | ( ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) ` x ) =/= ( 0g ` M ) } C_ { x e. V | ( A ` x ) =/= ( 0g ` S ) } ) )
42 32 41 mpbird 
 |-  ( ( ( dom A = V /\ A : V --> R ) /\ ( V e. ~P ( Base ` M ) /\ M e. LMod ) ) -> { x e. dom ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) | ( ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) ` x ) =/= ( 0g ` M ) } C_ { x e. dom A | ( A ` x ) =/= ( 0g ` S ) } )
43 42 exp43 
 |-  ( dom A = V -> ( A : V --> R -> ( V e. ~P ( Base ` M ) -> ( M e. LMod -> { x e. dom ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) | ( ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) ` x ) =/= ( 0g ` M ) } C_ { x e. dom A | ( A ` x ) =/= ( 0g ` S ) } ) ) ) )
44 4 43 mpcom 
 |-  ( A : V --> R -> ( V e. ~P ( Base ` M ) -> ( M e. LMod -> { x e. dom ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) | ( ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) ` x ) =/= ( 0g ` M ) } C_ { x e. dom A | ( A ` x ) =/= ( 0g ` S ) } ) ) )
45 3 44 syl 
 |-  ( A e. ( R ^m V ) -> ( V e. ~P ( Base ` M ) -> ( M e. LMod -> { x e. dom ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) | ( ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) ` x ) =/= ( 0g ` M ) } C_ { x e. dom A | ( A ` x ) =/= ( 0g ` S ) } ) ) )
46 45 com13 
 |-  ( M e. LMod -> ( V e. ~P ( Base ` M ) -> ( A e. ( R ^m V ) -> { x e. dom ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) | ( ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) ` x ) =/= ( 0g ` M ) } C_ { x e. dom A | ( A ` x ) =/= ( 0g ` S ) } ) ) )
47 46 3imp 
 |-  ( ( M e. LMod /\ V e. ~P ( Base ` M ) /\ A e. ( R ^m V ) ) -> { x e. dom ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) | ( ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) ` x ) =/= ( 0g ` M ) } C_ { x e. dom A | ( A ` x ) =/= ( 0g ` S ) } )
48 funmpt 
 |-  Fun ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) )
49 48 a1i 
 |-  ( ( M e. LMod /\ V e. ~P ( Base ` M ) /\ A e. ( R ^m V ) ) -> Fun ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) )
50 mptexg 
 |-  ( V e. ~P ( Base ` M ) -> ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) e. _V )
51 50 3ad2ant2 
 |-  ( ( M e. LMod /\ V e. ~P ( Base ` M ) /\ A e. ( R ^m V ) ) -> ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) e. _V )
52 fvexd 
 |-  ( ( M e. LMod /\ V e. ~P ( Base ` M ) /\ A e. ( R ^m V ) ) -> ( 0g ` M ) e. _V )
53 suppval1 
 |-  ( ( Fun ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) /\ ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) e. _V /\ ( 0g ` M ) e. _V ) -> ( ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) supp ( 0g ` M ) ) = { x e. dom ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) | ( ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) ` x ) =/= ( 0g ` M ) } )
54 49 51 52 53 syl3anc 
 |-  ( ( M e. LMod /\ V e. ~P ( Base ` M ) /\ A e. ( R ^m V ) ) -> ( ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) supp ( 0g ` M ) ) = { x e. dom ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) | ( ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) ` x ) =/= ( 0g ` M ) } )
55 elmapfun 
 |-  ( A e. ( R ^m V ) -> Fun A )
56 55 3ad2ant3 
 |-  ( ( M e. LMod /\ V e. ~P ( Base ` M ) /\ A e. ( R ^m V ) ) -> Fun A )
57 simp3 
 |-  ( ( M e. LMod /\ V e. ~P ( Base ` M ) /\ A e. ( R ^m V ) ) -> A e. ( R ^m V ) )
58 fvexd 
 |-  ( ( M e. LMod /\ V e. ~P ( Base ` M ) /\ A e. ( R ^m V ) ) -> ( 0g ` S ) e. _V )
59 suppval1 
 |-  ( ( Fun A /\ A e. ( R ^m V ) /\ ( 0g ` S ) e. _V ) -> ( A supp ( 0g ` S ) ) = { x e. dom A | ( A ` x ) =/= ( 0g ` S ) } )
60 56 57 58 59 syl3anc 
 |-  ( ( M e. LMod /\ V e. ~P ( Base ` M ) /\ A e. ( R ^m V ) ) -> ( A supp ( 0g ` S ) ) = { x e. dom A | ( A ` x ) =/= ( 0g ` S ) } )
61 47 54 60 3sstr4d 
 |-  ( ( M e. LMod /\ V e. ~P ( Base ` M ) /\ A e. ( R ^m V ) ) -> ( ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) supp ( 0g ` M ) ) C_ ( A supp ( 0g ` S ) ) )