Metamath Proof Explorer

Theorem bj-bary1lem1

Description: Lemma for bj-bary1: computation of one of the two barycentric coordinates of a barycenter of two points in one dimension (complex line). (Contributed by BJ, 6-Jun-2019)

Ref Expression
Hypotheses bj-bary1.a 
|- ( ph -> A e. CC )
bj-bary1.b 
|- ( ph -> B e. CC )
bj-bary1.x 
|- ( ph -> X e. CC )
bj-bary1.neq 
|- ( ph -> A =/= B )
bj-bary1.s 
|- ( ph -> S e. CC )
bj-bary1.t 
|- ( ph -> T e. CC )
Assertion bj-bary1lem1 
|- ( ph -> ( ( X = ( ( S x. A ) + ( T x. B ) ) /\ ( S + T ) = 1 ) -> T = ( ( X - A ) / ( B - A ) ) ) )

Proof

Step Hyp Ref Expression
1 bj-bary1.a 
 |-  ( ph -> A e. CC )
2 bj-bary1.b 
 |-  ( ph -> B e. CC )
3 bj-bary1.x 
 |-  ( ph -> X e. CC )
4 bj-bary1.neq 
 |-  ( ph -> A =/= B )
5 bj-bary1.s 
 |-  ( ph -> S e. CC )
6 bj-bary1.t 
 |-  ( ph -> T e. CC )
7 5 6 pncand 
 |-  ( ph -> ( ( S + T ) - T ) = S )
8 oveq1 
 |-  ( ( S + T ) = 1 -> ( ( S + T ) - T ) = ( 1 - T ) )
9 pm5.31 
 |-  ( ( ( ( S + T ) - T ) = S /\ ( ( S + T ) = 1 -> ( ( S + T ) - T ) = ( 1 - T ) ) ) -> ( ( S + T ) = 1 -> ( ( ( S + T ) - T ) = ( 1 - T ) /\ ( ( S + T ) - T ) = S ) ) )
10 7 8 9 sylancl 
 |-  ( ph -> ( ( S + T ) = 1 -> ( ( ( S + T ) - T ) = ( 1 - T ) /\ ( ( S + T ) - T ) = S ) ) )
11 eqtr2 
 |-  ( ( ( ( S + T ) - T ) = ( 1 - T ) /\ ( ( S + T ) - T ) = S ) -> ( 1 - T ) = S )
12 11 eqcomd 
 |-  ( ( ( ( S + T ) - T ) = ( 1 - T ) /\ ( ( S + T ) - T ) = S ) -> S = ( 1 - T ) )
13 10 12 syl6 
 |-  ( ph -> ( ( S + T ) = 1 -> S = ( 1 - T ) ) )
14 oveq1 
 |-  ( S = ( 1 - T ) -> ( S x. A ) = ( ( 1 - T ) x. A ) )
15 14 oveq1d 
 |-  ( S = ( 1 - T ) -> ( ( S x. A ) + ( T x. B ) ) = ( ( ( 1 - T ) x. A ) + ( T x. B ) ) )
16 eqtr 
 |-  ( ( X = ( ( S x. A ) + ( T x. B ) ) /\ ( ( S x. A ) + ( T x. B ) ) = ( ( ( 1 - T ) x. A ) + ( T x. B ) ) ) -> X = ( ( ( 1 - T ) x. A ) + ( T x. B ) ) )
17 15 16 sylan2 
 |-  ( ( X = ( ( S x. A ) + ( T x. B ) ) /\ S = ( 1 - T ) ) -> X = ( ( ( 1 - T ) x. A ) + ( T x. B ) ) )
18 1cnd 
 |-  ( ph -> 1 e. CC )
19 18 6 1 subdird 
 |-  ( ph -> ( ( 1 - T ) x. A ) = ( ( 1 x. A ) - ( T x. A ) ) )
20 1 mulid2d 
 |-  ( ph -> ( 1 x. A ) = A )
21 20 oveq1d 
 |-  ( ph -> ( ( 1 x. A ) - ( T x. A ) ) = ( A - ( T x. A ) ) )
22 19 21 eqtrd 
 |-  ( ph -> ( ( 1 - T ) x. A ) = ( A - ( T x. A ) ) )
23 22 oveq1d 
 |-  ( ph -> ( ( ( 1 - T ) x. A ) + ( T x. B ) ) = ( ( A - ( T x. A ) ) + ( T x. B ) ) )
24 17 23 sylan9eqr 
 |-  ( ( ph /\ ( X = ( ( S x. A ) + ( T x. B ) ) /\ S = ( 1 - T ) ) ) -> X = ( ( A - ( T x. A ) ) + ( T x. B ) ) )
