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 |