Theorem bj-bary1lem

Description: Lemma for bj-bary1 : expression for 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$$
Assertion	bj-bary1lem	$$⊢\phi \to X=\left(\frac{B-X}{B-A}\right)A+\left(\frac{X-A}{B-A}\right)B$$

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	2 1	mulcld	$$⊢\phi \to BA\in ℂ$$
6	3 1	mulcld	$$⊢\phi \to XA\in ℂ$$
7	5 6	subcld	$$⊢\phi \to BA-XA\in ℂ$$
8	3 2	mulcld	$$⊢\phi \to XB\in ℂ$$
9	1 2	mulcld	$$⊢\phi \to AB\in ℂ$$
10	7 8 9	addsub12d	$$⊢\phi \to \left(BA-XA\right)+XB-AB=XB+\left(BA-XA\right)-AB$$
11	5 6 9	sub32d	$$⊢\phi \to BA-XA-AB=BA-AB-XA$$
12	2 1	bj-subcom	$$⊢\phi \to BA-AB=0$$
13	12	oveq1d	$$⊢\phi \to BA-AB-XA=0-XA$$
14	11 13	eqtrd	$$⊢\phi \to BA-XA-AB=0-XA$$
15	14	oveq2d	$$⊢\phi \to XB+\left(BA-XA\right)-AB=XB+0-XA$$
16	10 15	eqtrd	$$⊢\phi \to \left(BA-XA\right)+XB-AB=XB+0-XA$$
17		0cnd	$$⊢\phi \to 0\in ℂ$$
18	8 17 6	addsubassd	$$⊢\phi \to XB+0-XA=XB+0-XA$$
19	8	addid1d	$$⊢\phi \to XB+0=XB$$
20	19	oveq1d	$$⊢\phi \to XB+0-XA=XB-XA$$
21	16 18 20	3eqtr2d	$$⊢\phi \to \left(BA-XA\right)+XB-AB=XB-XA$$
22	2 3 1	subdird	$$⊢\phi \to \left(B-X\right)A=BA-XA$$
23	3 1 2	subdird	$$⊢\phi \to \left(X-A\right)B=XB-AB$$
24	22 23	oveq12d	$$⊢\phi \to \left(B-X\right)A+\left(X-A\right)B=\left(BA-XA\right)+XB-AB$$
25	3 2 1	subdid	$$⊢\phi \to X\left(B-A\right)=XB-XA$$
26	21 24 25	3eqtr4rd	$$⊢\phi \to X\left(B-A\right)=\left(B-X\right)A+\left(X-A\right)B$$
27	26	oveq1d	$$⊢\phi \to \frac{X\left(B-A\right)}{B-A}=\frac{\left(B-X\right)A+\left(X-A\right)B}{B-A}$$
28	2 3	subcld	$$⊢\phi \to B-X\in ℂ$$
29	28 1	mulcld	$$⊢\phi \to \left(B-X\right)A\in ℂ$$
30	3 1	subcld	$$⊢\phi \to X-A\in ℂ$$
31	30 2	mulcld	$$⊢\phi \to \left(X-A\right)B\in ℂ$$
32	2 1	subcld	$$⊢\phi \to B-A\in ℂ$$
33	4	necomd	$$⊢\phi \to B\ne A$$
34	2 1 33	subne0d	$$⊢\phi \to B-A\ne 0$$
35	29 31 32 34	divdird	$$⊢\phi \to \frac{\left(B-X\right)A+\left(X-A\right)B}{B-A}=\left(\frac{\left(B-X\right)A}{B-A}\right)+\left(\frac{\left(X-A\right)B}{B-A}\right)$$
36	27 35	eqtrd	$$⊢\phi \to \frac{X\left(B-A\right)}{B-A}=\left(\frac{\left(B-X\right)A}{B-A}\right)+\left(\frac{\left(X-A\right)B}{B-A}\right)$$
37	3 32 34	divcan4d	$$⊢\phi \to \frac{X\left(B-A\right)}{B-A}=X$$
38	28 1 32 34	div23d	$$⊢\phi \to \frac{\left(B-X\right)A}{B-A}=\left(\frac{B-X}{B-A}\right)A$$
39	30 2 32 34	div23d	$$⊢\phi \to \frac{\left(X-A\right)B}{B-A}=\left(\frac{X-A}{B-A}\right)B$$
40	38 39	oveq12d	$$⊢\phi \to \left(\frac{\left(B-X\right)A}{B-A}\right)+\left(\frac{\left(X-A\right)B}{B-A}\right)=\left(\frac{B-X}{B-A}\right)A+\left(\frac{X-A}{B-A}\right)B$$
41	36 37 40	3eqtr3d	$$⊢\phi \to X=\left(\frac{B-X}{B-A}\right)A+\left(\frac{X-A}{B-A}\right)B$$