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 ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
bj-bary1.b ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
bj-bary1.x ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
bj-bary1.neq ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
bj-bary1.s ⊢ ( 𝜑 → 𝑆 ∈ ℂ )
bj-bary1.t ⊢ ( 𝜑 → 𝑇 ∈ ℂ )
Assertion bj-bary1lem1 ( 𝜑 → ( ( 𝑋 = ( ( 𝑆 · 𝐴 ) + ( 𝑇 · 𝐵 ) ) ∧ ( 𝑆 + 𝑇 ) = 1 ) → 𝑇 = ( ( 𝑋 − 𝐴 ) / ( 𝐵 − 𝐴 ) ) ) )

Proof

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