Metamath Proof Explorer

Theorem bj-bary1

Description: Barycentric coordinates in one dimension (complex line). In the statement, X is the barycenter of the two points A , B with respective normalized coefficients S , T . (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-bary1 
|- ( ph -> ( ( X = ( ( S x. A ) + ( T x. B ) ) /\ ( S + T ) = 1 ) <-> ( S = ( ( B - X ) / ( B - A ) ) /\ 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 1 mulcld 
 |-  ( ph -> ( S x. A ) e. CC )
8 6 2 mulcld 
 |-  ( ph -> ( T x. B ) e. CC )
9 7 8 addcomd 
 |-  ( ph -> ( ( S x. A ) + ( T x. B ) ) = ( ( T x. B ) + ( S x. A ) ) )
10 9 eqeq2d 
 |-  ( ph -> ( X = ( ( S x. A ) + ( T x. B ) ) <-> X = ( ( T x. B ) + ( S x. A ) ) ) )
11 10 biimpd 
 |-  ( ph -> ( X = ( ( S x. A ) + ( T x. B ) ) -> X = ( ( T x. B ) + ( S x. A ) ) ) )
12 5 6 addcomd 
 |-  ( ph -> ( S + T ) = ( T + S ) )
13 12 eqeq1d 
 |-  ( ph -> ( ( S + T ) = 1 <-> ( T + S ) = 1 ) )
14 13 biimpd 
 |-  ( ph -> ( ( S + T ) = 1 -> ( T + S ) = 1 ) )
15 4 necomd 
 |-  ( ph -> B =/= A )
16 2 1 3 15 6 5 bj-bary1lem1 
 |-  ( ph -> ( ( X = ( ( T x. B ) + ( S x. A ) ) /\ ( T + S ) = 1 ) -> S = ( ( X - B ) / ( A - B ) ) ) )
17 11 14 16 syl2and 
 |-  ( ph -> ( ( X = ( ( S x. A ) + ( T x. B ) ) /\ ( S + T ) = 1 ) -> S = ( ( X - B ) / ( A - B ) ) ) )
18 3 2 1 2 4 div2subd 
 |-  ( ph -> ( ( X - B ) / ( A - B ) ) = ( ( B - X ) / ( B - A ) ) )
19 18 eqeq2d 
 |-  ( ph -> ( S = ( ( X - B ) / ( A - B ) ) <-> S = ( ( B - X ) / ( B - A ) ) ) )
20 17 19 sylibd 
 |-  ( ph -> ( ( X = ( ( S x. A ) + ( T x. B ) ) /\ ( S + T ) = 1 ) -> S = ( ( B - X ) / ( B - A ) ) ) )
21 1 2 3 4 5 6 bj-bary1lem1 
 |-  ( ph -> ( ( X = ( ( S x. A ) + ( T x. B ) ) /\ ( S + T ) = 1 ) -> T = ( ( X - A ) / ( B - A ) ) ) )
22 20 21 jcad 
 |-  ( ph -> ( ( X = ( ( S x. A ) + ( T x. B ) ) /\ ( S + T ) = 1 ) -> ( S = ( ( B - X ) / ( B - A ) ) /\ T = ( ( X - A ) / ( B - A ) ) ) ) )
23 1 2 3 4 bj-bary1lem 
 |-  ( ph -> X = ( ( ( ( B - X ) / ( B - A ) ) x. A ) + ( ( ( X - A ) / ( B - A ) ) x. B ) ) )
24 oveq1 
 |-  ( S = ( ( B - X ) / ( B - A ) ) -> ( S x. A ) = ( ( ( B - X ) / ( B - A ) ) x. A ) )
25 oveq1 
 |-  ( T = ( ( X - A ) / ( B - A ) ) -> ( T x. B ) = ( ( ( X - A ) / ( B - A ) ) x. B ) )
26 24 25 oveqan12d 
 |-  ( ( S = ( ( B - X ) / ( B - A ) ) /\ T = ( ( X - A ) / ( B - A ) ) ) -> ( ( S x. A ) + ( T x. B ) ) = ( ( ( ( B - X ) / ( B - A ) ) x. A ) + ( ( ( X - A ) / ( B - A ) ) x. B ) ) )
27 26 a1i 
 |-  ( ph -> ( ( S = ( ( B - X ) / ( B - A ) ) /\ T = ( ( X - A ) / ( B - A ) ) ) -> ( ( S x. A ) + ( T x. B ) ) = ( ( ( ( B - X ) / ( B - A ) ) x. A ) + ( ( ( X - A ) / ( B - A ) ) x. B ) ) ) )
28 eqtr3 
 |-  ( ( X = ( ( ( ( B - X ) / ( B - A ) ) x. A ) + ( ( ( X - A ) / ( B - A ) ) x. B ) ) /\ ( ( S x. A ) + ( T x. B ) ) = ( ( ( ( B - X ) / ( B - A ) ) x. A ) + ( ( ( X - A ) / ( B - A ) ) x. B ) ) ) -> X = ( ( S x. A ) + ( T x. B ) ) )
29 23 27 28 syl6an 
 |-  ( ph -> ( ( S = ( ( B - X ) / ( B - A ) ) /\ T = ( ( X - A ) / ( B - A ) ) ) -> X = ( ( S x. A ) + ( T x. B ) ) ) )
30 oveq12 
 |-  ( ( S = ( ( B - X ) / ( B - A ) ) /\ T = ( ( X - A ) / ( B - A ) ) ) -> ( S + T ) = ( ( ( B - X ) / ( B - A ) ) + ( ( X - A ) / ( B - A ) ) ) )
31 2 3 subcld 
 |-  ( ph -> ( B - X ) e. CC )
32 3 1 subcld 
 |-  ( ph -> ( X - A ) e. CC )
33 2 1 subcld 
 |-  ( ph -> ( B - A ) e. CC )
34 2 1 15 subne0d 
 |-  ( ph -> ( B - A ) =/= 0 )
35 31 32 33 34 divdird 
 |-  ( ph -> ( ( ( B - X ) + ( X - A ) ) / ( B - A ) ) = ( ( ( B - X ) / ( B - A ) ) + ( ( X - A ) / ( B - A ) ) ) )
36 2 3 1 npncand 
 |-  ( ph -> ( ( B - X ) + ( X - A ) ) = ( B - A ) )
37 33 34 36 diveq1bd 
 |-  ( ph -> ( ( ( B - X ) + ( X - A ) ) / ( B - A ) ) = 1 )
38 35 37 eqtr3d 
 |-  ( ph -> ( ( ( B - X ) / ( B - A ) ) + ( ( X - A ) / ( B - A ) ) ) = 1 )
39 38 eqeq2d 
 |-  ( ph -> ( ( S + T ) = ( ( ( B - X ) / ( B - A ) ) + ( ( X - A ) / ( B - A ) ) ) <-> ( S + T ) = 1 ) )
40 30 39 imbitrid 
 |-  ( ph -> ( ( S = ( ( B - X ) / ( B - A ) ) /\ T = ( ( X - A ) / ( B - A ) ) ) -> ( S + T ) = 1 ) )
41 29 40 jcad 
 |-  ( ph -> ( ( S = ( ( B - X ) / ( B - A ) ) /\ T = ( ( X - A ) / ( B - A ) ) ) -> ( X = ( ( S x. A ) + ( T x. B ) ) /\ ( S + T ) = 1 ) ) )
42 22 41 impbid 
 |-  ( ph -> ( ( X = ( ( S x. A ) + ( T x. B ) ) /\ ( S + T ) = 1 ) <-> ( S = ( ( B - X ) / ( B - A ) ) /\ T = ( ( X - A ) / ( B - A ) ) ) ) )