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 
|- LVec C. LMod

Proof

Step Hyp Ref Expression
1 lveclmod 
 |-  ( v e. LVec -> v e. LMod )
2 1 ssriv 
 |-  LVec C_ LMod
3 vex 
 |-  i e. _V
4 vex 
 |-  z e. _V
5 3 4 pm3.2i 
 |-  ( i e. _V /\ z e. _V )
6 eqid 
 |-  { <. ( Base ` ndx ) , { z } >. , <. ( +g ` ndx ) , { <. <. z , z >. , z >. } >. , <. ( .r ` ndx ) , { <. <. z , z >. , z >. } >. } = { <. ( Base ` ndx ) , { z } >. , <. ( +g ` ndx ) , { <. <. z , z >. , z >. } >. , <. ( .r ` ndx ) , { <. <. z , z >. , z >. } >. }
7 eqid 
 |-  ( { <. ( Base ` ndx ) , { i } >. , <. ( +g ` ndx ) , { <. <. i , i >. , i >. } >. , <. ( Scalar ` ndx ) , { <. ( Base ` ndx ) , { z } >. , <. ( +g ` ndx ) , { <. <. z , z >. , z >. } >. , <. ( .r ` ndx ) , { <. <. z , z >. , z >. } >. } >. } u. { <. ( .s ` ndx ) , { <. <. z , i >. , i >. } >. } ) = ( { <. ( Base ` ndx ) , { i } >. , <. ( +g ` ndx ) , { <. <. i , i >. , i >. } >. , <. ( Scalar ` ndx ) , { <. ( Base ` ndx ) , { z } >. , <. ( +g ` ndx ) , { <. <. z , z >. , z >. } >. , <. ( .r ` ndx ) , { <. <. z , z >. , z >. } >. } >. } u. { <. ( .s ` ndx ) , { <. <. z , i >. , i >. } >. } )
8 6 7 lmod1zr 
 |-  ( ( i e. _V /\ z e. _V ) -> ( { <. ( Base ` ndx ) , { i } >. , <. ( +g ` ndx ) , { <. <. i , i >. , i >. } >. , <. ( Scalar ` ndx ) , { <. ( Base ` ndx ) , { z } >. , <. ( +g ` ndx ) , { <. <. z , z >. , z >. } >. , <. ( .r ` ndx ) , { <. <. z , z >. , z >. } >. } >. } u. { <. ( .s ` ndx ) , { <. <. z , i >. , i >. } >. } ) e. LMod )
9 6 7 lmod1zrnlvec 
 |-  ( ( i e. _V /\ z e. _V ) -> ( { <. ( Base ` ndx ) , { i } >. , <. ( +g ` ndx ) , { <. <. i , i >. , i >. } >. , <. ( Scalar ` ndx ) , { <. ( Base ` ndx ) , { z } >. , <. ( +g ` ndx ) , { <. <. z , z >. , z >. } >. , <. ( .r ` ndx ) , { <. <. z , z >. , z >. } >. } >. } u. { <. ( .s ` ndx ) , { <. <. z , i >. , i >. } >. } ) e/ LVec )
10 df-nel 
 |-  ( ( { <. ( Base ` ndx ) , { i } >. , <. ( +g ` ndx ) , { <. <. i , i >. , i >. } >. , <. ( Scalar ` ndx ) , { <. ( Base ` ndx ) , { z } >. , <. ( +g ` ndx ) , { <. <. z , z >. , z >. } >. , <. ( .r ` ndx ) , { <. <. z , z >. , z >. } >. } >. } u. { <. ( .s ` ndx ) , { <. <. z , i >. , i >. } >. } ) e/ LVec <-> -. ( { <. ( Base ` ndx ) , { i } >. , <. ( +g ` ndx ) , { <. <. i , i >. , i >. } >. , <. ( Scalar ` ndx ) , { <. ( Base ` ndx ) , { z } >. , <. ( +g ` ndx ) , { <. <. z , z >. , z >. } >. , <. ( .r ` ndx ) , { <. <. z , z >. , z >. } >. } >. } u. { <. ( .s ` ndx ) , { <. <. z , i >. , i >. } >. } ) e. LVec )
