Description: Unit group of the scalar ring of a subcomplex vector space. (Contributed by Thierry Arnoux, 22-May-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cvsdiv.f | |
|
cvsdiv.k | |
||
Assertion | cvsunit | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cvsdiv.f | |
|
2 | cvsdiv.k | |
|
3 | id | |
|
4 | 3 | cvsclm | |
5 | 1 | clm0 | |
6 | 4 5 | syl | |
7 | 6 | sneqd | |
8 | 7 | difeq2d | |
9 | 3 | cvslvec | |
10 | 1 | lvecdrng | |
11 | eqid | |
|
12 | eqid | |
|
13 | 2 11 12 | isdrng | |
14 | 13 | simprbi | |
15 | 9 10 14 | 3syl | |
16 | 8 15 | eqtr4d | |