Theorem affinecomb2

Description: Combination of two real affine combinations, presented without fraction. (Contributed by AV, 22-Jan-2023)

	Ref	Expression
Hypotheses	affinecomb1.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	affinecomb1.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	affinecomb1.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
	affinecomb1.d	⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
	affinecomb1.e	⊢ ( 𝜑 → 𝐸 ∈ ℝ )
	affinecomb1.f	⊢ ( 𝜑 → 𝐹 ∈ ℝ )
	affinecomb1.g	⊢ ( 𝜑 → 𝐺 ∈ ℝ )
Assertion	affinecomb2	⊢ ( 𝜑 → ( ∃ 𝑡 ∈ ℝ ( 𝐴 = ( ( ( 1 − 𝑡 ) · 𝐵 ) + ( 𝑡 · 𝐶 ) ) ∧ 𝐸 = ( ( ( 1 − 𝑡 ) · 𝐹 ) + ( 𝑡 · 𝐺 ) ) ) ↔ ( ( 𝐶 − 𝐵 ) · 𝐸 ) = ( ( ( 𝐺 − 𝐹 ) · 𝐴 ) + ( ( 𝐹 · 𝐶 ) − ( 𝐵 · 𝐺 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		affinecomb1.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		affinecomb1.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3		affinecomb1.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
4		affinecomb1.d	⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
5		affinecomb1.e	⊢ ( 𝜑 → 𝐸 ∈ ℝ )
6		affinecomb1.f	⊢ ( 𝜑 → 𝐹 ∈ ℝ )
7		affinecomb1.g	⊢ ( 𝜑 → 𝐺 ∈ ℝ )
8		eqid	⊢ ( ( 𝐺 − 𝐹 ) / ( 𝐶 − 𝐵 ) ) = ( ( 𝐺 − 𝐹 ) / ( 𝐶 − 𝐵 ) )
9	1 2 3 4 5 6 7 8	affinecomb1	⊢ ( 𝜑 → ( ∃ 𝑡 ∈ ℝ ( 𝐴 = ( ( ( 1 − 𝑡 ) · 𝐵 ) + ( 𝑡 · 𝐶 ) ) ∧ 𝐸 = ( ( ( 1 − 𝑡 ) · 𝐹 ) + ( 𝑡 · 𝐺 ) ) ) ↔ 𝐸 = ( ( ( ( 𝐺 − 𝐹 ) / ( 𝐶 − 𝐵 ) ) · ( 𝐴 − 𝐵 ) ) + 𝐹 ) ) )
10	5	recnd	⊢ ( 𝜑 → 𝐸 ∈ ℂ )
11	7	recnd	⊢ ( 𝜑 → 𝐺 ∈ ℂ )
12	6	recnd	⊢ ( 𝜑 → 𝐹 ∈ ℂ )
13	11 12	subcld	⊢ ( 𝜑 → ( 𝐺 − 𝐹 ) ∈ ℂ )
14	3	recnd	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
15	2	recnd	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
16	14 15	subcld	⊢ ( 𝜑 → ( 𝐶 − 𝐵 ) ∈ ℂ )
17	4	necomd	⊢ ( 𝜑 → 𝐶 ≠ 𝐵 )
18	14 15 17	subne0d	⊢ ( 𝜑 → ( 𝐶 − 𝐵 ) ≠ 0 )
19	13 16 18	divcld	⊢ ( 𝜑 → ( ( 𝐺 − 𝐹 ) / ( 𝐶 − 𝐵 ) ) ∈ ℂ )
20	1	recnd	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
21	20 15	subcld	⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) ∈ ℂ )
22	19 21	mulcld	⊢ ( 𝜑 → ( ( ( 𝐺 − 𝐹 ) / ( 𝐶 − 𝐵 ) ) · ( 𝐴 − 𝐵 ) ) ∈ ℂ )
23	22 12	addcld	⊢ ( 𝜑 → ( ( ( ( 𝐺 − 𝐹 ) / ( 𝐶 − 𝐵 ) ) · ( 𝐴 − 𝐵 ) ) + 𝐹 ) ∈ ℂ )
24	10 23 16 18	mulcand	⊢ ( 𝜑 → ( ( ( 𝐶 − 𝐵 ) · 𝐸 ) = ( ( 𝐶 − 𝐵 ) · ( ( ( ( 𝐺 − 𝐹 ) / ( 𝐶 − 𝐵 ) ) · ( 𝐴 − 𝐵 ) ) + 𝐹 ) ) ↔ 𝐸 = ( ( ( ( 𝐺 − 𝐹 ) / ( 𝐶 − 𝐵 ) ) · ( 𝐴 − 𝐵 ) ) + 𝐹 ) ) )
25	16 22 12	adddid	⊢ ( 𝜑 → ( ( 𝐶 − 𝐵 ) · ( ( ( ( 𝐺 − 𝐹 ) / ( 𝐶 − 𝐵 ) ) · ( 𝐴 − 𝐵 ) ) + 𝐹 ) ) = ( ( ( 𝐶 − 𝐵 ) · ( ( ( 𝐺 − 𝐹 ) / ( 𝐶 − 𝐵 ) ) · ( 𝐴 − 𝐵 ) ) ) + ( ( 𝐶 − 𝐵 ) · 𝐹 ) ) )
26	13 16 18	divcan2d	⊢ ( 𝜑 → ( ( 𝐶 − 𝐵 ) · ( ( 𝐺 − 𝐹 ) / ( 𝐶 − 𝐵 ) ) ) = ( 𝐺 − 𝐹 ) )
27	26	oveq1d	⊢ ( 𝜑 → ( ( ( 𝐶 − 𝐵 ) · ( ( 𝐺 − 𝐹 ) / ( 𝐶 − 𝐵 ) ) ) · ( 𝐴 − 𝐵 ) ) = ( ( 𝐺 − 𝐹 ) · ( 𝐴 − 𝐵 ) ) )
28	16 19 21	mulassd	⊢ ( 𝜑 → ( ( ( 𝐶 − 𝐵 ) · ( ( 𝐺 − 𝐹 ) / ( 𝐶 − 𝐵 ) ) ) · ( 𝐴 − 𝐵 ) ) = ( ( 𝐶 − 𝐵 ) · ( ( ( 𝐺 − 𝐹 ) / ( 𝐶 − 𝐵 ) ) · ( 𝐴 − 𝐵 ) ) ) )
29	13 20 15	subdid	⊢ ( 𝜑 → ( ( 𝐺 − 𝐹 ) · ( 𝐴 − 𝐵 ) ) = ( ( ( 𝐺 − 𝐹 ) · 𝐴 ) − ( ( 𝐺 − 𝐹 ) · 𝐵 ) ) )
30	27 28 29	3eqtr3d	⊢ ( 𝜑 → ( ( 𝐶 − 𝐵 ) · ( ( ( 𝐺 − 𝐹 ) / ( 𝐶 − 𝐵 ) ) · ( 𝐴 − 𝐵 ) ) ) = ( ( ( 𝐺 − 𝐹 ) · 𝐴 ) − ( ( 𝐺 − 𝐹 ) · 𝐵 ) ) )
31	14 15 12	subdird	⊢ ( 𝜑 → ( ( 𝐶 − 𝐵 ) · 𝐹 ) = ( ( 𝐶 · 𝐹 ) − ( 𝐵 · 𝐹 ) ) )
32	30 31	oveq12d	⊢ ( 𝜑 → ( ( ( 𝐶 − 𝐵 ) · ( ( ( 𝐺 − 𝐹 ) / ( 𝐶 − 𝐵 ) ) · ( 𝐴 − 𝐵 ) ) ) + ( ( 𝐶 − 𝐵 ) · 𝐹 ) ) = ( ( ( ( 𝐺 − 𝐹 ) · 𝐴 ) − ( ( 𝐺 − 𝐹 ) · 𝐵 ) ) + ( ( 𝐶 · 𝐹 ) − ( 𝐵 · 𝐹 ) ) ) )
33	13 20	mulcld	⊢ ( 𝜑 → ( ( 𝐺 − 𝐹 ) · 𝐴 ) ∈ ℂ )
34	13 15	mulcld	⊢ ( 𝜑 → ( ( 𝐺 − 𝐹 ) · 𝐵 ) ∈ ℂ )
35	14 12	mulcld	⊢ ( 𝜑 → ( 𝐶 · 𝐹 ) ∈ ℂ )
36	15 12	mulcld	⊢ ( 𝜑 → ( 𝐵 · 𝐹 ) ∈ ℂ )
37	35 36	subcld	⊢ ( 𝜑 → ( ( 𝐶 · 𝐹 ) − ( 𝐵 · 𝐹 ) ) ∈ ℂ )
38	33 34 37	subadd23d	⊢ ( 𝜑 → ( ( ( ( 𝐺 − 𝐹 ) · 𝐴 ) − ( ( 𝐺 − 𝐹 ) · 𝐵 ) ) + ( ( 𝐶 · 𝐹 ) − ( 𝐵 · 𝐹 ) ) ) = ( ( ( 𝐺 − 𝐹 ) · 𝐴 ) + ( ( ( 𝐶 · 𝐹 ) − ( 𝐵 · 𝐹 ) ) − ( ( 𝐺 − 𝐹 ) · 𝐵 ) ) ) )
39	32 38	eqtrd	⊢ ( 𝜑 → ( ( ( 𝐶 − 𝐵 ) · ( ( ( 𝐺 − 𝐹 ) / ( 𝐶 − 𝐵 ) ) · ( 𝐴 − 𝐵 ) ) ) + ( ( 𝐶 − 𝐵 ) · 𝐹 ) ) = ( ( ( 𝐺 − 𝐹 ) · 𝐴 ) + ( ( ( 𝐶 · 𝐹 ) − ( 𝐵 · 𝐹 ) ) − ( ( 𝐺 − 𝐹 ) · 𝐵 ) ) ) )
40	14 12	mulcomd	⊢ ( 𝜑 → ( 𝐶 · 𝐹 ) = ( 𝐹 · 𝐶 ) )
41	15 12	mulcomd	⊢ ( 𝜑 → ( 𝐵 · 𝐹 ) = ( 𝐹 · 𝐵 ) )
42	40 41	oveq12d	⊢ ( 𝜑 → ( ( 𝐶 · 𝐹 ) − ( 𝐵 · 𝐹 ) ) = ( ( 𝐹 · 𝐶 ) − ( 𝐹 · 𝐵 ) ) )
43	11 12 15	subdird	⊢ ( 𝜑 → ( ( 𝐺 − 𝐹 ) · 𝐵 ) = ( ( 𝐺 · 𝐵 ) − ( 𝐹 · 𝐵 ) ) )
44	42 43	oveq12d	⊢ ( 𝜑 → ( ( ( 𝐶 · 𝐹 ) − ( 𝐵 · 𝐹 ) ) − ( ( 𝐺 − 𝐹 ) · 𝐵 ) ) = ( ( ( 𝐹 · 𝐶 ) − ( 𝐹 · 𝐵 ) ) − ( ( 𝐺 · 𝐵 ) − ( 𝐹 · 𝐵 ) ) ) )
45	12 14	mulcld	⊢ ( 𝜑 → ( 𝐹 · 𝐶 ) ∈ ℂ )
46	11 15	mulcld	⊢ ( 𝜑 → ( 𝐺 · 𝐵 ) ∈ ℂ )
47	12 15	mulcld	⊢ ( 𝜑 → ( 𝐹 · 𝐵 ) ∈ ℂ )
48	45 46 47	nnncan2d	⊢ ( 𝜑 → ( ( ( 𝐹 · 𝐶 ) − ( 𝐹 · 𝐵 ) ) − ( ( 𝐺 · 𝐵 ) − ( 𝐹 · 𝐵 ) ) ) = ( ( 𝐹 · 𝐶 ) − ( 𝐺 · 𝐵 ) ) )
49	11 15	mulcomd	⊢ ( 𝜑 → ( 𝐺 · 𝐵 ) = ( 𝐵 · 𝐺 ) )
50	49	oveq2d	⊢ ( 𝜑 → ( ( 𝐹 · 𝐶 ) − ( 𝐺 · 𝐵 ) ) = ( ( 𝐹 · 𝐶 ) − ( 𝐵 · 𝐺 ) ) )
51	44 48 50	3eqtrd	⊢ ( 𝜑 → ( ( ( 𝐶 · 𝐹 ) − ( 𝐵 · 𝐹 ) ) − ( ( 𝐺 − 𝐹 ) · 𝐵 ) ) = ( ( 𝐹 · 𝐶 ) − ( 𝐵 · 𝐺 ) ) )
52	51	oveq2d	⊢ ( 𝜑 → ( ( ( 𝐺 − 𝐹 ) · 𝐴 ) + ( ( ( 𝐶 · 𝐹 ) − ( 𝐵 · 𝐹 ) ) − ( ( 𝐺 − 𝐹 ) · 𝐵 ) ) ) = ( ( ( 𝐺 − 𝐹 ) · 𝐴 ) + ( ( 𝐹 · 𝐶 ) − ( 𝐵 · 𝐺 ) ) ) )
53	25 39 52	3eqtrd	⊢ ( 𝜑 → ( ( 𝐶 − 𝐵 ) · ( ( ( ( 𝐺 − 𝐹 ) / ( 𝐶 − 𝐵 ) ) · ( 𝐴 − 𝐵 ) ) + 𝐹 ) ) = ( ( ( 𝐺 − 𝐹 ) · 𝐴 ) + ( ( 𝐹 · 𝐶 ) − ( 𝐵 · 𝐺 ) ) ) )
54	53	eqeq2d	⊢ ( 𝜑 → ( ( ( 𝐶 − 𝐵 ) · 𝐸 ) = ( ( 𝐶 − 𝐵 ) · ( ( ( ( 𝐺 − 𝐹 ) / ( 𝐶 − 𝐵 ) ) · ( 𝐴 − 𝐵 ) ) + 𝐹 ) ) ↔ ( ( 𝐶 − 𝐵 ) · 𝐸 ) = ( ( ( 𝐺 − 𝐹 ) · 𝐴 ) + ( ( 𝐹 · 𝐶 ) − ( 𝐵 · 𝐺 ) ) ) ) )
55	9 24 54	3bitr2d	⊢ ( 𝜑 → ( ∃ 𝑡 ∈ ℝ ( 𝐴 = ( ( ( 1 − 𝑡 ) · 𝐵 ) + ( 𝑡 · 𝐶 ) ) ∧ 𝐸 = ( ( ( 1 − 𝑡 ) · 𝐹 ) + ( 𝑡 · 𝐺 ) ) ) ↔ ( ( 𝐶 − 𝐵 ) · 𝐸 ) = ( ( ( 𝐺 − 𝐹 ) · 𝐴 ) + ( ( 𝐹 · 𝐶 ) − ( 𝐵 · 𝐺 ) ) ) ) )