Metamath Proof Explorer

Theorem bj-bary1lem

Description: Lemma for bj-bary1 : expression for 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 )
Assertion bj-bary1lem 
|- ( ph -> X = ( ( ( ( B - X ) / ( B - A ) ) x. A ) + ( ( ( X - A ) / ( B - A ) ) x. B ) ) )

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 2 1 mulcld 
 |-  ( ph -> ( B x. A ) e. CC )
6 3 1 mulcld 
 |-  ( ph -> ( X x. A ) e. CC )
7 5 6 subcld 
 |-  ( ph -> ( ( B x. A ) - ( X x. A ) ) e. CC )
8 3 2 mulcld 
 |-  ( ph -> ( X x. B ) e. CC )
9 1 2 mulcld 
 |-  ( ph -> ( A x. B ) e. CC )
10 7 8 9 addsub12d 
 |-  ( ph -> ( ( ( B x. A ) - ( X x. A ) ) + ( ( X x. B ) - ( A x. B ) ) ) = ( ( X x. B ) + ( ( ( B x. A ) - ( X x. A ) ) - ( A x. B ) ) ) )
11 5 6 9 sub32d 
 |-  ( ph -> ( ( ( B x. A ) - ( X x. A ) ) - ( A x. B ) ) = ( ( ( B x. A ) - ( A x. B ) ) - ( X x. A ) ) )
12 2 1 bj-subcom 
 |-  ( ph -> ( ( B x. A ) - ( A x. B ) ) = 0 )
13 12 oveq1d 
 |-  ( ph -> ( ( ( B x. A ) - ( A x. B ) ) - ( X x. A ) ) = ( 0 - ( X x. A ) ) )
14 11 13 eqtrd 
 |-  ( ph -> ( ( ( B x. A ) - ( X x. A ) ) - ( A x. B ) ) = ( 0 - ( X x. A ) ) )
15 14 oveq2d 
 |-  ( ph -> ( ( X x. B ) + ( ( ( B x. A ) - ( X x. A ) ) - ( A x. B ) ) ) = ( ( X x. B ) + ( 0 - ( X x. A ) ) ) )
16 10 15 eqtrd 
 |-  ( ph -> ( ( ( B x. A ) - ( X x. A ) ) + ( ( X x. B ) - ( A x. B ) ) ) = ( ( X x. B ) + ( 0 - ( X x. A ) ) ) )
17 0cnd 
 |-  ( ph -> 0 e. CC )
18 8 17 6 addsubassd 
 |-  ( ph -> ( ( ( X x. B ) + 0 ) - ( X x. A ) ) = ( ( X x. B ) + ( 0 - ( X x. A ) ) ) )
19 8 addridd 
 |-  ( ph -> ( ( X x. B ) + 0 ) = ( X x. B ) )
20 19 oveq1d 
 |-  ( ph -> ( ( ( X x. B ) + 0 ) - ( X x. A ) ) = ( ( X x. B ) - ( X x. A ) ) )
21 16 18 20 3eqtr2d 
 |-  ( ph -> ( ( ( B x. A ) - ( X x. A ) ) + ( ( X x. B ) - ( A x. B ) ) ) = ( ( X x. B ) - ( X x. A ) ) )
22 2 3 1 subdird 
 |-  ( ph -> ( ( B - X ) x. A ) = ( ( B x. A ) - ( X x. A ) ) )
23 3 1 2 subdird 
 |-  ( ph -> ( ( X - A ) x. B ) = ( ( X x. B ) - ( A x. B ) ) )
24 22 23 oveq12d 
 |-  ( ph -> ( ( ( B - X ) x. A ) + ( ( X - A ) x. B ) ) = ( ( ( B x. A ) - ( X x. A ) ) + ( ( X x. B ) - ( A x. B ) ) ) )
25 3 2 1 subdid 
 |-  ( ph -> ( X x. ( B - A ) ) = ( ( X x. B ) - ( X x. A ) ) )
26 21 24 25 3eqtr4rd 
 |-  ( ph -> ( X x. ( B - A ) ) = ( ( ( B - X ) x. A ) + ( ( X - A ) x. B ) ) )
27 26 oveq1d 
 |-  ( ph -> ( ( X x. ( B - A ) ) / ( B - A ) ) = ( ( ( ( B - X ) x. A ) + ( ( X - A ) x. B ) ) / ( B - A ) ) )
28 2 3 subcld 
 |-  ( ph -> ( B - X ) e. CC )
29 28 1 mulcld 
 |-  ( ph -> ( ( B - X ) x. A ) e. CC )
30 3 1 subcld 
 |-  ( ph -> ( X - A ) e. CC )
31 30 2 mulcld 
 |-  ( ph -> ( ( X - A ) x. B ) e. CC )
32 2 1 subcld 
 |-  ( ph -> ( B - A ) e. CC )
33 4 necomd 
 |-  ( ph -> B =/= A )
34 2 1 33 subne0d 
 |-  ( ph -> ( B - A ) =/= 0 )
35 29 31 32 34 divdird 
 |-  ( ph -> ( ( ( ( B - X ) x. A ) + ( ( X - A ) x. B ) ) / ( B - A ) ) = ( ( ( ( B - X ) x. A ) / ( B - A ) ) + ( ( ( X - A ) x. B ) / ( B - A ) ) ) )
36 27 35 eqtrd 
 |-  ( ph -> ( ( X x. ( B - A ) ) / ( B - A ) ) = ( ( ( ( B - X ) x. A ) / ( B - A ) ) + ( ( ( X - A ) x. B ) / ( B - A ) ) ) )
37 3 32 34 divcan4d 
 |-  ( ph -> ( ( X x. ( B - A ) ) / ( B - A ) ) = X )
38 28 1 32 34 div23d 
 |-  ( ph -> ( ( ( B - X ) x. A ) / ( B - A ) ) = ( ( ( B - X ) / ( B - A ) ) x. A ) )
39 30 2 32 34 div23d 
 |-  ( ph -> ( ( ( X - A ) x. B ) / ( B - A ) ) = ( ( ( X - A ) / ( B - A ) ) x. B ) )
40 38 39 oveq12d 
 |-  ( ph -> ( ( ( ( B - X ) x. A ) / ( B - A ) ) + ( ( ( X - A ) x. B ) / ( B - A ) ) ) = ( ( ( ( B - X ) / ( B - A ) ) x. A ) + ( ( ( X - A ) / ( B - A ) ) x. B ) ) )
41 36 37 40 3eqtr3d 
 |-  ( ph -> X = ( ( ( ( B - X ) / ( B - A ) ) x. A ) + ( ( ( X - A ) / ( B - A ) ) x. B ) ) )