Metamath Proof Explorer


Theorem lmod1zrnlvec

Description: There is a (left) module (azero module) which is not a (left) vector space. (Contributed by AV, 29-Apr-2019)

Ref Expression
Hypotheses lmod1zr.r R=BasendxZ+ndxZZZndxZZZ
lmod1zr.m M=BasendxI+ndxIIIScalarndxRndxZII
Assertion lmod1zrnlvec IVZWMLVec

Proof

Step Hyp Ref Expression
1 lmod1zr.r R=BasendxZ+ndxZZZndxZZZ
2 lmod1zr.m M=BasendxI+ndxIIIScalarndxRndxZII
3 tpex BasendxZ+ndxZZZndxZZZV
4 1 3 eqeltri RV
5 2 lmodsca RVR=ScalarM
6 4 5 mp1i IVZWR=ScalarM
7 1 rng1nnzr ZWRNzRing
8 df-nel RNzRing¬RNzRing
9 7 8 sylib ZW¬RNzRing
10 drngnzr RDivRingRNzRing
11 9 10 nsyl ZW¬RDivRing
12 11 adantl IVZW¬RDivRing
13 6 12 eqneltrrd IVZW¬ScalarMDivRing
14 13 intnand IVZW¬MLModScalarMDivRing
15 df-nel MLVec¬MLVec
16 eqid ScalarM=ScalarM
17 16 islvec MLVecMLModScalarMDivRing
18 15 17 xchbinx MLVec¬MLModScalarMDivRing
19 14 18 sylibr IVZWMLVec