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	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	bj-bary1.b	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
	bj-bary1.x	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
	bj-bary1.neq	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
Assertion	bj-bary1lem	⊢ ( 𝜑 → 𝑋 = ( ( ( ( 𝐵 − 𝑋 ) / ( 𝐵 − 𝐴 ) ) · 𝐴 ) + ( ( ( 𝑋 − 𝐴 ) / ( 𝐵 − 𝐴 ) ) · 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		bj-bary1.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2		bj-bary1.b	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
3		bj-bary1.x	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
4		bj-bary1.neq	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
5	2 1	mulcld	⊢ ( 𝜑 → ( 𝐵 · 𝐴 ) ∈ ℂ )
6	3 1	mulcld	⊢ ( 𝜑 → ( 𝑋 · 𝐴 ) ∈ ℂ )
7	5 6	subcld	⊢ ( 𝜑 → ( ( 𝐵 · 𝐴 ) − ( 𝑋 · 𝐴 ) ) ∈ ℂ )
8	3 2	mulcld	⊢ ( 𝜑 → ( 𝑋 · 𝐵 ) ∈ ℂ )
9	1 2	mulcld	⊢ ( 𝜑 → ( 𝐴 · 𝐵 ) ∈ ℂ )
10	7 8 9	addsub12d	⊢ ( 𝜑 → ( ( ( 𝐵 · 𝐴 ) − ( 𝑋 · 𝐴 ) ) + ( ( 𝑋 · 𝐵 ) − ( 𝐴 · 𝐵 ) ) ) = ( ( 𝑋 · 𝐵 ) + ( ( ( 𝐵 · 𝐴 ) − ( 𝑋 · 𝐴 ) ) − ( 𝐴 · 𝐵 ) ) ) )
11	5 6 9	sub32d	⊢ ( 𝜑 → ( ( ( 𝐵 · 𝐴 ) − ( 𝑋 · 𝐴 ) ) − ( 𝐴 · 𝐵 ) ) = ( ( ( 𝐵 · 𝐴 ) − ( 𝐴 · 𝐵 ) ) − ( 𝑋 · 𝐴 ) ) )
12	2 1	bj-subcom	⊢ ( 𝜑 → ( ( 𝐵 · 𝐴 ) − ( 𝐴 · 𝐵 ) ) = 0 )
13	12	oveq1d	⊢ ( 𝜑 → ( ( ( 𝐵 · 𝐴 ) − ( 𝐴 · 𝐵 ) ) − ( 𝑋 · 𝐴 ) ) = ( 0 − ( 𝑋 · 𝐴 ) ) )
14	11 13	eqtrd	⊢ ( 𝜑 → ( ( ( 𝐵 · 𝐴 ) − ( 𝑋 · 𝐴 ) ) − ( 𝐴 · 𝐵 ) ) = ( 0 − ( 𝑋 · 𝐴 ) ) )
15	14	oveq2d	⊢ ( 𝜑 → ( ( 𝑋 · 𝐵 ) + ( ( ( 𝐵 · 𝐴 ) − ( 𝑋 · 𝐴 ) ) − ( 𝐴 · 𝐵 ) ) ) = ( ( 𝑋 · 𝐵 ) + ( 0 − ( 𝑋 · 𝐴 ) ) ) )
16	10 15	eqtrd	⊢ ( 𝜑 → ( ( ( 𝐵 · 𝐴 ) − ( 𝑋 · 𝐴 ) ) + ( ( 𝑋 · 𝐵 ) − ( 𝐴 · 𝐵 ) ) ) = ( ( 𝑋 · 𝐵 ) + ( 0 − ( 𝑋 · 𝐴 ) ) ) )
17		0cnd	⊢ ( 𝜑 → 0 ∈ ℂ )
18	8 17 6	addsubassd	⊢ ( 𝜑 → ( ( ( 𝑋 · 𝐵 ) + 0 ) − ( 𝑋 · 𝐴 ) ) = ( ( 𝑋 · 𝐵 ) + ( 0 − ( 𝑋 · 𝐴 ) ) ) )
19	8	addid1d	⊢ ( 𝜑 → ( ( 𝑋 · 𝐵 ) + 0 ) = ( 𝑋 · 𝐵 ) )
20	19	oveq1d	⊢ ( 𝜑 → ( ( ( 𝑋 · 𝐵 ) + 0 ) − ( 𝑋 · 𝐴 ) ) = ( ( 𝑋 · 𝐵 ) − ( 𝑋 · 𝐴 ) ) )
21	16 18 20	3eqtr2d	⊢ ( 𝜑 → ( ( ( 𝐵 · 𝐴 ) − ( 𝑋 · 𝐴 ) ) + ( ( 𝑋 · 𝐵 ) − ( 𝐴 · 𝐵 ) ) ) = ( ( 𝑋 · 𝐵 ) − ( 𝑋 · 𝐴 ) ) )
22	2 3 1	subdird	⊢ ( 𝜑 → ( ( 𝐵 − 𝑋 ) · 𝐴 ) = ( ( 𝐵 · 𝐴 ) − ( 𝑋 · 𝐴 ) ) )
23	3 1 2	subdird	⊢ ( 𝜑 → ( ( 𝑋 − 𝐴 ) · 𝐵 ) = ( ( 𝑋 · 𝐵 ) − ( 𝐴 · 𝐵 ) ) )
24	22 23	oveq12d	⊢ ( 𝜑 → ( ( ( 𝐵 − 𝑋 ) · 𝐴 ) + ( ( 𝑋 − 𝐴 ) · 𝐵 ) ) = ( ( ( 𝐵 · 𝐴 ) − ( 𝑋 · 𝐴 ) ) + ( ( 𝑋 · 𝐵 ) − ( 𝐴 · 𝐵 ) ) ) )
25	3 2 1	subdid	⊢ ( 𝜑 → ( 𝑋 · ( 𝐵 − 𝐴 ) ) = ( ( 𝑋 · 𝐵 ) − ( 𝑋 · 𝐴 ) ) )
26	21 24 25	3eqtr4rd	⊢ ( 𝜑 → ( 𝑋 · ( 𝐵 − 𝐴 ) ) = ( ( ( 𝐵 − 𝑋 ) · 𝐴 ) + ( ( 𝑋 − 𝐴 ) · 𝐵 ) ) )
27	26	oveq1d	⊢ ( 𝜑 → ( ( 𝑋 · ( 𝐵 − 𝐴 ) ) / ( 𝐵 − 𝐴 ) ) = ( ( ( ( 𝐵 − 𝑋 ) · 𝐴 ) + ( ( 𝑋 − 𝐴 ) · 𝐵 ) ) / ( 𝐵 − 𝐴 ) ) )
28	2 3	subcld	⊢ ( 𝜑 → ( 𝐵 − 𝑋 ) ∈ ℂ )
29	28 1	mulcld	⊢ ( 𝜑 → ( ( 𝐵 − 𝑋 ) · 𝐴 ) ∈ ℂ )
30	3 1	subcld	⊢ ( 𝜑 → ( 𝑋 − 𝐴 ) ∈ ℂ )
31	30 2	mulcld	⊢ ( 𝜑 → ( ( 𝑋 − 𝐴 ) · 𝐵 ) ∈ ℂ )
32	2 1	subcld	⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ∈ ℂ )
33	4	necomd	⊢ ( 𝜑 → 𝐵 ≠ 𝐴 )
34	2 1 33	subne0d	⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ≠ 0 )
35	29 31 32 34	divdird	⊢ ( 𝜑 → ( ( ( ( 𝐵 − 𝑋 ) · 𝐴 ) + ( ( 𝑋 − 𝐴 ) · 𝐵 ) ) / ( 𝐵 − 𝐴 ) ) = ( ( ( ( 𝐵 − 𝑋 ) · 𝐴 ) / ( 𝐵 − 𝐴 ) ) + ( ( ( 𝑋 − 𝐴 ) · 𝐵 ) / ( 𝐵 − 𝐴 ) ) ) )
36	27 35	eqtrd	⊢ ( 𝜑 → ( ( 𝑋 · ( 𝐵 − 𝐴 ) ) / ( 𝐵 − 𝐴 ) ) = ( ( ( ( 𝐵 − 𝑋 ) · 𝐴 ) / ( 𝐵 − 𝐴 ) ) + ( ( ( 𝑋 − 𝐴 ) · 𝐵 ) / ( 𝐵 − 𝐴 ) ) ) )
37	3 32 34	divcan4d	⊢ ( 𝜑 → ( ( 𝑋 · ( 𝐵 − 𝐴 ) ) / ( 𝐵 − 𝐴 ) ) = 𝑋 )
38	28 1 32 34	div23d	⊢ ( 𝜑 → ( ( ( 𝐵 − 𝑋 ) · 𝐴 ) / ( 𝐵 − 𝐴 ) ) = ( ( ( 𝐵 − 𝑋 ) / ( 𝐵 − 𝐴 ) ) · 𝐴 ) )
39	30 2 32 34	div23d	⊢ ( 𝜑 → ( ( ( 𝑋 − 𝐴 ) · 𝐵 ) / ( 𝐵 − 𝐴 ) ) = ( ( ( 𝑋 − 𝐴 ) / ( 𝐵 − 𝐴 ) ) · 𝐵 ) )
40	38 39	oveq12d	⊢ ( 𝜑 → ( ( ( ( 𝐵 − 𝑋 ) · 𝐴 ) / ( 𝐵 − 𝐴 ) ) + ( ( ( 𝑋 − 𝐴 ) · 𝐵 ) / ( 𝐵 − 𝐴 ) ) ) = ( ( ( ( 𝐵 − 𝑋 ) / ( 𝐵 − 𝐴 ) ) · 𝐴 ) + ( ( ( 𝑋 − 𝐴 ) / ( 𝐵 − 𝐴 ) ) · 𝐵 ) ) )
41	36 37 40	3eqtr3d	⊢ ( 𝜑 → 𝑋 = ( ( ( ( 𝐵 − 𝑋 ) / ( 𝐵 − 𝐴 ) ) · 𝐴 ) + ( ( ( 𝑋 − 𝐴 ) / ( 𝐵 − 𝐴 ) ) · 𝐵 ) ) )