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 โŠŠ LMod

Proof

Step Hyp Ref Expression
1 lveclmod โŠข ( ๐‘ฃ โˆˆ LVec โ†’ ๐‘ฃ โˆˆ LMod )
2 1 ssriv โŠข LVec โŠ† LMod
3 vex โŠข ๐‘– โˆˆ V
4 vex โŠข ๐‘ง โˆˆ V
5 3 4 pm3.2i โŠข ( ๐‘– โˆˆ V โˆง ๐‘ง โˆˆ V )
6 eqid โŠข { โŸจ ( Base โ€˜ ndx ) , { ๐‘ง } โŸฉ , โŸจ ( +g โ€˜ ndx ) , { โŸจ โŸจ ๐‘ง , ๐‘ง โŸฉ , ๐‘ง โŸฉ } โŸฉ , โŸจ ( .r โ€˜ ndx ) , { โŸจ โŸจ ๐‘ง , ๐‘ง โŸฉ , ๐‘ง โŸฉ } โŸฉ } = { โŸจ ( Base โ€˜ ndx ) , { ๐‘ง } โŸฉ , โŸจ ( +g โ€˜ ndx ) , { โŸจ โŸจ ๐‘ง , ๐‘ง โŸฉ , ๐‘ง โŸฉ } โŸฉ , โŸจ ( .r โ€˜ ndx ) , { โŸจ โŸจ ๐‘ง , ๐‘ง โŸฉ , ๐‘ง โŸฉ } โŸฉ }
7 eqid โŠข ( { โŸจ ( Base โ€˜ ndx ) , { ๐‘– } โŸฉ , โŸจ ( +g โ€˜ ndx ) , { โŸจ โŸจ ๐‘– , ๐‘– โŸฉ , ๐‘– โŸฉ } โŸฉ , โŸจ ( Scalar โ€˜ ndx ) , { โŸจ ( Base โ€˜ ndx ) , { ๐‘ง } โŸฉ , โŸจ ( +g โ€˜ ndx ) , { โŸจ โŸจ ๐‘ง , ๐‘ง โŸฉ , ๐‘ง โŸฉ } โŸฉ , โŸจ ( .r โ€˜ ndx ) , { โŸจ โŸจ ๐‘ง , ๐‘ง โŸฉ , ๐‘ง โŸฉ } โŸฉ } โŸฉ } โˆช { โŸจ ( ยท๐‘  โ€˜ ndx ) , { โŸจ โŸจ ๐‘ง , ๐‘– โŸฉ , ๐‘– โŸฉ } โŸฉ } ) = ( { โŸจ ( Base โ€˜ ndx ) , { ๐‘– } โŸฉ , โŸจ ( +g โ€˜ ndx ) , { โŸจ โŸจ ๐‘– , ๐‘– โŸฉ , ๐‘– โŸฉ } โŸฉ , โŸจ ( Scalar โ€˜ ndx ) , { โŸจ ( Base โ€˜ ndx ) , { ๐‘ง } โŸฉ , โŸจ ( +g โ€˜ ndx ) , { โŸจ โŸจ ๐‘ง , ๐‘ง โŸฉ , ๐‘ง โŸฉ } โŸฉ , โŸจ ( .r โ€˜ ndx ) , { โŸจ โŸจ ๐‘ง , ๐‘ง โŸฉ , ๐‘ง โŸฉ } โŸฉ } โŸฉ } โˆช { โŸจ ( ยท๐‘  โ€˜ ndx ) , { โŸจ โŸจ ๐‘ง , ๐‘– โŸฉ , ๐‘– โŸฉ } โŸฉ } )
8 6 7 lmod1zr โŠข ( ( ๐‘– โˆˆ V โˆง ๐‘ง โˆˆ V ) โ†’ ( { โŸจ ( Base โ€˜ ndx ) , { ๐‘– } โŸฉ , โŸจ ( +g โ€˜ ndx ) , { โŸจ โŸจ ๐‘– , ๐‘– โŸฉ , ๐‘– โŸฉ } โŸฉ , โŸจ ( Scalar โ€˜ ndx ) , { โŸจ ( Base โ€˜ ndx ) , { ๐‘ง } โŸฉ , โŸจ ( +g โ€˜ ndx ) , { โŸจ โŸจ ๐‘ง , ๐‘ง โŸฉ , ๐‘ง โŸฉ } โŸฉ , โŸจ ( .r โ€˜ ndx ) , { โŸจ โŸจ ๐‘ง , ๐‘ง โŸฉ , ๐‘ง โŸฉ } โŸฉ } โŸฉ } โˆช { โŸจ ( ยท๐‘  โ€˜ ndx ) , { โŸจ โŸจ ๐‘ง , ๐‘– โŸฉ , ๐‘– โŸฉ } โŸฉ } ) โˆˆ LMod )
9 6 7 lmod1zrnlvec โŠข ( ( ๐‘– โˆˆ V โˆง ๐‘ง โˆˆ V ) โ†’ ( { โŸจ ( Base โ€˜ ndx ) , { ๐‘– } โŸฉ , โŸจ ( +g โ€˜ ndx ) , { โŸจ โŸจ ๐‘– , ๐‘– โŸฉ , ๐‘– โŸฉ } โŸฉ , โŸจ ( Scalar โ€˜ ndx ) , { โŸจ ( Base โ€˜ ndx ) , { ๐‘ง } โŸฉ , โŸจ ( +g โ€˜ ndx ) , { โŸจ โŸจ ๐‘ง , ๐‘ง โŸฉ , ๐‘ง โŸฉ } โŸฉ , โŸจ ( .r โ€˜ ndx ) , { โŸจ โŸจ ๐‘ง , ๐‘ง โŸฉ , ๐‘ง โŸฉ } โŸฉ } โŸฉ } โˆช { โŸจ ( ยท๐‘  โ€˜ ndx ) , { โŸจ โŸจ ๐‘ง , ๐‘– โŸฉ , ๐‘– โŸฉ } โŸฉ } ) โˆ‰ LVec )
10 df-nel โŠข ( ( { โŸจ ( Base โ€˜ ndx ) , { ๐‘– } โŸฉ , โŸจ ( +g โ€˜ ndx ) , { โŸจ โŸจ ๐‘– , ๐‘– โŸฉ , ๐‘– โŸฉ } โŸฉ , โŸจ ( Scalar โ€˜ ndx ) , { โŸจ ( Base โ€˜ ndx ) , { ๐‘ง } โŸฉ , โŸจ ( +g โ€˜ ndx ) , { โŸจ โŸจ ๐‘ง , ๐‘ง โŸฉ , ๐‘ง โŸฉ } โŸฉ , โŸจ ( .r โ€˜ ndx ) , { โŸจ โŸจ ๐‘ง , ๐‘ง โŸฉ , ๐‘ง โŸฉ } โŸฉ } โŸฉ } โˆช { โŸจ ( ยท๐‘  โ€˜ ndx ) , { โŸจ โŸจ ๐‘ง , ๐‘– โŸฉ , ๐‘– โŸฉ } โŸฉ } ) โˆ‰ LVec โ†” ยฌ ( { โŸจ ( Base โ€˜ ndx ) , { ๐‘– } โŸฉ , โŸจ ( +g โ€˜ ndx ) , { โŸจ โŸจ ๐‘– , ๐‘– โŸฉ , ๐‘– โŸฉ } โŸฉ , โŸจ ( Scalar โ€˜ ndx ) , { โŸจ ( Base โ€˜ ndx ) , { ๐‘ง } โŸฉ , โŸจ ( +g โ€˜ ndx ) , { โŸจ โŸจ ๐‘ง , ๐‘ง โŸฉ , ๐‘ง โŸฉ } โŸฉ , โŸจ ( .r โ€˜ ndx ) , { โŸจ โŸจ ๐‘ง , ๐‘ง โŸฉ , ๐‘ง โŸฉ } โŸฉ } โŸฉ } โˆช { โŸจ ( ยท๐‘  โ€˜ ndx ) , { โŸจ โŸจ ๐‘ง , ๐‘– โŸฉ , ๐‘– โŸฉ } โŸฉ } ) โˆˆ LVec )
11 9 10 sylib โŠข ( ( ๐‘– โˆˆ V โˆง ๐‘ง โˆˆ V ) โ†’ ยฌ ( { โŸจ ( Base โ€˜ ndx ) , { ๐‘– } โŸฉ , โŸจ ( +g โ€˜ ndx ) , { โŸจ โŸจ ๐‘– , ๐‘– โŸฉ , ๐‘– โŸฉ } โŸฉ , โŸจ ( Scalar โ€˜ ndx ) , { โŸจ ( Base โ€˜ ndx ) , { ๐‘ง } โŸฉ , โŸจ ( +g โ€˜ ndx ) , { โŸจ โŸจ ๐‘ง , ๐‘ง โŸฉ , ๐‘ง โŸฉ } โŸฉ , โŸจ ( .r โ€˜ ndx ) , { โŸจ โŸจ ๐‘ง , ๐‘ง โŸฉ , ๐‘ง โŸฉ } โŸฉ } โŸฉ } โˆช { โŸจ ( ยท๐‘  โ€˜ ndx ) , { โŸจ โŸจ ๐‘ง , ๐‘– โŸฉ , ๐‘– โŸฉ } โŸฉ } ) โˆˆ LVec )
12 8 11 jca โŠข ( ( ๐‘– โˆˆ V โˆง ๐‘ง โˆˆ V ) โ†’ ( ( { โŸจ ( Base โ€˜ ndx ) , { ๐‘– } โŸฉ , โŸจ ( +g โ€˜ ndx ) , { โŸจ โŸจ ๐‘– , ๐‘– โŸฉ , ๐‘– โŸฉ } โŸฉ , โŸจ ( Scalar โ€˜ ndx ) , { โŸจ ( Base โ€˜ ndx ) , { ๐‘ง } โŸฉ , โŸจ ( +g โ€˜ ndx ) , { โŸจ โŸจ ๐‘ง , ๐‘ง โŸฉ , ๐‘ง โŸฉ } โŸฉ , โŸจ ( .r โ€˜ ndx ) , { โŸจ โŸจ ๐‘ง , ๐‘ง โŸฉ , ๐‘ง โŸฉ } โŸฉ } โŸฉ } โˆช { โŸจ ( ยท๐‘  โ€˜ ndx ) , { โŸจ โŸจ ๐‘ง , ๐‘– โŸฉ , ๐‘– โŸฉ } โŸฉ } ) โˆˆ LMod โˆง ยฌ ( { โŸจ ( Base โ€˜ ndx ) , { ๐‘– } โŸฉ , โŸจ ( +g โ€˜ ndx ) , { โŸจ โŸจ ๐‘– , ๐‘– โŸฉ , ๐‘– โŸฉ } โŸฉ , โŸจ ( Scalar โ€˜ ndx ) , { โŸจ ( Base โ€˜ ndx ) , { ๐‘ง } โŸฉ , โŸจ ( +g โ€˜ ndx ) , { โŸจ โŸจ ๐‘ง , ๐‘ง โŸฉ , ๐‘ง โŸฉ } โŸฉ , โŸจ ( .r โ€˜ ndx ) , { โŸจ โŸจ ๐‘ง , ๐‘ง โŸฉ , ๐‘ง โŸฉ } โŸฉ } โŸฉ } โˆช { โŸจ ( ยท๐‘  โ€˜ ndx ) , { โŸจ โŸจ ๐‘ง , ๐‘– โŸฉ , ๐‘– โŸฉ } โŸฉ } ) โˆˆ LVec ) )
13 nelne1 โŠข ( ( ( { โŸจ ( Base โ€˜ ndx ) , { ๐‘– } โŸฉ , โŸจ ( +g โ€˜ ndx ) , { โŸจ โŸจ ๐‘– , ๐‘– โŸฉ , ๐‘– โŸฉ } โŸฉ , โŸจ ( Scalar โ€˜ ndx ) , { โŸจ ( Base โ€˜ ndx ) , { ๐‘ง } โŸฉ , โŸจ ( +g โ€˜ ndx ) , { โŸจ โŸจ ๐‘ง , ๐‘ง โŸฉ , ๐‘ง โŸฉ } โŸฉ , โŸจ ( .r โ€˜ ndx ) , { โŸจ โŸจ ๐‘ง , ๐‘ง โŸฉ , ๐‘ง โŸฉ } โŸฉ } โŸฉ } โˆช { โŸจ ( ยท๐‘  โ€˜ ndx ) , { โŸจ โŸจ ๐‘ง , ๐‘– โŸฉ , ๐‘– โŸฉ } โŸฉ } ) โˆˆ LMod โˆง ยฌ ( { โŸจ ( Base โ€˜ ndx ) , { ๐‘– } โŸฉ , โŸจ ( +g โ€˜ ndx ) , { โŸจ โŸจ ๐‘– , ๐‘– โŸฉ , ๐‘– โŸฉ } โŸฉ , โŸจ ( Scalar โ€˜ ndx ) , { โŸจ ( Base โ€˜ ndx ) , { ๐‘ง } โŸฉ , โŸจ ( +g โ€˜ ndx ) , { โŸจ โŸจ ๐‘ง , ๐‘ง โŸฉ , ๐‘ง โŸฉ } โŸฉ , โŸจ ( .r โ€˜ ndx ) , { โŸจ โŸจ ๐‘ง , ๐‘ง โŸฉ , ๐‘ง โŸฉ } โŸฉ } โŸฉ } โˆช { โŸจ ( ยท๐‘  โ€˜ ndx ) , { โŸจ โŸจ ๐‘ง , ๐‘– โŸฉ , ๐‘– โŸฉ } โŸฉ } ) โˆˆ LVec ) โ†’ LMod โ‰  LVec )
14 13 necomd โŠข ( ( ( { โŸจ ( Base โ€˜ ndx ) , { ๐‘– } โŸฉ , โŸจ ( +g โ€˜ ndx ) , { โŸจ โŸจ ๐‘– , ๐‘– โŸฉ , ๐‘– โŸฉ } โŸฉ , โŸจ ( Scalar โ€˜ ndx ) , { โŸจ ( Base โ€˜ ndx ) , { ๐‘ง } โŸฉ , โŸจ ( +g โ€˜ ndx ) , { โŸจ โŸจ ๐‘ง , ๐‘ง โŸฉ , ๐‘ง โŸฉ } โŸฉ , โŸจ ( .r โ€˜ ndx ) , { โŸจ โŸจ ๐‘ง , ๐‘ง โŸฉ , ๐‘ง โŸฉ } โŸฉ } โŸฉ } โˆช { โŸจ ( ยท๐‘  โ€˜ ndx ) , { โŸจ โŸจ ๐‘ง , ๐‘– โŸฉ , ๐‘– โŸฉ } โŸฉ } ) โˆˆ LMod โˆง ยฌ ( { โŸจ ( Base โ€˜ ndx ) , { ๐‘– } โŸฉ , โŸจ ( +g โ€˜ ndx ) , { โŸจ โŸจ ๐‘– , ๐‘– โŸฉ , ๐‘– โŸฉ } โŸฉ , โŸจ ( Scalar โ€˜ ndx ) , { โŸจ ( Base โ€˜ ndx ) , { ๐‘ง } โŸฉ , โŸจ ( +g โ€˜ ndx ) , { โŸจ โŸจ ๐‘ง , ๐‘ง โŸฉ , ๐‘ง โŸฉ } โŸฉ , โŸจ ( .r โ€˜ ndx ) , { โŸจ โŸจ ๐‘ง , ๐‘ง โŸฉ , ๐‘ง โŸฉ } โŸฉ } โŸฉ } โˆช { โŸจ ( ยท๐‘  โ€˜ ndx ) , { โŸจ โŸจ ๐‘ง , ๐‘– โŸฉ , ๐‘– โŸฉ } โŸฉ } ) โˆˆ LVec ) โ†’ LVec โ‰  LMod )
15 5 12 14 mp2b โŠข LVec โ‰  LMod
16 df-pss โŠข ( LVec โŠŠ LMod โ†” ( LVec โŠ† LMod โˆง LVec โ‰  LMod ) )
17 2 15 16 mpbir2an โŠข LVec โŠŠ LMod