Theorem affinecomb1

Description: Combination of two real affine combinations, one class variable resolved. (Contributed by AV, 22-Jan-2023)

	Ref	Expression
Hypotheses	affinecomb1.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	affinecomb1.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	affinecomb1.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
	affinecomb1.d	⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
	affinecomb1.e	⊢ ( 𝜑 → 𝐸 ∈ ℝ )
	affinecomb1.f	⊢ ( 𝜑 → 𝐹 ∈ ℝ )
	affinecomb1.g	⊢ ( 𝜑 → 𝐺 ∈ ℝ )
	affinecomb1.s	⊢ 𝑆 = ( ( 𝐺 − 𝐹 ) / ( 𝐶 − 𝐵 ) )
Assertion	affinecomb1	⊢ ( 𝜑 → ( ∃ 𝑡 ∈ ℝ ( 𝐴 = ( ( ( 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		affinecomb1.s	⊢ 𝑆 = ( ( 𝐺 − 𝐹 ) / ( 𝐶 − 𝐵 ) )
9	1	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → 𝐴 ∈ ℝ )
10	9	recnd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → 𝐴 ∈ ℂ )
11	2	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → 𝐵 ∈ ℝ )
12	11	recnd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → 𝐵 ∈ ℂ )
13	3	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → 𝐶 ∈ ℝ )
14	13	recnd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → 𝐶 ∈ ℂ )
15		simpr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → 𝑡 ∈ ℝ )
16	15	recnd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → 𝑡 ∈ ℂ )
17	4	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → 𝐵 ≠ 𝐶 )
18	10 12 14 16 17	affineequivne	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → ( 𝐴 = ( ( ( 1 − 𝑡 ) · 𝐵 ) + ( 𝑡 · 𝐶 ) ) ↔ 𝑡 = ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) ) )
19		oveq2	⊢ ( 𝑡 = ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) → ( 1 − 𝑡 ) = ( 1 − ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) ) )
20	19	oveq1d	⊢ ( 𝑡 = ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) → ( ( 1 − 𝑡 ) · 𝐹 ) = ( ( 1 − ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) ) · 𝐹 ) )
21		oveq1	⊢ ( 𝑡 = ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) → ( 𝑡 · 𝐺 ) = ( ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) · 𝐺 ) )
22	20 21	oveq12d	⊢ ( 𝑡 = ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) → ( ( ( 1 − 𝑡 ) · 𝐹 ) + ( 𝑡 · 𝐺 ) ) = ( ( ( 1 − ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) ) · 𝐹 ) + ( ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) · 𝐺 ) ) )
23	22	eqeq2d	⊢ ( 𝑡 = ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) → ( 𝐸 = ( ( ( 1 − 𝑡 ) · 𝐹 ) + ( 𝑡 · 𝐺 ) ) ↔ 𝐸 = ( ( ( 1 − ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) ) · 𝐹 ) + ( ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) · 𝐺 ) ) ) )
24	23	adantl	⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 = ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) ) → ( 𝐸 = ( ( ( 1 − 𝑡 ) · 𝐹 ) + ( 𝑡 · 𝐺 ) ) ↔ 𝐸 = ( ( ( 1 − ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) ) · 𝐹 ) + ( ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) · 𝐺 ) ) ) )
25		eqidd	⊢ ( 𝜑 → ( ( ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) · ( 𝐺 − 𝐹 ) ) + 𝐹 ) = ( ( ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) · ( 𝐺 − 𝐹 ) ) + 𝐹 ) )
26	1 2	resubcld	⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) ∈ ℝ )
27	3 2	resubcld	⊢ ( 𝜑 → ( 𝐶 − 𝐵 ) ∈ ℝ )
28	3	recnd	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
29	2	recnd	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
30	4	necomd	⊢ ( 𝜑 → 𝐶 ≠ 𝐵 )
31	28 29 30	subne0d	⊢ ( 𝜑 → ( 𝐶 − 𝐵 ) ≠ 0 )
32	26 27 31	redivcld	⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) ∈ ℝ )
33	7 6	resubcld	⊢ ( 𝜑 → ( 𝐺 − 𝐹 ) ∈ ℝ )
34	32 33	remulcld	⊢ ( 𝜑 → ( ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) · ( 𝐺 − 𝐹 ) ) ∈ ℝ )
35	34 6	readdcld	⊢ ( 𝜑 → ( ( ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) · ( 𝐺 − 𝐹 ) ) + 𝐹 ) ∈ ℝ )
36	35	recnd	⊢ ( 𝜑 → ( ( ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) · ( 𝐺 − 𝐹 ) ) + 𝐹 ) ∈ ℂ )
37	6	recnd	⊢ ( 𝜑 → 𝐹 ∈ ℂ )
38	7	recnd	⊢ ( 𝜑 → 𝐺 ∈ ℂ )
39	32	recnd	⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) ∈ ℂ )
40	36 37 38 39	affineequiv4	⊢ ( 𝜑 → ( ( ( ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) · ( 𝐺 − 𝐹 ) ) + 𝐹 ) = ( ( ( 1 − ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) ) · 𝐹 ) + ( ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) · 𝐺 ) ) ↔ ( ( ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) · ( 𝐺 − 𝐹 ) ) + 𝐹 ) = ( ( ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) · ( 𝐺 − 𝐹 ) ) + 𝐹 ) ) )
41	25 40	mpbird	⊢ ( 𝜑 → ( ( ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) · ( 𝐺 − 𝐹 ) ) + 𝐹 ) = ( ( ( 1 − ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) ) · 𝐹 ) + ( ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) · 𝐺 ) ) )
42	26	recnd	⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) ∈ ℂ )
43	27	recnd	⊢ ( 𝜑 → ( 𝐶 − 𝐵 ) ∈ ℂ )
44	33	recnd	⊢ ( 𝜑 → ( 𝐺 − 𝐹 ) ∈ ℂ )
45	42 43 44 31	div13d	⊢ ( 𝜑 → ( ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) · ( 𝐺 − 𝐹 ) ) = ( ( ( 𝐺 − 𝐹 ) / ( 𝐶 − 𝐵 ) ) · ( 𝐴 − 𝐵 ) ) )
46	8	oveq1i	⊢ ( 𝑆 · ( 𝐴 − 𝐵 ) ) = ( ( ( 𝐺 − 𝐹 ) / ( 𝐶 − 𝐵 ) ) · ( 𝐴 − 𝐵 ) )
47	45 46	eqtr4di	⊢ ( 𝜑 → ( ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) · ( 𝐺 − 𝐹 ) ) = ( 𝑆 · ( 𝐴 − 𝐵 ) ) )
48	47	oveq1d	⊢ ( 𝜑 → ( ( ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) · ( 𝐺 − 𝐹 ) ) + 𝐹 ) = ( ( 𝑆 · ( 𝐴 − 𝐵 ) ) + 𝐹 ) )
49	41 48	eqtr3d	⊢ ( 𝜑 → ( ( ( 1 − ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) ) · 𝐹 ) + ( ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) · 𝐺 ) ) = ( ( 𝑆 · ( 𝐴 − 𝐵 ) ) + 𝐹 ) )
50	49	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → ( ( ( 1 − ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) ) · 𝐹 ) + ( ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) · 𝐺 ) ) = ( ( 𝑆 · ( 𝐴 − 𝐵 ) ) + 𝐹 ) )
51	50	eqeq2d	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → ( 𝐸 = ( ( ( 1 − ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) ) · 𝐹 ) + ( ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) · 𝐺 ) ) ↔ 𝐸 = ( ( 𝑆 · ( 𝐴 − 𝐵 ) ) + 𝐹 ) ) )
52	51	biimpd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → ( 𝐸 = ( ( ( 1 − ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) ) · 𝐹 ) + ( ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) · 𝐺 ) ) → 𝐸 = ( ( 𝑆 · ( 𝐴 − 𝐵 ) ) + 𝐹 ) ) )
53	52	adantr	⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 = ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) ) → ( 𝐸 = ( ( ( 1 − ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) ) · 𝐹 ) + ( ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) · 𝐺 ) ) → 𝐸 = ( ( 𝑆 · ( 𝐴 − 𝐵 ) ) + 𝐹 ) ) )
54	24 53	sylbid	⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 = ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) ) → ( 𝐸 = ( ( ( 1 − 𝑡 ) · 𝐹 ) + ( 𝑡 · 𝐺 ) ) → 𝐸 = ( ( 𝑆 · ( 𝐴 − 𝐵 ) ) + 𝐹 ) ) )
55	54	ex	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → ( 𝑡 = ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) → ( 𝐸 = ( ( ( 1 − 𝑡 ) · 𝐹 ) + ( 𝑡 · 𝐺 ) ) → 𝐸 = ( ( 𝑆 · ( 𝐴 − 𝐵 ) ) + 𝐹 ) ) ) )
56	18 55	sylbid	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → ( 𝐴 = ( ( ( 1 − 𝑡 ) · 𝐵 ) + ( 𝑡 · 𝐶 ) ) → ( 𝐸 = ( ( ( 1 − 𝑡 ) · 𝐹 ) + ( 𝑡 · 𝐺 ) ) → 𝐸 = ( ( 𝑆 · ( 𝐴 − 𝐵 ) ) + 𝐹 ) ) ) )
57	56	impd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → ( ( 𝐴 = ( ( ( 1 − 𝑡 ) · 𝐵 ) + ( 𝑡 · 𝐶 ) ) ∧ 𝐸 = ( ( ( 1 − 𝑡 ) · 𝐹 ) + ( 𝑡 · 𝐺 ) ) ) → 𝐸 = ( ( 𝑆 · ( 𝐴 − 𝐵 ) ) + 𝐹 ) ) )
58	57	rexlimdva	⊢ ( 𝜑 → ( ∃ 𝑡 ∈ ℝ ( 𝐴 = ( ( ( 1 − 𝑡 ) · 𝐵 ) + ( 𝑡 · 𝐶 ) ) ∧ 𝐸 = ( ( ( 1 − 𝑡 ) · 𝐹 ) + ( 𝑡 · 𝐺 ) ) ) → 𝐸 = ( ( 𝑆 · ( 𝐴 − 𝐵 ) ) + 𝐹 ) ) )
59	5	adantr	⊢ ( ( 𝜑 ∧ 𝑡 = ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) ) → 𝐸 ∈ ℝ )
60	59	recnd	⊢ ( ( 𝜑 ∧ 𝑡 = ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) ) → 𝐸 ∈ ℂ )
61	37	adantr	⊢ ( ( 𝜑 ∧ 𝑡 = ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) ) → 𝐹 ∈ ℂ )
62	38	adantr	⊢ ( ( 𝜑 ∧ 𝑡 = ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) ) → 𝐺 ∈ ℂ )
63	32	adantr	⊢ ( ( 𝜑 ∧ 𝑡 = ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) ) → ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) ∈ ℝ )
64		eleq1	⊢ ( 𝑡 = ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) → ( 𝑡 ∈ ℝ ↔ ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) ∈ ℝ ) )
65	64	adantl	⊢ ( ( 𝜑 ∧ 𝑡 = ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) ) → ( 𝑡 ∈ ℝ ↔ ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) ∈ ℝ ) )
66	63 65	mpbird	⊢ ( ( 𝜑 ∧ 𝑡 = ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) ) → 𝑡 ∈ ℝ )
67	66	recnd	⊢ ( ( 𝜑 ∧ 𝑡 = ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) ) → 𝑡 ∈ ℂ )
68	60 61 62 67	affineequiv4	⊢ ( ( 𝜑 ∧ 𝑡 = ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) ) → ( 𝐸 = ( ( ( 1 − 𝑡 ) · 𝐹 ) + ( 𝑡 · 𝐺 ) ) ↔ 𝐸 = ( ( 𝑡 · ( 𝐺 − 𝐹 ) ) + 𝐹 ) ) )
69	19	oveq1d	⊢ ( 𝑡 = ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) → ( ( 1 − 𝑡 ) · 𝐵 ) = ( ( 1 − ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) ) · 𝐵 ) )
70		oveq1	⊢ ( 𝑡 = ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) → ( 𝑡 · 𝐶 ) = ( ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) · 𝐶 ) )
71	69 70	oveq12d	⊢ ( 𝑡 = ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) → ( ( ( 1 − 𝑡 ) · 𝐵 ) + ( 𝑡 · 𝐶 ) ) = ( ( ( 1 − ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) ) · 𝐵 ) + ( ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) · 𝐶 ) ) )
72		eqidd	⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) = ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) )
73	1	recnd	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
74	73 29 28 39 4	affineequivne	⊢ ( 𝜑 → ( 𝐴 = ( ( ( 1 − ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) ) · 𝐵 ) + ( ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) · 𝐶 ) ) ↔ ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) = ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) ) )
75	72 74	mpbird	⊢ ( 𝜑 → 𝐴 = ( ( ( 1 − ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) ) · 𝐵 ) + ( ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) · 𝐶 ) ) )
76	75	eqcomd	⊢ ( 𝜑 → ( ( ( 1 − ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) ) · 𝐵 ) + ( ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) · 𝐶 ) ) = 𝐴 )
77	71 76	sylan9eqr	⊢ ( ( 𝜑 ∧ 𝑡 = ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) ) → ( ( ( 1 − 𝑡 ) · 𝐵 ) + ( 𝑡 · 𝐶 ) ) = 𝐴 )
78	77	eqcomd	⊢ ( ( 𝜑 ∧ 𝑡 = ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) ) → 𝐴 = ( ( ( 1 − 𝑡 ) · 𝐵 ) + ( 𝑡 · 𝐶 ) ) )
79	78	biantrurd	⊢ ( ( 𝜑 ∧ 𝑡 = ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) ) → ( 𝐸 = ( ( ( 1 − 𝑡 ) · 𝐹 ) + ( 𝑡 · 𝐺 ) ) ↔ ( 𝐴 = ( ( ( 1 − 𝑡 ) · 𝐵 ) + ( 𝑡 · 𝐶 ) ) ∧ 𝐸 = ( ( ( 1 − 𝑡 ) · 𝐹 ) + ( 𝑡 · 𝐺 ) ) ) ) )
80	45	adantr	⊢ ( ( 𝜑 ∧ 𝑡 = ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) ) → ( ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) · ( 𝐺 − 𝐹 ) ) = ( ( ( 𝐺 − 𝐹 ) / ( 𝐶 − 𝐵 ) ) · ( 𝐴 − 𝐵 ) ) )
81		oveq1	⊢ ( 𝑡 = ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) → ( 𝑡 · ( 𝐺 − 𝐹 ) ) = ( ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) · ( 𝐺 − 𝐹 ) ) )
82	81	adantl	⊢ ( ( 𝜑 ∧ 𝑡 = ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) ) → ( 𝑡 · ( 𝐺 − 𝐹 ) ) = ( ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) · ( 𝐺 − 𝐹 ) ) )
83	46	a1i	⊢ ( ( 𝜑 ∧ 𝑡 = ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) ) → ( 𝑆 · ( 𝐴 − 𝐵 ) ) = ( ( ( 𝐺 − 𝐹 ) / ( 𝐶 − 𝐵 ) ) · ( 𝐴 − 𝐵 ) ) )
84	80 82 83	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑡 = ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) ) → ( 𝑡 · ( 𝐺 − 𝐹 ) ) = ( 𝑆 · ( 𝐴 − 𝐵 ) ) )
85	84	oveq1d	⊢ ( ( 𝜑 ∧ 𝑡 = ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) ) → ( ( 𝑡 · ( 𝐺 − 𝐹 ) ) + 𝐹 ) = ( ( 𝑆 · ( 𝐴 − 𝐵 ) ) + 𝐹 ) )
86	85	eqeq2d	⊢ ( ( 𝜑 ∧ 𝑡 = ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) ) → ( 𝐸 = ( ( 𝑡 · ( 𝐺 − 𝐹 ) ) + 𝐹 ) ↔ 𝐸 = ( ( 𝑆 · ( 𝐴 − 𝐵 ) ) + 𝐹 ) ) )
87	68 79 86	3bitr3d	⊢ ( ( 𝜑 ∧ 𝑡 = ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) ) → ( ( 𝐴 = ( ( ( 1 − 𝑡 ) · 𝐵 ) + ( 𝑡 · 𝐶 ) ) ∧ 𝐸 = ( ( ( 1 − 𝑡 ) · 𝐹 ) + ( 𝑡 · 𝐺 ) ) ) ↔ 𝐸 = ( ( 𝑆 · ( 𝐴 − 𝐵 ) ) + 𝐹 ) ) )
88	32 87	rspcedv	⊢ ( 𝜑 → ( 𝐸 = ( ( 𝑆 · ( 𝐴 − 𝐵 ) ) + 𝐹 ) → ∃ 𝑡 ∈ ℝ ( 𝐴 = ( ( ( 1 − 𝑡 ) · 𝐵 ) + ( 𝑡 · 𝐶 ) ) ∧ 𝐸 = ( ( ( 1 − 𝑡 ) · 𝐹 ) + ( 𝑡 · 𝐺 ) ) ) ) )
89	58 88	impbid	⊢ ( 𝜑 → ( ∃ 𝑡 ∈ ℝ ( 𝐴 = ( ( ( 1 − 𝑡 ) · 𝐵 ) + ( 𝑡 · 𝐶 ) ) ∧ 𝐸 = ( ( ( 1 − 𝑡 ) · 𝐹 ) + ( 𝑡 · 𝐺 ) ) ) ↔ 𝐸 = ( ( 𝑆 · ( 𝐴 − 𝐵 ) ) + 𝐹 ) ) )