Metamath Proof Explorer


Theorem cvsmuleqdivd

Description: An equality involving ratios in a subcomplex vector space. (Contributed by Thierry Arnoux, 22-May-2019)

Ref Expression
Hypotheses cvsdiveqd.v V=BaseW
cvsdiveqd.t ·˙=W
cvsdiveqd.f F=ScalarW
cvsdiveqd.k K=BaseF
cvsdiveqd.w φWℂVec
cvsdiveqd.a φAK
cvsdiveqd.b φBK
cvsdiveqd.x φXV
cvsdiveqd.y φYV
cvsdiveqd.1 φA0
cvsmuleqdivd.1 φA·˙X=B·˙Y
Assertion cvsmuleqdivd φX=BA·˙Y

Proof

Step Hyp Ref Expression
1 cvsdiveqd.v V=BaseW
2 cvsdiveqd.t ·˙=W
3 cvsdiveqd.f F=ScalarW
4 cvsdiveqd.k K=BaseF
5 cvsdiveqd.w φWℂVec
6 cvsdiveqd.a φAK
7 cvsdiveqd.b φBK
8 cvsdiveqd.x φXV
9 cvsdiveqd.y φYV
10 cvsdiveqd.1 φA0
11 cvsmuleqdivd.1 φA·˙X=B·˙Y
12 11 oveq2d φ1A·˙A·˙X=1A·˙B·˙Y
13 5 cvsclm φWCMod
14 3 4 clmsscn WCModK
15 13 14 syl φK
16 15 6 sseldd φA
17 16 10 recid2d φ1AA=1
18 17 oveq1d φ1AA·˙X=1·˙X
19 3 clm1 WCMod1=1F
20 13 19 syl φ1=1F
21 3 clmring WCModFRing
22 eqid 1F=1F
23 4 22 ringidcl FRing1FK
24 13 21 23 3syl φ1FK
25 20 24 eqeltrd φ1K
26 3 4 cvsdivcl WℂVec1KAKA01AK
27 5 25 6 10 26 syl13anc φ1AK
28 1 3 2 4 clmvsass WCMod1AKAKXV1AA·˙X=1A·˙A·˙X
29 13 27 6 8 28 syl13anc φ1AA·˙X=1A·˙A·˙X
30 1 2 clmvs1 WCModXV1·˙X=X
31 13 8 30 syl2anc φ1·˙X=X
32 18 29 31 3eqtr3d φ1A·˙A·˙X=X
33 15 7 sseldd φB
34 33 16 10 divrec2d φBA=1AB
35 34 oveq1d φBA·˙Y=1AB·˙Y
36 1 3 2 4 clmvsass WCMod1AKBKYV1AB·˙Y=1A·˙B·˙Y
37 13 27 7 9 36 syl13anc φ1AB·˙Y=1A·˙B·˙Y
38 35 37 eqtr2d φ1A·˙B·˙Y=BA·˙Y
39 12 32 38 3eqtr3d φX=BA·˙Y