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 = ( Scalar ` W )
	cvsdiv.k	|- K = ( Base ` F )
Assertion	cvsunit	|- ( W e. CVec -> ( K \ { 0 } ) = ( Unit ` F ) )

Proof

Step	Hyp	Ref	Expression
1		cvsdiv.f	|- F = ( Scalar ` W )
2		cvsdiv.k	|- K = ( Base ` F )
3		id	|- ( W e. CVec -> W e. CVec )
4	3	cvsclm	|- ( W e. CVec -> W e. CMod )
5	1	clm0	|- ( W e. CMod -> 0 = ( 0g ` F ) )
6	4 5	syl	|- ( W e. CVec -> 0 = ( 0g ` F ) )
7	6	sneqd	|- ( W e. CVec -> { 0 } = { ( 0g ` F ) } )
8	7	difeq2d	|- ( W e. CVec -> ( K \ { 0 } ) = ( K \ { ( 0g ` F ) } ) )
9	3	cvslvec	|- ( W e. CVec -> W e. LVec )
10	1	lvecdrng	|- ( W e. LVec -> F e. DivRing )
11		eqid	|- ( Unit ` F ) = ( Unit ` F )
12		eqid	|- ( 0g ` F ) = ( 0g ` F )
13	2 11 12	isdrng	|- ( F e. DivRing <-> ( F e. Ring /\ ( Unit ` F ) = ( K \ { ( 0g ` F ) } ) ) )
14	13	simprbi	|- ( F e. DivRing -> ( Unit ` F ) = ( K \ { ( 0g ` F ) } ) )
15	9 10 14	3syl	|- ( W e. CVec -> ( Unit ` F ) = ( K \ { ( 0g ` F ) } ) )
16	8 15	eqtr4d	|- ( W e. CVec -> ( K \ { 0 } ) = ( Unit ` F ) )