This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝐹 ) )