This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cvsdiveqd

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 )
cvsdiveqd.2 
|- ( ph -> B =/= 0 )
cvsdiveqd.3 
|- ( ph -> X = ( ( A / B ) .x. Y ) )
Assertion cvsdiveqd 
|- ( ph -> ( ( B / A ) .x. 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 cvsdiveqd.2 
 |-  ( ph -> B =/= 0 )
12 cvsdiveqd.3 
 |-  ( ph -> X = ( ( A / B ) .x. Y ) )
13 12 oveq2d 
 |-  ( ph -> ( ( B / A ) .x. X ) = ( ( B / A ) .x. ( ( A / B ) .x. Y ) ) )
14 5 cvsclm 
 |-  ( ph -> W e. CMod )
15 3 4 clmsscn 
 |-  ( W e. CMod -> K C_ CC )
16 14 15 syl 
 |-  ( ph -> K C_ CC )
17 16 7 sseldd 
 |-  ( ph -> B e. CC )
18 16 6 sseldd 
 |-  ( ph -> A e. CC )
19 17 18 11 10 divcan6d 
 |-  ( ph -> ( ( B / A ) x. ( A / B ) ) = 1 )
20 19 oveq1d 
 |-  ( ph -> ( ( ( B / A ) x. ( A / B ) ) .x. Y ) = ( 1 .x. Y ) )
21 3 4 cvsdivcl 
 |-  ( ( W e. CVec /\ ( B e. K /\ A e. K /\ A =/= 0 ) ) -> ( B / A ) e. K )
22 5 7 6 10 21 syl13anc 
 |-  ( ph -> ( B / A ) e. K )
23 3 4 cvsdivcl 
 |-  ( ( W e. CVec /\ ( A e. K /\ B e. K /\ B =/= 0 ) ) -> ( A / B ) e. K )
24 5 6 7 11 23 syl13anc 
 |-  ( ph -> ( A / B ) e. K )
25 1 3 2 4 clmvsass 
 |-  ( ( W e. CMod /\ ( ( B / A ) e. K /\ ( A / B ) e. K /\ Y e. V ) ) -> ( ( ( B / A ) x. ( A / B ) ) .x. Y ) = ( ( B / A ) .x. ( ( A / B ) .x. Y ) ) )
26 14 22 24 9 25 syl13anc 
 |-  ( ph -> ( ( ( B / A ) x. ( A / B ) ) .x. Y ) = ( ( B / A ) .x. ( ( A / B ) .x. Y ) ) )
27 1 2 clmvs1 
 |-  ( ( W e. CMod /\ Y e. V ) -> ( 1 .x. Y ) = Y )
28 14 9 27 syl2anc 
 |-  ( ph -> ( 1 .x. Y ) = Y )
29 20 26 28 3eqtr3d 
 |-  ( ph -> ( ( B / A ) .x. ( ( A / B ) .x. Y ) ) = Y )
30 13 29 eqtrd 
 |-  ( ph -> ( ( B / A ) .x. X ) = Y )