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	mullidd	⊢ ( 𝜑 → ( 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	imbitrid	⊢ ( 𝜑 → ( 𝑋 = ( 𝐴 + ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) → ( 𝑋 − 𝐴 ) = ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) )
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	biimtrid	⊢ ( 𝜑 → ( ( 𝑋 − 𝐴 ) = ( 𝑇 · ( 𝐵 − 𝐴 ) ) → 𝑇 = ( ( 𝑋 − 𝐴 ) / ( 𝐵 − 𝐴 ) ) ) )
52	35 41 51	3syld	⊢ ( 𝜑 → ( ( 𝑋 = ( ( 𝑆 · 𝐴 ) + ( 𝑇 · 𝐵 ) ) ∧ ( 𝑆 + 𝑇 ) = 1 ) → 𝑇 = ( ( 𝑋 − 𝐴 ) / ( 𝐵 − 𝐴 ) ) ) )