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	$⊢ φ \to A \in ℂ$
	bj-bary1.b	$⊢ φ \to B \in ℂ$
	bj-bary1.x	$⊢ φ \to X \in ℂ$
	bj-bary1.neq	$⊢ φ \to A \neq B$
	bj-bary1.s	$⊢ φ \to S \in ℂ$
	bj-bary1.t	$⊢ φ \to T \in ℂ$
Assertion	bj-bary1	$⊢ φ \to ((X = S A + T B \land S + T = 1) \leftrightarrow (S = \frac{B - X}{B - A} \land T = \frac{X - A}{B - A}))$

Proof

Step	Hyp	Ref	Expression
1		bj-bary1.a	$⊢ φ \to A \in ℂ$
2		bj-bary1.b	$⊢ φ \to B \in ℂ$
3		bj-bary1.x	$⊢ φ \to X \in ℂ$
4		bj-bary1.neq	$⊢ φ \to A \neq B$
5		bj-bary1.s	$⊢ φ \to S \in ℂ$
6		bj-bary1.t	$⊢ φ \to T \in ℂ$
7	5 1	mulcld	$⊢ φ \to S A \in ℂ$
8	6 2	mulcld	$⊢ φ \to T B \in ℂ$
9	7 8	addcomd	$⊢ φ \to S A + T B = T B + S A$
10	9	eqeq2d	$⊢ φ \to (X = S A + T B \leftrightarrow X = T B + S A)$
11	10	biimpd	$⊢ φ \to (X = S A + T B \to X = T B + S A)$
12	5 6	addcomd	$⊢ φ \to S + T = T + S$
13	12	eqeq1d	$⊢ φ \to (S + T = 1 \leftrightarrow T + S = 1)$
14	13	biimpd	$⊢ φ \to (S + T = 1 \to T + S = 1)$
15	4	necomd	$⊢ φ \to B \neq A$
16	2 1 3 15 6 5	bj-bary1lem1	$⊢ φ \to ((X = T B + S A \land T + S = 1) \to S = \frac{X - B}{A - B})$
17	11 14 16	syl2and	$⊢ φ \to ((X = S A + T B \land S + T = 1) \to S = \frac{X - B}{A - B})$
18	3 2 1 2 4	div2subd	$⊢ φ \to \frac{X - B}{A - B} = \frac{B - X}{B - A}$
19	18	eqeq2d	$⊢ φ \to (S = \frac{X - B}{A - B} \leftrightarrow S = \frac{B - X}{B - A})$
20	17 19	sylibd	$⊢ φ \to ((X = S A + T B \land S + T = 1) \to S = \frac{B - X}{B - A})$
21	1 2 3 4 5 6	bj-bary1lem1	$⊢ φ \to ((X = S A + T B \land S + T = 1) \to T = \frac{X - A}{B - A})$
22	20 21	jcad	$⊢ φ \to ((X = S A + T B \land S + T = 1) \to (S = \frac{B - X}{B - A} \land T = \frac{X - A}{B - A}))$
23	1 2 3 4	bj-bary1lem	$⊢ φ \to X = (\frac{B - X}{B - A}) A + (\frac{X - A}{B - A}) B$
24		oveq1	$⊢ S = \frac{B - X}{B - A} \to S A = (\frac{B - X}{B - A}) A$
25		oveq1	$⊢ T = \frac{X - A}{B - A} \to T B = (\frac{X - A}{B - A}) B$
26	24 25	oveqan12d	$⊢ (S = \frac{B - X}{B - A} \land T = \frac{X - A}{B - A}) \to S A + T B = (\frac{B - X}{B - A}) A + (\frac{X - A}{B - A}) B$
27	26	a1i	$⊢ φ \to ((S = \frac{B - X}{B - A} \land T = \frac{X - A}{B - A}) \to S A + T B = (\frac{B - X}{B - A}) A + (\frac{X - A}{B - A}) B)$
28		eqtr3	$⊢ (X = (\frac{B - X}{B - A}) A + (\frac{X - A}{B - A}) B \land S A + T B = (\frac{B - X}{B - A}) A + (\frac{X - A}{B - A}) B) \to X = S A + T B$
29	23 27 28	syl6an	$⊢ φ \to ((S = \frac{B - X}{B - A} \land T = \frac{X - A}{B - A}) \to X = S A + T B)$
30		oveq12	$⊢ (S = \frac{B - X}{B - A} \land T = \frac{X - A}{B - A}) \to S + T = (\frac{B - X}{B - A}) + (\frac{X - A}{B - A})$
31	2 3	subcld	$⊢ φ \to B - X \in ℂ$
32	3 1	subcld	$⊢ φ \to X - A \in ℂ$
33	2 1	subcld	$⊢ φ \to B - A \in ℂ$
34	2 1 15	subne0d	$⊢ φ \to B - A \neq 0$
35	31 32 33 34	divdird	$⊢ φ \to \frac{(B - X) + X - A}{B - A} = (\frac{B - X}{B - A}) + (\frac{X - A}{B - A})$
36	2 3 1	npncand	$⊢ φ \to (B - X) + X - A = B - A$
37	33 34 36	diveq1bd	$⊢ φ \to \frac{(B - X) + X - A}{B - A} = 1$
38	35 37	eqtr3d	$⊢ φ \to (\frac{B - X}{B - A}) + (\frac{X - A}{B - A}) = 1$
39	38	eqeq2d	$⊢ φ \to (S + T = (\frac{B - X}{B - A}) + (\frac{X - A}{B - A}) \leftrightarrow S + T = 1)$
40	30 39	imbitrid	$⊢ φ \to ((S = \frac{B - X}{B - A} \land T = \frac{X - A}{B - A}) \to S + T = 1)$
41	29 40	jcad	$⊢ φ \to ((S = \frac{B - X}{B - A} \land T = \frac{X - A}{B - A}) \to (X = S A + T B \land S + T = 1))$
42	22 41	impbid	$⊢ φ \to ((X = S A + T B \land S + T = 1) \leftrightarrow (S = \frac{B - X}{B - A} \land T = \frac{X - A}{B - A}))$

Metamath Proof Explorer

Theorem bj-bary1

Proof