Metamath Proof Explorer

Theorem lmodn0

Description: Left modules exist. (Contributed by AV, 29-Apr-2019)

Ref Expression
Assertion lmodn0 
|- LMod =/= (/)

Proof

Step Hyp Ref Expression
1 vex 
 |-  i e. _V
2 vex 
 |-  z e. _V
3 1 2 pm3.2i 
 |-  ( i e. _V /\ z e. _V )
4 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 >. } >. }
5 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 >. } >. } )
6 4 5 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 )
7 ne0i 
 |-  ( ( { <. ( 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 -> LMod =/= (/) )
8 3 6 7 mp2b 
 |-  LMod =/= (/)