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 F=ScalarW
cvsdiv.k K=BaseF
Assertion cvsunit WℂVecK0=UnitF

Proof

Step Hyp Ref Expression
1 cvsdiv.f F=ScalarW
2 cvsdiv.k K=BaseF
3 id WℂVecWℂVec
4 3 cvsclm WℂVecWCMod
5 1 clm0 WCMod0=0F
6 4 5 syl WℂVec0=0F
7 6 sneqd WℂVec0=0F
8 7 difeq2d WℂVecK0=K0F
9 3 cvslvec WℂVecWLVec
10 1 lvecdrng WLVecFDivRing
11 eqid UnitF=UnitF
12 eqid 0F=0F
13 2 11 12 isdrng FDivRingFRingUnitF=K0F
14 13 simprbi FDivRingUnitF=K0F
15 9 10 14 3syl WℂVecUnitF=K0F
16 8 15 eqtr4d WℂVecK0=UnitF