Metamath Proof Explorer


Theorem lvecpsslmod

Description: The class of all (left) vector spaces is a proper subclass of the class of all (left) modules. Although it is obvious (and proven by lveclmod ) that every left vector space is a left module, there is (at least) one left module which is no left vector space, for example the zero module over the zero ring, see lmod1zrnlvec . (Contributed by AV, 29-Apr-2019)

Ref Expression
Assertion lvecpsslmod LVecLMod

Proof

Step Hyp Ref Expression
1 lveclmod vLVecvLMod
2 1 ssriv LVecLMod
3 vex iV
4 vex zV
5 3 4 pm3.2i iVzV
6 eqid Basendxz+ndxzzzndxzzz=Basendxz+ndxzzzndxzzz
7 eqid Basendxi+ndxiiiScalarndxBasendxz+ndxzzzndxzzzndxzii=Basendxi+ndxiiiScalarndxBasendxz+ndxzzzndxzzzndxzii
8 6 7 lmod1zr iVzVBasendxi+ndxiiiScalarndxBasendxz+ndxzzzndxzzzndxziiLMod
9 6 7 lmod1zrnlvec iVzVBasendxi+ndxiiiScalarndxBasendxz+ndxzzzndxzzzndxziiLVec
10 df-nel Basendxi+ndxiiiScalarndxBasendxz+ndxzzzndxzzzndxziiLVec¬Basendxi+ndxiiiScalarndxBasendxz+ndxzzzndxzzzndxziiLVec
11 9 10 sylib iVzV¬Basendxi+ndxiiiScalarndxBasendxz+ndxzzzndxzzzndxziiLVec
12 8 11 jca iVzVBasendxi+ndxiiiScalarndxBasendxz+ndxzzzndxzzzndxziiLMod¬Basendxi+ndxiiiScalarndxBasendxz+ndxzzzndxzzzndxziiLVec
13 nelne1 Basendxi+ndxiiiScalarndxBasendxz+ndxzzzndxzzzndxziiLMod¬Basendxi+ndxiiiScalarndxBasendxz+ndxzzzndxzzzndxziiLVecLModLVec
14 13 necomd Basendxi+ndxiiiScalarndxBasendxz+ndxzzzndxzzzndxziiLMod¬Basendxi+ndxiiiScalarndxBasendxz+ndxzzzndxzzzndxziiLVecLVecLMod
15 5 12 14 mp2b LVecLMod
16 df-pss LVecLModLVecLModLVecLMod
17 2 15 16 mpbir2an LVecLMod