cvsunit

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

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

Metamath Proof Explorer