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	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	cvsdiv.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
Assertion	cvsunit	⊢ ( 𝑊 ∈ ℂVec → ( 𝐾 ∖ { 0 } ) = ( Unit ‘ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		cvsdiv.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2		cvsdiv.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
3		id	⊢ ( 𝑊 ∈ ℂVec → 𝑊 ∈ ℂVec )
4	3	cvsclm	⊢ ( 𝑊 ∈ ℂVec → 𝑊 ∈ ℂMod )
5	1	clm0	⊢ ( 𝑊 ∈ ℂMod → 0 = ( 0g ‘ 𝐹 ) )
6	4 5	syl	⊢ ( 𝑊 ∈ ℂVec → 0 = ( 0g ‘ 𝐹 ) )
7	6	sneqd	⊢ ( 𝑊 ∈ ℂVec → { 0 } = { ( 0g ‘ 𝐹 ) } )
8	7	difeq2d	⊢ ( 𝑊 ∈ ℂVec → ( 𝐾 ∖ { 0 } ) = ( 𝐾 ∖ { ( 0g ‘ 𝐹 ) } ) )
9	3	cvslvec	⊢ ( 𝑊 ∈ ℂVec → 𝑊 ∈ LVec )
10	1	lvecdrng	⊢ ( 𝑊 ∈ LVec → 𝐹 ∈ DivRing )
11		eqid	⊢ ( Unit ‘ 𝐹 ) = ( Unit ‘ 𝐹 )
12		eqid	⊢ ( 0g ‘ 𝐹 ) = ( 0g ‘ 𝐹 )
13	2 11 12	isdrng	⊢ ( 𝐹 ∈ DivRing ↔ ( 𝐹 ∈ Ring ∧ ( Unit ‘ 𝐹 ) = ( 𝐾 ∖ { ( 0g ‘ 𝐹 ) } ) ) )
14	13	simprbi	⊢ ( 𝐹 ∈ DivRing → ( Unit ‘ 𝐹 ) = ( 𝐾 ∖ { ( 0g ‘ 𝐹 ) } ) )
15	9 10 14	3syl	⊢ ( 𝑊 ∈ ℂVec → ( Unit ‘ 𝐹 ) = ( 𝐾 ∖ { ( 0g ‘ 𝐹 ) } ) )
16	8 15	eqtr4d	⊢ ( 𝑊 ∈ ℂVec → ( 𝐾 ∖ { 0 } ) = ( Unit ‘ 𝐹 ) )