Description: The all-zero vector is contained in the finite hull, since its support is empty and therefore finite. This theorem along with the next one effectively proves that the finite hull is a "submonoid", although that does not exist as a defined concept yet. (Contributed by Stefan O'Rear, 11-Jan-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | dsmmcl.p | |
|
dsmmcl.h | |
||
dsmmcl.i | |
||
dsmmcl.s | |
||
dsmmcl.r | |
||
dsmm0cl.z | |
||
Assertion | dsmm0cl | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dsmmcl.p | |
|
2 | dsmmcl.h | |
|
3 | dsmmcl.i | |
|
4 | dsmmcl.s | |
|
5 | dsmmcl.r | |
|
6 | dsmm0cl.z | |
|
7 | 1 3 4 5 | prdsmndd | |
8 | eqid | |
|
9 | 8 6 | mndidcl | |
10 | 7 9 | syl | |
11 | 1 3 4 5 | prds0g | |
12 | 11 6 | eqtr4di | |
13 | 12 | adantr | |
14 | 13 | fveq1d | |
15 | 5 | ffnd | |
16 | fvco2 | |
|
17 | 15 16 | sylan | |
18 | 14 17 | eqtr3d | |
19 | nne | |
|
20 | 18 19 | sylibr | |
21 | 20 | ralrimiva | |
22 | rabeq0 | |
|
23 | 21 22 | sylibr | |
24 | 0fin | |
|
25 | 23 24 | eqeltrdi | |
26 | eqid | |
|
27 | 1 26 8 2 3 15 | dsmmelbas | |
28 | 10 25 27 | mpbir2and | |