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 = { <. ( Base ` ndx ) , { Z } >. , <. ( +g ` ndx ) , { <. <. Z , Z >. , Z >. } >. , <. ( .r ` ndx ) , { <. <. Z , Z >. , Z >. } >. }
	lmod1zr.m	|- M = ( { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. , <. ( Scalar ` ndx ) , R >. } u. { <. ( .s ` ndx ) , { <. <. Z , I >. , I >. } >. } )
Assertion	lmod1zrnlvec	|- ( ( I e. V /\ Z e. W ) -> M e/ LVec )

Proof

Step	Hyp	Ref	Expression
1		lmod1zr.r	|- R = { <. ( Base ` ndx ) , { Z } >. , <. ( +g ` ndx ) , { <. <. Z , Z >. , Z >. } >. , <. ( .r ` ndx ) , { <. <. Z , Z >. , Z >. } >. }
2		lmod1zr.m	|- M = ( { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. , <. ( Scalar ` ndx ) , R >. } u. { <. ( .s ` ndx ) , { <. <. Z , I >. , I >. } >. } )
3		tpex	|- { <. ( Base ` ndx ) , { Z } >. , <. ( +g ` ndx ) , { <. <. Z , Z >. , Z >. } >. , <. ( .r ` ndx ) , { <. <. Z , Z >. , Z >. } >. } e. _V
4	1 3	eqeltri	|- R e. _V
5	2	lmodsca	|- ( R e. _V -> R = ( Scalar ` M ) )
6	4 5	mp1i	|- ( ( I e. V /\ Z e. W ) -> R = ( Scalar ` M ) )
7	1	rng1nnzr	|- ( Z e. W -> R e/ NzRing )
8		df-nel	|- ( R e/ NzRing <-> -. R e. NzRing )
9	7 8	sylib	|- ( Z e. W -> -. R e. NzRing )
10		drngnzr	|- ( R e. DivRing -> R e. NzRing )
11	9 10	nsyl	|- ( Z e. W -> -. R e. DivRing )
12	11	adantl	|- ( ( I e. V /\ Z e. W ) -> -. R e. DivRing )
13	6 12	eqneltrrd	|- ( ( I e. V /\ Z e. W ) -> -. ( Scalar ` M ) e. DivRing )
14	13	intnand	|- ( ( I e. V /\ Z e. W ) -> -. ( M e. LMod /\ ( Scalar ` M ) e. DivRing ) )
15		df-nel	|- ( M e/ LVec <-> -. M e. LVec )
16		eqid	|- ( Scalar ` M ) = ( Scalar ` M )
17	16	islvec	|- ( M e. LVec <-> ( M e. LMod /\ ( Scalar ` M ) e. DivRing ) )
18	15 17	xchbinx	|- ( M e/ LVec <-> -. ( M e. LMod /\ ( Scalar ` M ) e. DivRing ) )
19	14 18	sylibr	|- ( ( I e. V /\ Z e. W ) -> M e/ LVec )