Description: There is a (left) module (azero module) which is not a (left) vector space. (Contributed by AV, 29-Apr-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | lmod1zr.r | |
|
lmod1zr.m | |
||
Assertion | lmod1zrnlvec | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lmod1zr.r | |
|
2 | lmod1zr.m | |
|
3 | tpex | |
|
4 | 1 3 | eqeltri | |
5 | 2 | lmodsca | |
6 | 4 5 | mp1i | |
7 | 1 | rng1nnzr | |
8 | df-nel | |
|
9 | 7 8 | sylib | |
10 | drngnzr | |
|
11 | 9 10 | nsyl | |
12 | 11 | adantl | |
13 | 6 12 | eqneltrrd | |
14 | 13 | intnand | |
15 | df-nel | |
|
16 | eqid | |
|
17 | 16 | islvec | |
18 | 15 17 | xchbinx | |
19 | 14 18 | sylibr | |