25 24 ex 
 |-  ( ph -> ( ( X = ( ( S x. A ) + ( T x. B ) ) /\ S = ( 1 - T ) ) -> X = ( ( A - ( T x. A ) ) + ( T x. B ) ) ) )
26 13 25 sylan2d 
 |-  ( ph -> ( ( X = ( ( S x. A ) + ( T x. B ) ) /\ ( S + T ) = 1 ) -> X = ( ( A - ( T x. A ) ) + ( T x. B ) ) ) )
27 6 1 mulcld 
 |-  ( ph -> ( T x. A ) e. CC )
28 6 2 mulcld 
 |-  ( ph -> ( T x. B ) e. CC )
29 1 27 28 subadd23d 
 |-  ( ph -> ( ( A - ( T x. A ) ) + ( T x. B ) ) = ( A + ( ( T x. B ) - ( T x. A ) ) ) )
30 6 2 1 subdid 
 |-  ( ph -> ( T x. ( B - A ) ) = ( ( T x. B ) - ( T x. A ) ) )
31 30 eqcomd 
 |-  ( ph -> ( ( T x. B ) - ( T x. A ) ) = ( T x. ( B - A ) ) )
32 31 oveq2d 
 |-  ( ph -> ( A + ( ( T x. B ) - ( T x. A ) ) ) = ( A + ( T x. ( B - A ) ) ) )
33 29 32 eqtrd 
 |-  ( ph -> ( ( A - ( T x. A ) ) + ( T x. B ) ) = ( A + ( T x. ( B - A ) ) ) )
34 33 eqeq2d 
 |-  ( ph -> ( X = ( ( A - ( T x. A ) ) + ( T x. B ) ) <-> X = ( A + ( T x. ( B - A ) ) ) ) )
35 26 34 sylibd 
 |-  ( ph -> ( ( X = ( ( S x. A ) + ( T x. B ) ) /\ ( S + T ) = 1 ) -> X = ( A + ( T x. ( B - A ) ) ) ) )
36 oveq1 
 |-  ( X = ( A + ( T x. ( B - A ) ) ) -> ( X - A ) = ( ( A + ( T x. ( B - A ) ) ) - A ) )
37 2 1 subcld 
 |-  ( ph -> ( B - A ) e. CC )
38 6 37 mulcld 
 |-  ( ph -> ( T x. ( B - A ) ) e. CC )
39 1 38 pncan2d 
 |-  ( ph -> ( ( A + ( T x. ( B - A ) ) ) - A ) = ( T x. ( B - A ) ) )
40 39 eqeq2d 
 |-  ( ph -> ( ( X - A ) = ( ( A + ( T x. ( B - A ) ) ) - A ) <-> ( X - A ) = ( T x. ( B - A ) ) ) )
41 36 40 syl5ib 
 |-  ( ph -> ( X = ( A + ( T x. ( B - A ) ) ) -> ( X - A ) = ( T x. ( B - A ) ) ) )
42 eqcom 
 |-  ( ( X - A ) = ( T x. ( B - A ) ) <-> ( T x. ( B - A ) ) = ( X - A ) )
43 6 37 mulcomd 
 |-  ( ph -> ( T x. ( B - A ) ) = ( ( B - A ) x. T ) )
44 43 eqeq1d 
 |-  ( ph -> ( ( T x. ( B - A ) ) = ( X - A ) <-> ( ( B - A ) x. T ) = ( X - A ) ) )
45 3 1 subcld 
 |-  ( ph -> ( X - A ) e. CC )
46 4 necomd 
 |-  ( ph -> B =/= A )
47 2 1 46 subne0d 
 |-  ( ph -> ( B - A ) =/= 0 )
48 37 6 45 47 rdiv 
 |-  ( ph -> ( ( ( B - A ) x. T ) = ( X - A ) <-> T = ( ( X - A ) / ( B - A ) ) ) )
49 48 biimpd 
 |-  ( ph -> ( ( ( B - A ) x. T ) = ( X - A ) -> T = ( ( X - A ) / ( B - A ) ) ) )
50 44 49 sylbid 
 |-  ( ph -> ( ( T x. ( B - A ) ) = ( X - A ) -> T = ( ( X - A ) / ( B - A ) ) ) )
51 42 50 syl5bi 
 |-  ( ph -> ( ( X - A ) = ( T x. ( B - A ) ) -> T = ( ( X - A ) / ( B - A ) ) ) )
52 35 41 51 3syld 
 |-  ( ph -> ( ( X = ( ( S x. A ) + ( T x. B ) ) /\ ( S + T ) = 1 ) -> T = ( ( X - A ) / ( B - A ) ) ) )