Theorem cvsunit

Description: Unit group of the scalar ring of a subcomplex vector space. (Contributed by Thierry Arnoux, 22-May-2019)

	Ref	Expression
Hypotheses	cvsdiv.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	cvsdiv.k	$$⊢K={\mathrm{Base}}_F$$
Assertion	cvsunit	$$⊢W\in \mathrm{ℂVec}\to K\setminus \left\{0\right\}=\mathrm{Unit}\left(F\right)$$

Proof

Step	Hyp	Ref	Expression
1		cvsdiv.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
2		cvsdiv.k	$$⊢K={\mathrm{Base}}_F$$
3		id	$$⊢W\in \mathrm{ℂVec}\to W\in \mathrm{ℂVec}$$
4	3	cvsclm	$$⊢W\in \mathrm{ℂVec}\to W\in \mathrm{CMod}$$
5	1	clm0	$$⊢W\in \mathrm{CMod}\to 0=0_F$$
6	4 5	syl	$$⊢W\in \mathrm{ℂVec}\to 0=0_F$$
7	6	sneqd	$$⊢W\in \mathrm{ℂVec}\to \left\{0\right\}=\left\{0_F\right\}$$
8	7	difeq2d	$$⊢W\in \mathrm{ℂVec}\to K\setminus \left\{0\right\}=K\setminus \left\{0_F\right\}$$
9	3	cvslvec	$$⊢W\in \mathrm{ℂVec}\to W\in \mathrm{LVec}$$
10	1	lvecdrng	$$⊢W\in \mathrm{LVec}\to F\in \mathrm{DivRing}$$
11		eqid	$$⊢\mathrm{Unit}\left(F\right)=\mathrm{Unit}\left(F\right)$$
12		eqid	$$⊢0_F=0_F$$
13	2 11 12	isdrng	$$⊢F\in \mathrm{DivRing}\leftrightarrow \left(F\in \mathrm{Ring}\wedge \mathrm{Unit}\left(F\right)=K\setminus \left\{0_F\right\}\right)$$
14	13	simprbi	$$⊢F\in \mathrm{DivRing}\to \mathrm{Unit}\left(F\right)=K\setminus \left\{0_F\right\}$$
15	9 10 14	3syl	$$⊢W\in \mathrm{ℂVec}\to \mathrm{Unit}\left(F\right)=K\setminus \left\{0_F\right\}$$
16	8 15	eqtr4d	$$⊢W\in \mathrm{ℂVec}\to K\setminus \left\{0\right\}=\mathrm{Unit}\left(F\right)$$