Theorem zclmncvs

Description: The ring of integers as left module over itself is a subcomplex module, but not a subcomplex vector space. The vector operation is + , and the scalar product is x. . (Contributed by AV, 22-Oct-2021)

	Ref	Expression
Hypothesis	zclmncvs.z	$$⊢Z=\mathrm{ringLMod}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
Assertion	zclmncvs	$$⊢\left(Z\in \mathrm{CMod}\wedge Z\notin \mathrm{ℂVec}\right)$$

Proof

Step	Hyp	Ref	Expression
1		zclmncvs.z	$$⊢Z=\mathrm{ringLMod}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
2		zringring	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Ring}$$
3		rlmlmod	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Ring}\to \mathrm{ringLMod}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\in \mathrm{LMod}$$
4	2 3	ax-mp	$$⊢\mathrm{ringLMod}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\in \mathrm{LMod}$$
5		rlmsca	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Ring}\to {\mathbb{Z}}_{\mathrm{ring}}=\mathrm{Scalar}\left(\mathrm{ringLMod}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\right)$$
6	2 5	ax-mp	$$⊢{\mathbb{Z}}_{\mathrm{ring}}=\mathrm{Scalar}\left(\mathrm{ringLMod}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\right)$$
7		df-zring	$$⊢{\mathbb{Z}}_{\mathrm{ring}}={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Z}$$
8	6 7	eqtr3i	$$⊢\mathrm{Scalar}\left(\mathrm{ringLMod}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\right)={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Z}$$
9		zsubrg	$$⊢\mathbb{Z}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$
10		eqid	$$⊢\mathrm{Scalar}\left(\mathrm{ringLMod}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\right)=\mathrm{Scalar}\left(\mathrm{ringLMod}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\right)$$
11	10	isclmi	$$⊢\left(\mathrm{ringLMod}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\in \mathrm{LMod}\wedge \mathrm{Scalar}\left(\mathrm{ringLMod}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\right)={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Z}\wedge \mathbb{Z}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\right)\to \mathrm{ringLMod}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\in \mathrm{CMod}$$
12	4 8 9 11	mp3an	$$⊢\mathrm{ringLMod}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\in \mathrm{CMod}$$
13	1	eleq1i	$$⊢Z\in \mathrm{CMod}\leftrightarrow \mathrm{ringLMod}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\in \mathrm{CMod}$$
14	12 13	mpbir	$$⊢Z\in \mathrm{CMod}$$
15		zringndrg	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\notin \mathrm{DivRing}$$
16	15	neli	$$⊢\neg {\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{DivRing}$$
17	5	eqcomd	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Ring}\to \mathrm{Scalar}\left(\mathrm{ringLMod}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\right)={\mathbb{Z}}_{\mathrm{ring}}$$
18	2 17	ax-mp	$$⊢\mathrm{Scalar}\left(\mathrm{ringLMod}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\right)={\mathbb{Z}}_{\mathrm{ring}}$$
19	18	eleq1i	$$⊢\mathrm{Scalar}\left(\mathrm{ringLMod}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\right)\in \mathrm{DivRing}\leftrightarrow {\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{DivRing}$$
20	16 19	mtbir	$$⊢\neg \mathrm{Scalar}\left(\mathrm{ringLMod}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\right)\in \mathrm{DivRing}$$
21	20	intnan	$$⊢\neg \left(\mathrm{ringLMod}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\in \mathrm{LMod}\wedge \mathrm{Scalar}\left(\mathrm{ringLMod}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\right)\in \mathrm{DivRing}\right)$$
22	10	islvec	$$⊢\mathrm{ringLMod}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\in \mathrm{LVec}\leftrightarrow \left(\mathrm{ringLMod}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\in \mathrm{LMod}\wedge \mathrm{Scalar}\left(\mathrm{ringLMod}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\right)\in \mathrm{DivRing}\right)$$
23	21 22	mtbir	$$⊢\neg \mathrm{ringLMod}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\in \mathrm{LVec}$$
24	23	olci	$$⊢\left(\neg \mathrm{ringLMod}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\in \mathrm{CMod}\vee \neg \mathrm{ringLMod}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\in \mathrm{LVec}\right)$$
25		df-nel	$$⊢Z\notin \mathrm{ℂVec}\leftrightarrow \neg Z\in \mathrm{ℂVec}$$
26		ianor	$$⊢\neg \left(\mathrm{ringLMod}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\in \mathrm{CMod}\wedge \mathrm{ringLMod}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\in \mathrm{LVec}\right)\leftrightarrow \left(\neg \mathrm{ringLMod}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\in \mathrm{CMod}\vee \neg \mathrm{ringLMod}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\in \mathrm{LVec}\right)$$
27		elin	$$⊢\mathrm{ringLMod}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\in \left(\mathrm{CMod}\cap \mathrm{LVec}\right)\leftrightarrow \left(\mathrm{ringLMod}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\in \mathrm{CMod}\wedge \mathrm{ringLMod}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\in \mathrm{LVec}\right)$$
28	26 27	xchnxbir	$$⊢\neg \mathrm{ringLMod}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\in \left(\mathrm{CMod}\cap \mathrm{LVec}\right)\leftrightarrow \left(\neg \mathrm{ringLMod}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\in \mathrm{CMod}\vee \neg \mathrm{ringLMod}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\in \mathrm{LVec}\right)$$
29		df-cvs	$$⊢\mathrm{ℂVec}=\mathrm{CMod}\cap \mathrm{LVec}$$
30	1 29	eleq12i	$$⊢Z\in \mathrm{ℂVec}\leftrightarrow \mathrm{ringLMod}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\in \left(\mathrm{CMod}\cap \mathrm{LVec}\right)$$
31	28 30	xchnxbir	$$⊢\neg Z\in \mathrm{ℂVec}\leftrightarrow \left(\neg \mathrm{ringLMod}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\in \mathrm{CMod}\vee \neg \mathrm{ringLMod}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\in \mathrm{LVec}\right)$$
32	25 31	bitri	$$⊢Z\notin \mathrm{ℂVec}\leftrightarrow \left(\neg \mathrm{ringLMod}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\in \mathrm{CMod}\vee \neg \mathrm{ringLMod}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\in \mathrm{LVec}\right)$$
33	24 32	mpbir	$$⊢Z\notin \mathrm{ℂVec}$$
34	14 33	pm3.2i	$$⊢\left(Z\in \mathrm{CMod}\wedge Z\notin \mathrm{ℂVec}\right)$$