Theorem lvecpsslmod

Description: The class of all (left) vector spaces is a proper subclass of the class of all (left) modules. Although it is obvious (and proven by lveclmod ) that every left vector space is a left module, there is (at least) one left module which is no left vector space, for example the zero module over the zero ring, see lmod1zrnlvec . (Contributed by AV, 29-Apr-2019)

	Ref	Expression
Assertion	lvecpsslmod	$$⊢\mathrm{LVec}\subset \mathrm{LMod}$$

Proof

Step	Hyp	Ref	Expression
1		lveclmod	$$⊢v\in \mathrm{LVec}\to v\in \mathrm{LMod}$$
2	1	ssriv	$$⊢\mathrm{LVec}\subseteq \mathrm{LMod}$$
3		vex	$$⊢i\in \mathrm{V}$$
4		vex	$$⊢z\in \mathrm{V}$$
5	3 4	pm3.2i	$$⊢\left(i\in \mathrm{V}\wedge z\in \mathrm{V}\right)$$
6		eqid	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{z\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨z,z⟩,z⟩\right\}⟩,⟨{\cdot }_{\mathrm{ndx}},\left\{⟨⟨z,z⟩,z⟩\right\}⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{z\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨z,z⟩,z⟩\right\}⟩,⟨{\cdot }_{\mathrm{ndx}},\left\{⟨⟨z,z⟩,z⟩\right\}⟩\right\}$$
7		eqid	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{i\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨i,i⟩,i⟩\right\}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{z\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨z,z⟩,z⟩\right\}⟩,⟨{\cdot }_{\mathrm{ndx}},\left\{⟨⟨z,z⟩,z⟩\right\}⟩\right\}⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},\left\{⟨⟨z,i⟩,i⟩\right\}⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{i\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨i,i⟩,i⟩\right\}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{z\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨z,z⟩,z⟩\right\}⟩,⟨{\cdot }_{\mathrm{ndx}},\left\{⟨⟨z,z⟩,z⟩\right\}⟩\right\}⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},\left\{⟨⟨z,i⟩,i⟩\right\}⟩\right\}$$
8	6 7	lmod1zr	$$⊢\left(i\in \mathrm{V}\wedge z\in \mathrm{V}\right)\to \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{i\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨i,i⟩,i⟩\right\}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{z\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨z,z⟩,z⟩\right\}⟩,⟨{\cdot }_{\mathrm{ndx}},\left\{⟨⟨z,z⟩,z⟩\right\}⟩\right\}⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},\left\{⟨⟨z,i⟩,i⟩\right\}⟩\right\}\in \mathrm{LMod}$$
9	6 7	lmod1zrnlvec	$$⊢\left(i\in \mathrm{V}\wedge z\in \mathrm{V}\right)\to \left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{i\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨i,i⟩,i⟩\right\}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{z\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨z,z⟩,z⟩\right\}⟩,⟨{\cdot }_{\mathrm{ndx}},\left\{⟨⟨z,z⟩,z⟩\right\}⟩\right\}⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},\left\{⟨⟨z,i⟩,i⟩\right\}⟩\right\}\right)\notin \mathrm{LVec}$$
10		df-nel	$$⊢\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{i\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨i,i⟩,i⟩\right\}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{z\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨z,z⟩,z⟩\right\}⟩,⟨{\cdot }_{\mathrm{ndx}},\left\{⟨⟨z,z⟩,z⟩\right\}⟩\right\}⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},\left\{⟨⟨z,i⟩,i⟩\right\}⟩\right\}\right)\notin \mathrm{LVec}\leftrightarrow \neg \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{i\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨i,i⟩,i⟩\right\}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{z\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨z,z⟩,z⟩\right\}⟩,⟨{\cdot }_{\mathrm{ndx}},\left\{⟨⟨z,z⟩,z⟩\right\}⟩\right\}⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},\left\{⟨⟨z,i⟩,i⟩\right\}⟩\right\}\in \mathrm{LVec}$$
11	9 10	sylib	$$⊢\left(i\in \mathrm{V}\wedge z\in \mathrm{V}\right)\to \neg \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{i\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨i,i⟩,i⟩\right\}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{z\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨z,z⟩,z⟩\right\}⟩,⟨{\cdot }_{\mathrm{ndx}},\left\{⟨⟨z,z⟩,z⟩\right\}⟩\right\}⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},\left\{⟨⟨z,i⟩,i⟩\right\}⟩\right\}\in \mathrm{LVec}$$
12	8 11	jca	$$⊢\left(i\in \mathrm{V}\wedge z\in \mathrm{V}\right)\to \left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{i\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨i,i⟩,i⟩\right\}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{z\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨z,z⟩,z⟩\right\}⟩,⟨{\cdot }_{\mathrm{ndx}},\left\{⟨⟨z,z⟩,z⟩\right\}⟩\right\}⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},\left\{⟨⟨z,i⟩,i⟩\right\}⟩\right\}\in \mathrm{LMod}\wedge \neg \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{i\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨i,i⟩,i⟩\right\}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{z\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨z,z⟩,z⟩\right\}⟩,⟨{\cdot }_{\mathrm{ndx}},\left\{⟨⟨z,z⟩,z⟩\right\}⟩\right\}⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},\left\{⟨⟨z,i⟩,i⟩\right\}⟩\right\}\in \mathrm{LVec}\right)$$
13		nelne1	$$⊢\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{i\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨i,i⟩,i⟩\right\}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{z\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨z,z⟩,z⟩\right\}⟩,⟨{\cdot }_{\mathrm{ndx}},\left\{⟨⟨z,z⟩,z⟩\right\}⟩\right\}⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},\left\{⟨⟨z,i⟩,i⟩\right\}⟩\right\}\in \mathrm{LMod}\wedge \neg \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{i\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨i,i⟩,i⟩\right\}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{z\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨z,z⟩,z⟩\right\}⟩,⟨{\cdot }_{\mathrm{ndx}},\left\{⟨⟨z,z⟩,z⟩\right\}⟩\right\}⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},\left\{⟨⟨z,i⟩,i⟩\right\}⟩\right\}\in \mathrm{LVec}\right)\to \mathrm{LMod}\ne \mathrm{LVec}$$
14	13	necomd	$$⊢\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{i\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨i,i⟩,i⟩\right\}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{z\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨z,z⟩,z⟩\right\}⟩,⟨{\cdot }_{\mathrm{ndx}},\left\{⟨⟨z,z⟩,z⟩\right\}⟩\right\}⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},\left\{⟨⟨z,i⟩,i⟩\right\}⟩\right\}\in \mathrm{LMod}\wedge \neg \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{i\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨i,i⟩,i⟩\right\}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{z\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨z,z⟩,z⟩\right\}⟩,⟨{\cdot }_{\mathrm{ndx}},\left\{⟨⟨z,z⟩,z⟩\right\}⟩\right\}⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},\left\{⟨⟨z,i⟩,i⟩\right\}⟩\right\}\in \mathrm{LVec}\right)\to \mathrm{LVec}\ne \mathrm{LMod}$$
15	5 12 14	mp2b	$$⊢\mathrm{LVec}\ne \mathrm{LMod}$$
16		df-pss	$$⊢\mathrm{LVec}\subset \mathrm{LMod}\leftrightarrow \left(\mathrm{LVec}\subseteq \mathrm{LMod}\wedge \mathrm{LVec}\ne \mathrm{LMod}\right)$$
17	2 15 16	mpbir2an	$$⊢\mathrm{LVec}\subset \mathrm{LMod}$$