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 = ( Base ` W )
cvsdiveqd.t 
|- .x. = ( .s ` W )
cvsdiveqd.f 
|- F = ( Scalar ` W )
cvsdiveqd.k 
|- K = ( Base ` F )
cvsdiveqd.w 
|- ( ph -> W e. CVec )
cvsdiveqd.a 
|- ( ph -> A e. K )
cvsdiveqd.b 
|- ( ph -> B e. K )
cvsdiveqd.x 
|- ( ph -> X e. V )
cvsdiveqd.y 
|- ( ph -> Y e. V )
cvsdiveqd.1 
|- ( ph -> A =/= 0 )
cvsmuleqdivd.1 
|- ( ph -> ( A .x. X ) = ( B .x. Y ) )
Assertion cvsmuleqdivd 
|- ( ph -> X = ( ( B / A ) .x. Y ) )

Proof

Step Hyp Ref Expression
1 cvsdiveqd.v 
 |-  V = ( Base ` W )
2 cvsdiveqd.t 
 |-  .x. = ( .s ` W )
3 cvsdiveqd.f 
 |-  F = ( Scalar ` W )
4 cvsdiveqd.k 
 |-  K = ( Base ` F )
5 cvsdiveqd.w 
 |-  ( ph -> W e. CVec )
6 cvsdiveqd.a 
 |-  ( ph -> A e. K )
7 cvsdiveqd.b 
 |-  ( ph -> B e. K )
8 cvsdiveqd.x 
 |-  ( ph -> X e. V )
9 cvsdiveqd.y 
 |-  ( ph -> Y e. V )
10 cvsdiveqd.1 
 |-  ( ph -> A =/= 0 )
11 cvsmuleqdivd.1 
 |-  ( ph -> ( A .x. X ) = ( B .x. Y ) )
12 11 oveq2d 
 |-  ( ph -> ( ( 1 / A ) .x. ( A .x. X ) ) = ( ( 1 / A ) .x. ( B .x. Y ) ) )
13 5 cvsclm 
 |-  ( ph -> W e. CMod )
14 3 4 clmsscn 
 |-  ( W e. CMod -> K C_ CC )
15 13 14 syl 
 |-  ( ph -> K C_ CC )
16 15 6 sseldd 
 |-  ( ph -> A e. CC )
17 16 10 recid2d 
 |-  ( ph -> ( ( 1 / A ) x. A ) = 1 )
18 17 oveq1d 
 |-  ( ph -> ( ( ( 1 / A ) x. A ) .x. X ) = ( 1 .x. X ) )
19 3 clm1 
 |-  ( W e. CMod -> 1 = ( 1r ` F ) )
20 13 19 syl 
 |-  ( ph -> 1 = ( 1r ` F ) )
21 3 clmring 
 |-  ( W e. CMod -> F e. Ring )
22 eqid 
 |-  ( 1r ` F ) = ( 1r ` F )
23 4 22 ringidcl 
 |-  ( F e. Ring -> ( 1r ` F ) e. K )
24 13 21 23 3syl 
 |-  ( ph -> ( 1r ` F ) e. K )
25 20 24 eqeltrd 
 |-  ( ph -> 1 e. K )
26 3 4 cvsdivcl 
 |-  ( ( W e. CVec /\ ( 1 e. K /\ A e. K /\ A =/= 0 ) ) -> ( 1 / A ) e. K )
27 5 25 6 10 26 syl13anc 
 |-  ( ph -> ( 1 / A ) e. K )
28 1 3 2 4 clmvsass 
 |-  ( ( W e. CMod /\ ( ( 1 / A ) e. K /\ A e. K /\ X e. V ) ) -> ( ( ( 1 / A ) x. A ) .x. X ) = ( ( 1 / A ) .x. ( A .x. X ) ) )
29 13 27 6 8 28 syl13anc 
 |-  ( ph -> ( ( ( 1 / A ) x. A ) .x. X ) = ( ( 1 / A ) .x. ( A .x. X ) ) )
30 1 2 clmvs1 
 |-  ( ( W e. CMod /\ X e. V ) -> ( 1 .x. X ) = X )
31 13 8 30 syl2anc 
 |-  ( ph -> ( 1 .x. X ) = X )
32 18 29 31 3eqtr3d 
 |-  ( ph -> ( ( 1 / A ) .x. ( A .x. X ) ) = X )
33 15 7 sseldd 
 |-  ( ph -> B e. CC )
34 33 16 10 divrec2d 
 |-  ( ph -> ( B / A ) = ( ( 1 / A ) x. B ) )
35 34 oveq1d 
 |-  ( ph -> ( ( B / A ) .x. Y ) = ( ( ( 1 / A ) x. B ) .x. Y ) )
36 1 3 2 4 clmvsass 
 |-  ( ( W e. CMod /\ ( ( 1 / A ) e. K /\ B e. K /\ Y e. V ) ) -> ( ( ( 1 / A ) x. B ) .x. Y ) = ( ( 1 / A ) .x. ( B .x. Y ) ) )
37 13 27 7 9 36 syl13anc 
 |-  ( ph -> ( ( ( 1 / A ) x. B ) .x. Y ) = ( ( 1 / A ) .x. ( B .x. Y ) ) )
38 35 37 eqtr2d 
 |-  ( ph -> ( ( 1 / A ) .x. ( B .x. Y ) ) = ( ( B / A ) .x. Y ) )
39 12 32 38 3eqtr3d 
 |-  ( ph -> X = ( ( B / A ) .x. Y ) )