Metamath Proof Explorer

Theorem mndpsuppss

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
Hypothesis mndpsuppss.r 
|- R = ( Base ` M )
Assertion mndpsuppss 
|- ( ( ( M e. Mnd /\ V e. X ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) -> ( ( A oF ( +g ` M ) B ) supp ( 0g ` M ) ) C_ ( ( A supp ( 0g ` M ) ) u. ( B supp ( 0g ` M ) ) ) )

Proof

Step Hyp Ref Expression
1 mndpsuppss.r 
 |-  R = ( Base ` M )
2 ioran 
 |-  ( -. ( ( A ` x ) =/= ( 0g ` M ) \/ ( B ` x ) =/= ( 0g ` M ) ) <-> ( -. ( A ` x ) =/= ( 0g ` M ) /\ -. ( B ` x ) =/= ( 0g ` M ) ) )
3 nne 
 |-  ( -. ( A ` x ) =/= ( 0g ` M ) <-> ( A ` x ) = ( 0g ` M ) )
4 nne 
 |-  ( -. ( B ` x ) =/= ( 0g ` M ) <-> ( B ` x ) = ( 0g ` M ) )
5 3 4 anbi12i 
 |-  ( ( -. ( A ` x ) =/= ( 0g ` M ) /\ -. ( B ` x ) =/= ( 0g ` M ) ) <-> ( ( A ` x ) = ( 0g ` M ) /\ ( B ` x ) = ( 0g ` M ) ) )
6 2 5 bitri 
 |-  ( -. ( ( A ` x ) =/= ( 0g ` M ) \/ ( B ` x ) =/= ( 0g ` M ) ) <-> ( ( A ` x ) = ( 0g ` M ) /\ ( B ` x ) = ( 0g ` M ) ) )
7 elmapfn 
 |-  ( A e. ( R ^m V ) -> A Fn V )
8 7 ad2antrl 
 |-  ( ( ( M e. Mnd /\ V e. X ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) -> A Fn V )
9 8 adantr 
 |-  ( ( ( ( M e. Mnd /\ V e. X ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) /\ ( ( A ` x ) = ( 0g ` M ) /\ ( B ` x ) = ( 0g ` M ) ) ) -> A Fn V )
10 elmapfn 
 |-  ( B e. ( R ^m V ) -> B Fn V )
11 10 ad2antll 
 |-  ( ( ( M e. Mnd /\ V e. X ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) -> B Fn V )
12 11 adantr 
 |-  ( ( ( ( M e. Mnd /\ V e. X ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) /\ ( ( A ` x ) = ( 0g ` M ) /\ ( B ` x ) = ( 0g ` M ) ) ) -> B Fn V )
13 simplr 
 |-  ( ( ( M e. Mnd /\ V e. X ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) -> V e. X )
14 13 adantr 
 |-  ( ( ( ( M e. Mnd /\ V e. X ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) /\ ( ( A ` x ) = ( 0g ` M ) /\ ( B ` x ) = ( 0g ` M ) ) ) -> V e. X )
15 inidm 
 |-  ( V i^i V ) = V
16 simplrl 
 |-  ( ( ( ( ( M e. Mnd /\ V e. X ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) /\ ( ( A ` x ) = ( 0g ` M ) /\ ( B ` x ) = ( 0g ` M ) ) ) /\ x e. V ) -> ( A ` x ) = ( 0g ` M ) )
17 simplrr 
 |-  ( ( ( ( ( M e. Mnd /\ V e. X ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) /\ ( ( A ` x ) = ( 0g ` M ) /\ ( B ` x ) = ( 0g ` M ) ) ) /\ x e. V ) -> ( B ` x ) = ( 0g ` M ) )
18 9 12 14 14 15 16 17 ofval 
 |-  ( ( ( ( ( M e. Mnd /\ V e. X ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) /\ ( ( A ` x ) = ( 0g ` M ) /\ ( B ` x ) = ( 0g ` M ) ) ) /\ x e. V ) -> ( ( A oF ( +g ` M ) B ) ` x ) = ( ( 0g ` M ) ( +g ` M ) ( 0g ` M ) ) )
19 18 an32s 
 |-  ( ( ( ( ( M e. Mnd /\ V e. X ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) /\ x e. V ) /\ ( ( A ` x ) = ( 0g ` M ) /\ ( B ` x ) = ( 0g ` M ) ) ) -> ( ( A oF ( +g ` M ) B ) ` x ) = ( ( 0g ` M ) ( +g ` M ) ( 0g ` M ) ) )
20 eqid 
 |-  ( Base ` M ) = ( Base ` M )
21 eqid 
 |-  ( 0g ` M ) = ( 0g ` M )
22 20 21 mndidcl 
 |-  ( M e. Mnd -> ( 0g ` M ) e. ( Base ` M ) )
23 22 ancli 
 |-  ( M e. Mnd -> ( M e. Mnd /\ ( 0g ` M ) e. ( Base ` M ) ) )
24 23 ad4antr 
 |-  ( ( ( ( ( M e. Mnd /\ V e. X ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) /\ x e. V ) /\ ( ( A ` x ) = ( 0g ` M ) /\ ( B ` x ) = ( 0g ` M ) ) ) -> ( M e. Mnd /\ ( 0g ` M ) e. ( Base ` M ) ) )
25 eqid 
 |-  ( +g ` M ) = ( +g ` M )
26 20 25 21 mndlid 
 |-  ( ( M e. Mnd /\ ( 0g ` M ) e. ( Base ` M ) ) -> ( ( 0g ` M ) ( +g ` M ) ( 0g ` M ) ) = ( 0g ` M ) )
27 24 26 syl 
 |-  ( ( ( ( ( M e. Mnd /\ V e. X ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) /\ x e. V ) /\ ( ( A ` x ) = ( 0g ` M ) /\ ( B ` x ) = ( 0g ` M ) ) ) -> ( ( 0g ` M ) ( +g ` M ) ( 0g ` M ) ) = ( 0g ` M ) )
28 19 27 eqtrd 
 |-  ( ( ( ( ( M e. Mnd /\ V e. X ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) /\ x e. V ) /\ ( ( A ` x ) = ( 0g ` M ) /\ ( B ` x ) = ( 0g ` M ) ) ) -> ( ( A oF ( +g ` M ) B ) ` x ) = ( 0g ` M ) )
29 nne 
 |-  ( -. ( ( A oF ( +g ` M ) B ) ` x ) =/= ( 0g ` M ) <-> ( ( A oF ( +g ` M ) B ) ` x ) = ( 0g ` M ) )
30 28 29 sylibr 
 |-  ( ( ( ( ( M e. Mnd /\ V e. X ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) /\ x e. V ) /\ ( ( A ` x ) = ( 0g ` M ) /\ ( B ` x ) = ( 0g ` M ) ) ) -> -. ( ( A oF ( +g ` M ) B ) ` x ) =/= ( 0g ` M ) )
31 30 ex 
 |-  ( ( ( ( M e. Mnd /\ V e. X ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) /\ x e. V ) -> ( ( ( A ` x ) = ( 0g ` M ) /\ ( B ` x ) = ( 0g ` M ) ) -> -. ( ( A oF ( +g ` M ) B ) ` x ) =/= ( 0g ` M ) ) )
32 6 31 syl5bi 
 |-  ( ( ( ( M e. Mnd /\ V e. X ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) /\ x e. V ) -> ( -. ( ( A ` x ) =/= ( 0g ` M ) \/ ( B ` x ) =/= ( 0g ` M ) ) -> -. ( ( A oF ( +g ` M ) B ) ` x ) =/= ( 0g ` M ) ) )
33 32 con4d 
 |-  ( ( ( ( M e. Mnd /\ V e. X ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) /\ x e. V ) -> ( ( ( A oF ( +g ` M ) B ) ` x ) =/= ( 0g ` M ) -> ( ( A ` x ) =/= ( 0g ` M ) \/ ( B ` x ) =/= ( 0g ` M ) ) ) )
34 33 ss2rabdv 
 |-  ( ( ( M e. Mnd /\ V e. X ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) -> { x e. V | ( ( A oF ( +g ` M ) B ) ` x ) =/= ( 0g ` M ) } C_ { x e. V | ( ( A ` x ) =/= ( 0g ` M ) \/ ( B ` x ) =/= ( 0g ` M ) ) } )
35 8 11 13 13 offun 
 |-  ( ( ( M e. Mnd /\ V e. X ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) -> Fun ( A oF ( +g ` M ) B ) )
36 ovexd 
 |-  ( ( ( M e. Mnd /\ V e. X ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) -> ( A oF ( +g ` M ) B ) e. _V )
37 fvexd 
 |-  ( ( ( M e. Mnd /\ V e. X ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) -> ( 0g ` M ) e. _V )
38 suppval1 
 |-  ( ( Fun ( A oF ( +g ` M ) B ) /\ ( A oF ( +g ` M ) B ) e. _V /\ ( 0g ` M ) e. _V ) -> ( ( A oF ( +g ` M ) B ) supp ( 0g ` M ) ) = { x e. dom ( A oF ( +g ` M ) B ) | ( ( A oF ( +g ` M ) B ) ` x ) =/= ( 0g ` M ) } )
39 35 36 37 38 syl3anc 
 |-  ( ( ( M e. Mnd /\ V e. X ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) -> ( ( A oF ( +g ` M ) B ) supp ( 0g ` M ) ) = { x e. dom ( A oF ( +g ` M ) B ) | ( ( A oF ( +g ` M ) B ) ` x ) =/= ( 0g ` M ) } )
40 13 8 11 offvalfv 
 |-  ( ( ( M e. Mnd /\ V e. X ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) -> ( A oF ( +g ` M ) B ) = ( v e. V |-> ( ( A ` v ) ( +g ` M ) ( B ` v ) ) ) )
41 40 dmeqd 
 |-  ( ( ( M e. Mnd /\ V e. X ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) -> dom ( A oF ( +g ` M ) B ) = dom ( v e. V |-> ( ( A ` v ) ( +g ` M ) ( B ` v ) ) ) )
42 ovex 
 |-  ( ( A ` v ) ( +g ` M ) ( B ` v ) ) e. _V
43 eqid 
 |-  ( v e. V |-> ( ( A ` v ) ( +g ` M ) ( B ` v ) ) ) = ( v e. V |-> ( ( A ` v ) ( +g ` M ) ( B ` v ) ) )
44 42 43 dmmpti 
 |-  dom ( v e. V |-> ( ( A ` v ) ( +g ` M ) ( B ` v ) ) ) = V
45 41 44 eqtrdi 
 |-  ( ( ( M e. Mnd /\ V e. X ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) -> dom ( A oF ( +g ` M ) B ) = V )
46 45 rabeqdv 
 |-  ( ( ( M e. Mnd /\ V e. X ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) -> { x e. dom ( A oF ( +g ` M ) B ) | ( ( A oF ( +g ` M ) B ) ` x ) =/= ( 0g ` M ) } = { x e. V | ( ( A oF ( +g ` M ) B ) ` x ) =/= ( 0g ` M ) } )
47 39 46 eqtrd 
 |-  ( ( ( M e. Mnd /\ V e. X ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) -> ( ( A oF ( +g ` M ) B ) supp ( 0g ` M ) ) = { x e. V | ( ( A oF ( +g ` M ) B ) ` x ) =/= ( 0g ` M ) } )
48 elmapfun 
 |-  ( A e. ( R ^m V ) -> Fun A )
49 id 
 |-  ( A e. ( R ^m V ) -> A e. ( R ^m V ) )
50 fvexd 
 |-  ( A e. ( R ^m V ) -> ( 0g ` M ) e. _V )
51 suppval1 
 |-  ( ( Fun A /\ A e. ( R ^m V ) /\ ( 0g ` M ) e. _V ) -> ( A supp ( 0g ` M ) ) = { x e. dom A | ( A ` x ) =/= ( 0g ` M ) } )
52 48 49 50 51 syl3anc 
 |-  ( A e. ( R ^m V ) -> ( A supp ( 0g ` M ) ) = { x e. dom A | ( A ` x ) =/= ( 0g ` M ) } )
53 elmapi 
 |-  ( A e. ( R ^m V ) -> A : V --> R )
54 fdm 
 |-  ( A : V --> R -> dom A = V )
55 rabeq 
 |-  ( dom A = V -> { x e. dom A | ( A ` x ) =/= ( 0g ` M ) } = { x e. V | ( A ` x ) =/= ( 0g ` M ) } )
56 53 54 55 3syl 
 |-  ( A e. ( R ^m V ) -> { x e. dom A | ( A ` x ) =/= ( 0g ` M ) } = { x e. V | ( A ` x ) =/= ( 0g ` M ) } )
57 52 56 eqtrd 
 |-  ( A e. ( R ^m V ) -> ( A supp ( 0g ` M ) ) = { x e. V | ( A ` x ) =/= ( 0g ` M ) } )
58 57 ad2antrl 
 |-  ( ( ( M e. Mnd /\ V e. X ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) -> ( A supp ( 0g ` M ) ) = { x e. V | ( A ` x ) =/= ( 0g ` M ) } )
59 elmapfun 
 |-  ( B e. ( R ^m V ) -> Fun B )
60 59 ad2antll 
 |-  ( ( ( M e. Mnd /\ V e. X ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) -> Fun B )
61 simprr 
 |-  ( ( ( M e. Mnd /\ V e. X ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) -> B e. ( R ^m V ) )
62 suppval1 
 |-  ( ( Fun B /\ B e. ( R ^m V ) /\ ( 0g ` M ) e. _V ) -> ( B supp ( 0g ` M ) ) = { x e. dom B | ( B ` x ) =/= ( 0g ` M ) } )
63 60 61 37 62 syl3anc 
 |-  ( ( ( M e. Mnd /\ V e. X ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) -> ( B supp ( 0g ` M ) ) = { x e. dom B | ( B ` x ) =/= ( 0g ` M ) } )
64 elmapi 
 |-  ( B e. ( R ^m V ) -> B : V --> R )
65 64 fdmd 
 |-  ( B e. ( R ^m V ) -> dom B = V )
66 65 ad2antll 
 |-  ( ( ( M e. Mnd /\ V e. X ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) -> dom B = V )
67 66 rabeqdv 
 |-  ( ( ( M e. Mnd /\ V e. X ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) -> { x e. dom B | ( B ` x ) =/= ( 0g ` M ) } = { x e. V | ( B ` x ) =/= ( 0g ` M ) } )
68 63 67 eqtrd 
 |-  ( ( ( M e. Mnd /\ V e. X ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) -> ( B supp ( 0g ` M ) ) = { x e. V | ( B ` x ) =/= ( 0g ` M ) } )
69 58 68 uneq12d 
 |-  ( ( ( M e. Mnd /\ V e. X ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) -> ( ( A supp ( 0g ` M ) ) u. ( B supp ( 0g ` M ) ) ) = ( { x e. V | ( A ` x ) =/= ( 0g ` M ) } u. { x e. V | ( B ` x ) =/= ( 0g ` M ) } ) )
70 unrab 
 |-  ( { x e. V | ( A ` x ) =/= ( 0g ` M ) } u. { x e. V | ( B ` x ) =/= ( 0g ` M ) } ) = { x e. V | ( ( A ` x ) =/= ( 0g ` M ) \/ ( B ` x ) =/= ( 0g ` M ) ) }
71 69 70 eqtrdi 
 |-  ( ( ( M e. Mnd /\ V e. X ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) -> ( ( A supp ( 0g ` M ) ) u. ( B supp ( 0g ` M ) ) ) = { x e. V | ( ( A ` x ) =/= ( 0g ` M ) \/ ( B ` x ) =/= ( 0g ` M ) ) } )
72 34 47 71 3sstr4d 
 |-  ( ( ( M e. Mnd /\ V e. X ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) -> ( ( A oF ( +g ` M ) B ) supp ( 0g ` M ) ) C_ ( ( A supp ( 0g ` M ) ) u. ( B supp ( 0g ` M ) ) ) )