Description: An equality involving ratios in a subcomplex vector space. (Contributed by Thierry Arnoux, 22-May-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cvsdiveqd.v | |
|
cvsdiveqd.t | |
||
cvsdiveqd.f | |
||
cvsdiveqd.k | |
||
cvsdiveqd.w | |
||
cvsdiveqd.a | |
||
cvsdiveqd.b | |
||
cvsdiveqd.x | |
||
cvsdiveqd.y | |
||
cvsdiveqd.1 | |
||
cvsmuleqdivd.1 | |
||
Assertion | cvsmuleqdivd | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cvsdiveqd.v | |
|
2 | cvsdiveqd.t | |
|
3 | cvsdiveqd.f | |
|
4 | cvsdiveqd.k | |
|
5 | cvsdiveqd.w | |
|
6 | cvsdiveqd.a | |
|
7 | cvsdiveqd.b | |
|
8 | cvsdiveqd.x | |
|
9 | cvsdiveqd.y | |
|
10 | cvsdiveqd.1 | |
|
11 | cvsmuleqdivd.1 | |
|
12 | 11 | oveq2d | |
13 | 5 | cvsclm | |
14 | 3 4 | clmsscn | |
15 | 13 14 | syl | |
16 | 15 6 | sseldd | |
17 | 16 10 | recid2d | |
18 | 17 | oveq1d | |
19 | 3 | clm1 | |
20 | 13 19 | syl | |
21 | 3 | clmring | |
22 | eqid | |
|
23 | 4 22 | ringidcl | |
24 | 13 21 23 | 3syl | |
25 | 20 24 | eqeltrd | |
26 | 3 4 | cvsdivcl | |
27 | 5 25 6 10 26 | syl13anc | |
28 | 1 3 2 4 | clmvsass | |
29 | 13 27 6 8 28 | syl13anc | |
30 | 1 2 | clmvs1 | |
31 | 13 8 30 | syl2anc | |
32 | 18 29 31 | 3eqtr3d | |
33 | 15 7 | sseldd | |
34 | 33 16 10 | divrec2d | |
35 | 34 | oveq1d | |
36 | 1 3 2 4 | clmvsass | |
37 | 13 27 7 9 36 | syl13anc | |
38 | 35 37 | eqtr2d | |
39 | 12 32 38 | 3eqtr3d | |