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	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	bj-bary1.b	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
	bj-bary1.x	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
	bj-bary1.neq	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
	bj-bary1.s	⊢ ( 𝜑 → 𝑆 ∈ ℂ )
	bj-bary1.t	⊢ ( 𝜑 → 𝑇 ∈ ℂ )
Assertion	bj-bary1	⊢ ( 𝜑 → ( ( 𝑋 = ( ( 𝑆 · 𝐴 ) + ( 𝑇 · 𝐵 ) ) ∧ ( 𝑆 + 𝑇 ) = 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 1	mulcld	⊢ ( 𝜑 → ( 𝑆 · 𝐴 ) ∈ ℂ )
8	6 2	mulcld	⊢ ( 𝜑 → ( 𝑇 · 𝐵 ) ∈ ℂ )
9	7 8	addcomd	⊢ ( 𝜑 → ( ( 𝑆 · 𝐴 ) + ( 𝑇 · 𝐵 ) ) = ( ( 𝑇 · 𝐵 ) + ( 𝑆 · 𝐴 ) ) )
10	9	eqeq2d	⊢ ( 𝜑 → ( 𝑋 = ( ( 𝑆 · 𝐴 ) + ( 𝑇 · 𝐵 ) ) ↔ 𝑋 = ( ( 𝑇 · 𝐵 ) + ( 𝑆 · 𝐴 ) ) ) )
11	10	biimpd	⊢ ( 𝜑 → ( 𝑋 = ( ( 𝑆 · 𝐴 ) + ( 𝑇 · 𝐵 ) ) → 𝑋 = ( ( 𝑇 · 𝐵 ) + ( 𝑆 · 𝐴 ) ) ) )
12	5 6	addcomd	⊢ ( 𝜑 → ( 𝑆 + 𝑇 ) = ( 𝑇 + 𝑆 ) )
13	12	eqeq1d	⊢ ( 𝜑 → ( ( 𝑆 + 𝑇 ) = 1 ↔ ( 𝑇 + 𝑆 ) = 1 ) )
14	13	biimpd	⊢ ( 𝜑 → ( ( 𝑆 + 𝑇 ) = 1 → ( 𝑇 + 𝑆 ) = 1 ) )
15	4	necomd	⊢ ( 𝜑 → 𝐵 ≠ 𝐴 )
16	2 1 3 15 6 5	bj-bary1lem1	⊢ ( 𝜑 → ( ( 𝑋 = ( ( 𝑇 · 𝐵 ) + ( 𝑆 · 𝐴 ) ) ∧ ( 𝑇 + 𝑆 ) = 1 ) → 𝑆 = ( ( 𝑋 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) ) )
17	11 14 16	syl2and	⊢ ( 𝜑 → ( ( 𝑋 = ( ( 𝑆 · 𝐴 ) + ( 𝑇 · 𝐵 ) ) ∧ ( 𝑆 + 𝑇 ) = 1 ) → 𝑆 = ( ( 𝑋 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) ) )
18	3 2 1 2 4	div2subd	⊢ ( 𝜑 → ( ( 𝑋 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) = ( ( 𝐵 − 𝑋 ) / ( 𝐵 − 𝐴 ) ) )
19	18	eqeq2d	⊢ ( 𝜑 → ( 𝑆 = ( ( 𝑋 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) ↔ 𝑆 = ( ( 𝐵 − 𝑋 ) / ( 𝐵 − 𝐴 ) ) ) )
20	17 19	sylibd	⊢ ( 𝜑 → ( ( 𝑋 = ( ( 𝑆 · 𝐴 ) + ( 𝑇 · 𝐵 ) ) ∧ ( 𝑆 + 𝑇 ) = 1 ) → 𝑆 = ( ( 𝐵 − 𝑋 ) / ( 𝐵 − 𝐴 ) ) ) )
21	1 2 3 4 5 6	bj-bary1lem1	⊢ ( 𝜑 → ( ( 𝑋 = ( ( 𝑆 · 𝐴 ) + ( 𝑇 · 𝐵 ) ) ∧ ( 𝑆 + 𝑇 ) = 1 ) → 𝑇 = ( ( 𝑋 − 𝐴 ) / ( 𝐵 − 𝐴 ) ) ) )
22	20 21	jcad	⊢ ( 𝜑 → ( ( 𝑋 = ( ( 𝑆 · 𝐴 ) + ( 𝑇 · 𝐵 ) ) ∧ ( 𝑆 + 𝑇 ) = 1 ) → ( 𝑆 = ( ( 𝐵 − 𝑋 ) / ( 𝐵 − 𝐴 ) ) ∧ 𝑇 = ( ( 𝑋 − 𝐴 ) / ( 𝐵 − 𝐴 ) ) ) ) )
23	1 2 3 4	bj-bary1lem	⊢ ( 𝜑 → 𝑋 = ( ( ( ( 𝐵 − 𝑋 ) / ( 𝐵 − 𝐴 ) ) · 𝐴 ) + ( ( ( 𝑋 − 𝐴 ) / ( 𝐵 − 𝐴 ) ) · 𝐵 ) ) )
24		oveq1	⊢ ( 𝑆 = ( ( 𝐵 − 𝑋 ) / ( 𝐵 − 𝐴 ) ) → ( 𝑆 · 𝐴 ) = ( ( ( 𝐵 − 𝑋 ) / ( 𝐵 − 𝐴 ) ) · 𝐴 ) )
25		oveq1	⊢ ( 𝑇 = ( ( 𝑋 − 𝐴 ) / ( 𝐵 − 𝐴 ) ) → ( 𝑇 · 𝐵 ) = ( ( ( 𝑋 − 𝐴 ) / ( 𝐵 − 𝐴 ) ) · 𝐵 ) )
26	24 25	oveqan12d	⊢ ( ( 𝑆 = ( ( 𝐵 − 𝑋 ) / ( 𝐵 − 𝐴 ) ) ∧ 𝑇 = ( ( 𝑋 − 𝐴 ) / ( 𝐵 − 𝐴 ) ) ) → ( ( 𝑆 · 𝐴 ) + ( 𝑇 · 𝐵 ) ) = ( ( ( ( 𝐵 − 𝑋 ) / ( 𝐵 − 𝐴 ) ) · 𝐴 ) + ( ( ( 𝑋 − 𝐴 ) / ( 𝐵 − 𝐴 ) ) · 𝐵 ) ) )
27	26	a1i	⊢ ( 𝜑 → ( ( 𝑆 = ( ( 𝐵 − 𝑋 ) / ( 𝐵 − 𝐴 ) ) ∧ 𝑇 = ( ( 𝑋 − 𝐴 ) / ( 𝐵 − 𝐴 ) ) ) → ( ( 𝑆 · 𝐴 ) + ( 𝑇 · 𝐵 ) ) = ( ( ( ( 𝐵 − 𝑋 ) / ( 𝐵 − 𝐴 ) ) · 𝐴 ) + ( ( ( 𝑋 − 𝐴 ) / ( 𝐵 − 𝐴 ) ) · 𝐵 ) ) ) )
28		eqtr3	⊢ ( ( 𝑋 = ( ( ( ( 𝐵 − 𝑋 ) / ( 𝐵 − 𝐴 ) ) · 𝐴 ) + ( ( ( 𝑋 − 𝐴 ) / ( 𝐵 − 𝐴 ) ) · 𝐵 ) ) ∧ ( ( 𝑆 · 𝐴 ) + ( 𝑇 · 𝐵 ) ) = ( ( ( ( 𝐵 − 𝑋 ) / ( 𝐵 − 𝐴 ) ) · 𝐴 ) + ( ( ( 𝑋 − 𝐴 ) / ( 𝐵 − 𝐴 ) ) · 𝐵 ) ) ) → 𝑋 = ( ( 𝑆 · 𝐴 ) + ( 𝑇 · 𝐵 ) ) )
29	23 27 28	syl6an	⊢ ( 𝜑 → ( ( 𝑆 = ( ( 𝐵 − 𝑋 ) / ( 𝐵 − 𝐴 ) ) ∧ 𝑇 = ( ( 𝑋 − 𝐴 ) / ( 𝐵 − 𝐴 ) ) ) → 𝑋 = ( ( 𝑆 · 𝐴 ) + ( 𝑇 · 𝐵 ) ) ) )
30		oveq12	⊢ ( ( 𝑆 = ( ( 𝐵 − 𝑋 ) / ( 𝐵 − 𝐴 ) ) ∧ 𝑇 = ( ( 𝑋 − 𝐴 ) / ( 𝐵 − 𝐴 ) ) ) → ( 𝑆 + 𝑇 ) = ( ( ( 𝐵 − 𝑋 ) / ( 𝐵 − 𝐴 ) ) + ( ( 𝑋 − 𝐴 ) / ( 𝐵 − 𝐴 ) ) ) )
31	2 3	subcld	⊢ ( 𝜑 → ( 𝐵 − 𝑋 ) ∈ ℂ )
32	3 1	subcld	⊢ ( 𝜑 → ( 𝑋 − 𝐴 ) ∈ ℂ )
33	2 1	subcld	⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ∈ ℂ )
34	2 1 15	subne0d	⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ≠ 0 )
35	31 32 33 34	divdird	⊢ ( 𝜑 → ( ( ( 𝐵 − 𝑋 ) + ( 𝑋 − 𝐴 ) ) / ( 𝐵 − 𝐴 ) ) = ( ( ( 𝐵 − 𝑋 ) / ( 𝐵 − 𝐴 ) ) + ( ( 𝑋 − 𝐴 ) / ( 𝐵 − 𝐴 ) ) ) )
36	2 3 1	npncand	⊢ ( 𝜑 → ( ( 𝐵 − 𝑋 ) + ( 𝑋 − 𝐴 ) ) = ( 𝐵 − 𝐴 ) )
37	33 34 36	diveq1bd	⊢ ( 𝜑 → ( ( ( 𝐵 − 𝑋 ) + ( 𝑋 − 𝐴 ) ) / ( 𝐵 − 𝐴 ) ) = 1 )
38	35 37	eqtr3d	⊢ ( 𝜑 → ( ( ( 𝐵 − 𝑋 ) / ( 𝐵 − 𝐴 ) ) + ( ( 𝑋 − 𝐴 ) / ( 𝐵 − 𝐴 ) ) ) = 1 )
39	38	eqeq2d	⊢ ( 𝜑 → ( ( 𝑆 + 𝑇 ) = ( ( ( 𝐵 − 𝑋 ) / ( 𝐵 − 𝐴 ) ) + ( ( 𝑋 − 𝐴 ) / ( 𝐵 − 𝐴 ) ) ) ↔ ( 𝑆 + 𝑇 ) = 1 ) )
40	30 39	syl5ib	⊢ ( 𝜑 → ( ( 𝑆 = ( ( 𝐵 − 𝑋 ) / ( 𝐵 − 𝐴 ) ) ∧ 𝑇 = ( ( 𝑋 − 𝐴 ) / ( 𝐵 − 𝐴 ) ) ) → ( 𝑆 + 𝑇 ) = 1 ) )
41	29 40	jcad	⊢ ( 𝜑 → ( ( 𝑆 = ( ( 𝐵 − 𝑋 ) / ( 𝐵 − 𝐴 ) ) ∧ 𝑇 = ( ( 𝑋 − 𝐴 ) / ( 𝐵 − 𝐴 ) ) ) → ( 𝑋 = ( ( 𝑆 · 𝐴 ) + ( 𝑇 · 𝐵 ) ) ∧ ( 𝑆 + 𝑇 ) = 1 ) ) )
42	22 41	impbid	⊢ ( 𝜑 → ( ( 𝑋 = ( ( 𝑆 · 𝐴 ) + ( 𝑇 · 𝐵 ) ) ∧ ( 𝑆 + 𝑇 ) = 1 ) ↔ ( 𝑆 = ( ( 𝐵 − 𝑋 ) / ( 𝐵 − 𝐴 ) ) ∧ 𝑇 = ( ( 𝑋 − 𝐴 ) / ( 𝐵 − 𝐴 ) ) ) ) )