11 9 10 sylib 
 |-  ( ( i e. _V /\ z e. _V ) -> -. ( { <. ( Base ` ndx ) , { i } >. , <. ( +g ` ndx ) , { <. <. i , i >. , i >. } >. , <. ( Scalar ` ndx ) , { <. ( Base ` ndx ) , { z } >. , <. ( +g ` ndx ) , { <. <. z , z >. , z >. } >. , <. ( .r ` ndx ) , { <. <. z , z >. , z >. } >. } >. } u. { <. ( .s ` ndx ) , { <. <. z , i >. , i >. } >. } ) e. LVec )
12 8 11 jca 
 |-  ( ( i e. _V /\ z e. _V ) -> ( ( { <. ( Base ` ndx ) , { i } >. , <. ( +g ` ndx ) , { <. <. i , i >. , i >. } >. , <. ( Scalar ` ndx ) , { <. ( Base ` ndx ) , { z } >. , <. ( +g ` ndx ) , { <. <. z , z >. , z >. } >. , <. ( .r ` ndx ) , { <. <. z , z >. , z >. } >. } >. } u. { <. ( .s ` ndx ) , { <. <. z , i >. , i >. } >. } ) e. LMod /\ -. ( { <. ( Base ` ndx ) , { i } >. , <. ( +g ` ndx ) , { <. <. i , i >. , i >. } >. , <. ( Scalar ` ndx ) , { <. ( Base ` ndx ) , { z } >. , <. ( +g ` ndx ) , { <. <. z , z >. , z >. } >. , <. ( .r ` ndx ) , { <. <. z , z >. , z >. } >. } >. } u. { <. ( .s ` ndx ) , { <. <. z , i >. , i >. } >. } ) e. LVec ) )
13 nelne1 
 |-  ( ( ( { <. ( Base ` ndx ) , { i } >. , <. ( +g ` ndx ) , { <. <. i , i >. , i >. } >. , <. ( Scalar ` ndx ) , { <. ( Base ` ndx ) , { z } >. , <. ( +g ` ndx ) , { <. <. z , z >. , z >. } >. , <. ( .r ` ndx ) , { <. <. z , z >. , z >. } >. } >. } u. { <. ( .s ` ndx ) , { <. <. z , i >. , i >. } >. } ) e. LMod /\ -. ( { <. ( Base ` ndx ) , { i } >. , <. ( +g ` ndx ) , { <. <. i , i >. , i >. } >. , <. ( Scalar ` ndx ) , { <. ( Base ` ndx ) , { z } >. , <. ( +g ` ndx ) , { <. <. z , z >. , z >. } >. , <. ( .r ` ndx ) , { <. <. z , z >. , z >. } >. } >. } u. { <. ( .s ` ndx ) , { <. <. z , i >. , i >. } >. } ) e. LVec ) -> LMod =/= LVec )
14 13 necomd 
 |-  ( ( ( { <. ( Base ` ndx ) , { i } >. , <. ( +g ` ndx ) , { <. <. i , i >. , i >. } >. , <. ( Scalar ` ndx ) , { <. ( Base ` ndx ) , { z } >. , <. ( +g ` ndx ) , { <. <. z , z >. , z >. } >. , <. ( .r ` ndx ) , { <. <. z , z >. , z >. } >. } >. } u. { <. ( .s ` ndx ) , { <. <. z , i >. , i >. } >. } ) e. LMod /\ -. ( { <. ( Base ` ndx ) , { i } >. , <. ( +g ` ndx ) , { <. <. i , i >. , i >. } >. , <. ( Scalar ` ndx ) , { <. ( Base ` ndx ) , { z } >. , <. ( +g ` ndx ) , { <. <. z , z >. , z >. } >. , <. ( .r ` ndx ) , { <. <. z , z >. , z >. } >. } >. } u. { <. ( .s ` ndx ) , { <. <. z , i >. , i >. } >. } ) e. LVec ) -> LVec =/= LMod )
15 5 12 14 mp2b 
 |-  LVec =/= LMod
16 df-pss 
 |-  ( LVec C. LMod <-> ( LVec C_ LMod /\ LVec =/= LMod ) )
17 2 15 16 mpbir2an 
 |-  LVec C. LMod