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	$$⊢\phi \to A\in ℂ$$
	bj-bary1.b	$$⊢\phi \to B\in ℂ$$
	bj-bary1.x	$$⊢\phi \to X\in ℂ$$
	bj-bary1.neq	$$⊢\phi \to A\ne B$$
	bj-bary1.s	$$⊢\phi \to S\in ℂ$$
	bj-bary1.t	$$⊢\phi \to T\in ℂ$$
Assertion	bj-bary1lem1	$$⊢\phi \to \left(\left(X=SA+TB\wedge S+T=1\right)\to T=\frac{X-A}{B-A}\right)$$

Proof

Step	Hyp	Ref	Expression
1		bj-bary1.a	$$⊢\phi \to A\in ℂ$$
2		bj-bary1.b	$$⊢\phi \to B\in ℂ$$
3		bj-bary1.x	$$⊢\phi \to X\in ℂ$$
4		bj-bary1.neq	$$⊢\phi \to A\ne B$$
5		bj-bary1.s	$$⊢\phi \to S\in ℂ$$
6		bj-bary1.t	$$⊢\phi \to T\in ℂ$$
7	5 6	pncand	$$⊢\phi \to S+T-T=S$$
8		oveq1	$$⊢S+T=1\to S+T-T=1-T$$
9		pm5.31	$$⊢\left(S+T-T=S\wedge \left(S+T=1\to S+T-T=1-T\right)\right)\to \left(S+T=1\to \left(S+T-T=1-T\wedge S+T-T=S\right)\right)$$
10	7 8 9	sylancl	$$⊢\phi \to \left(S+T=1\to \left(S+T-T=1-T\wedge S+T-T=S\right)\right)$$
11		eqtr2	$$⊢\left(S+T-T=1-T\wedge S+T-T=S\right)\to 1-T=S$$
12	11	eqcomd	$$⊢\left(S+T-T=1-T\wedge S+T-T=S\right)\to S=1-T$$
13	10 12	syl6	$$⊢\phi \to \left(S+T=1\to S=1-T\right)$$
14		oveq1	$$⊢S=1-T\to SA=\left(1-T\right)A$$
15	14	oveq1d	$$⊢S=1-T\to SA+TB=\left(1-T\right)A+TB$$
16		eqtr	$$⊢\left(X=SA+TB\wedge SA+TB=\left(1-T\right)A+TB\right)\to X=\left(1-T\right)A+TB$$
17	15 16	sylan2	$$⊢\left(X=SA+TB\wedge S=1-T\right)\to X=\left(1-T\right)A+TB$$
18		1cnd	$$⊢\phi \to 1\in ℂ$$
19	18 6 1	subdird	$$⊢\phi \to \left(1-T\right)A=1A-TA$$
20	1	mullidd	$$⊢\phi \to 1A=A$$
21	20	oveq1d	$$⊢\phi \to 1A-TA=A-TA$$
22	19 21	eqtrd	$$⊢\phi \to \left(1-T\right)A=A-TA$$
23	22	oveq1d	$$⊢\phi \to \left(1-T\right)A+TB=A-TA+TB$$
24	17 23	sylan9eqr	$$⊢\left(\phi \wedge \left(X=SA+TB\wedge S=1-T\right)\right)\to X=A-TA+TB$$
25	24	ex	$$⊢\phi \to \left(\left(X=SA+TB\wedge S=1-T\right)\to X=A-TA+TB\right)$$
26	13 25	sylan2d	$$⊢\phi \to \left(\left(X=SA+TB\wedge S+T=1\right)\to X=A-TA+TB\right)$$
27	6 1	mulcld	$$⊢\phi \to TA\in ℂ$$
28	6 2	mulcld	$$⊢\phi \to TB\in ℂ$$
29	1 27 28	subadd23d	$$⊢\phi \to A-TA+TB=A+TB-TA$$
30	6 2 1	subdid	$$⊢\phi \to T\left(B-A\right)=TB-TA$$
31	30	eqcomd	$$⊢\phi \to TB-TA=T\left(B-A\right)$$
32	31	oveq2d	$$⊢\phi \to A+TB-TA=A+T\left(B-A\right)$$
33	29 32	eqtrd	$$⊢\phi \to A-TA+TB=A+T\left(B-A\right)$$
34	33	eqeq2d	$$⊢\phi \to \left(X=A-TA+TB\leftrightarrow X=A+T\left(B-A\right)\right)$$
35	26 34	sylibd	$$⊢\phi \to \left(\left(X=SA+TB\wedge S+T=1\right)\to X=A+T\left(B-A\right)\right)$$
36		oveq1	$$⊢X=A+T\left(B-A\right)\to X-A=A+T\left(B-A\right)-A$$
37	2 1	subcld	$$⊢\phi \to B-A\in ℂ$$
38	6 37	mulcld	$$⊢\phi \to T\left(B-A\right)\in ℂ$$
39	1 38	pncan2d	$$⊢\phi \to A+T\left(B-A\right)-A=T\left(B-A\right)$$
40	39	eqeq2d	$$⊢\phi \to \left(X-A=A+T\left(B-A\right)-A\leftrightarrow X-A=T\left(B-A\right)\right)$$
41	36 40	imbitrid	$$⊢\phi \to \left(X=A+T\left(B-A\right)\to X-A=T\left(B-A\right)\right)$$
42		eqcom	$$⊢X-A=T\left(B-A\right)\leftrightarrow T\left(B-A\right)=X-A$$
43	6 37	mulcomd	$$⊢\phi \to T\left(B-A\right)=\left(B-A\right)T$$
44	43	eqeq1d	$$⊢\phi \to \left(T\left(B-A\right)=X-A\leftrightarrow \left(B-A\right)T=X-A\right)$$
45	3 1	subcld	$$⊢\phi \to X-A\in ℂ$$
46	4	necomd	$$⊢\phi \to B\ne A$$
47	2 1 46	subne0d	$$⊢\phi \to B-A\ne 0$$
48	37 6 45 47	rdiv	$$⊢\phi \to \left(\left(B-A\right)T=X-A\leftrightarrow T=\frac{X-A}{B-A}\right)$$
49	48	biimpd	$$⊢\phi \to \left(\left(B-A\right)T=X-A\to T=\frac{X-A}{B-A}\right)$$
50	44 49	sylbid	$$⊢\phi \to \left(T\left(B-A\right)=X-A\to T=\frac{X-A}{B-A}\right)$$
51	42 50	biimtrid	$$⊢\phi \to \left(X-A=T\left(B-A\right)\to T=\frac{X-A}{B-A}\right)$$
52	35 41 51	3syld	$$⊢\phi \to \left(\left(X=SA+TB\wedge S+T=1\right)\to T=\frac{X-A}{B-A}\right)$$