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\}⟩, ⟨+_{ndx}, \{⟨⟨Z, Z⟩, Z⟩\}⟩, ⟨\cdot_{ndx}, \{⟨⟨Z, Z⟩, Z⟩\}⟩\}$
	lmod1zr.m	$⊢ M = \{⟨{Base}_{ndx}, \{I\}⟩, ⟨+_{ndx}, \{⟨⟨I, I⟩, I⟩\}⟩, ⟨Scalar (ndx), R⟩\} \cup \{⟨\cdot_{ndx}, \{⟨⟨Z, I⟩, I⟩\}⟩\}$
Assertion	lmod1zrnlvec	$⊢ (I \in V \land Z \in W) \to M \notin LVec$

Step	Hyp	Ref	Expression
1		lmod1zr.r	$⊢ R = \{⟨{Base}_{ndx}, \{Z\}⟩, ⟨+_{ndx}, \{⟨⟨Z, Z⟩, Z⟩\}⟩, ⟨\cdot_{ndx}, \{⟨⟨Z, Z⟩, Z⟩\}⟩\}$
2		lmod1zr.m	$⊢ M = \{⟨{Base}_{ndx}, \{I\}⟩, ⟨+_{ndx}, \{⟨⟨I, I⟩, I⟩\}⟩, ⟨Scalar (ndx), R⟩\} \cup \{⟨\cdot_{ndx}, \{⟨⟨Z, I⟩, I⟩\}⟩\}$
3		tpex	$⊢ \{⟨{Base}_{ndx}, \{Z\}⟩, ⟨+_{ndx}, \{⟨⟨Z, Z⟩, Z⟩\}⟩, ⟨\cdot_{ndx}, \{⟨⟨Z, Z⟩, Z⟩\}⟩\} \in V$
4	1 3	eqeltri	$⊢ R \in V$
5	2	lmodsca	$⊢ R \in V \to R = Scalar (M)$
6	4 5	mp1i	$⊢ (I \in V \land Z \in W) \to R = Scalar (M)$
7	1	rng1nnzr	$⊢ Z \in W \to R \notin NzRing$
8		df-nel	$⊢ R \notin NzRing \leftrightarrow \neg R \in NzRing$
9	7 8	sylib	$⊢ Z \in W \to \neg R \in NzRing$
10		drngnzr	$⊢ R \in DivRing \to R \in NzRing$
11	9 10	nsyl	$⊢ Z \in W \to \neg R \in DivRing$
12	11	adantl	$⊢ (I \in V \land Z \in W) \to \neg R \in DivRing$
13	6 12	eqneltrrd	$⊢ (I \in V \land Z \in W) \to \neg Scalar (M) \in DivRing$
14	13	intnand	$⊢ (I \in V \land Z \in W) \to \neg (M \in LMod \land Scalar (M) \in DivRing)$
15		df-nel	$⊢ M \notin LVec \leftrightarrow \neg M \in LVec$
16		eqid	$⊢ Scalar (M) = Scalar (M)$
17	16	islvec	$⊢ M \in LVec \leftrightarrow (M \in LMod \land Scalar (M) \in DivRing)$
18	15 17	xchbinx	$⊢ M \notin LVec \leftrightarrow \neg (M \in LMod \land Scalar (M) \in DivRing)$
19	14 18	sylibr	$⊢ (I \in V \land Z \in W) \to M \notin LVec$

Metamath Proof Explorer