Theorem affinecomb2

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

	Ref	Expression
Hypotheses	affinecomb1.a	$$⊢\phi \to A\in ℝ$$
	affinecomb1.b	$$⊢\phi \to B\in ℝ$$
	affinecomb1.c	$$⊢\phi \to C\in ℝ$$
	affinecomb1.d	$$⊢\phi \to B\ne C$$
	affinecomb1.e	$$⊢\phi \to E\in ℝ$$
	affinecomb1.f	$$⊢\phi \to F\in ℝ$$
	affinecomb1.g	$$⊢\phi \to G\in ℝ$$
Assertion	affinecomb2	$$⊢\phi \to \left(\exists t\in ℝ\left(A=\left(1-t\right)B+tC\wedge E=\left(1-t\right)F+tG\right)\leftrightarrow \left(C-B\right)E=\left(G-F\right)A+FC-BG\right)$$

Proof

Step	Hyp	Ref	Expression
1		affinecomb1.a	$$⊢\phi \to A\in ℝ$$
2		affinecomb1.b	$$⊢\phi \to B\in ℝ$$
3		affinecomb1.c	$$⊢\phi \to C\in ℝ$$
4		affinecomb1.d	$$⊢\phi \to B\ne C$$
5		affinecomb1.e	$$⊢\phi \to E\in ℝ$$
6		affinecomb1.f	$$⊢\phi \to F\in ℝ$$
7		affinecomb1.g	$$⊢\phi \to G\in ℝ$$
8		eqid	$$⊢\frac{G-F}{C-B}=\frac{G-F}{C-B}$$
9	1 2 3 4 5 6 7 8	affinecomb1	$$⊢\phi \to \left(\exists t\in ℝ\left(A=\left(1-t\right)B+tC\wedge E=\left(1-t\right)F+tG\right)\leftrightarrow E=\left(\frac{G-F}{C-B}\right)\left(A-B\right)+F\right)$$
10	5	recnd	$$⊢\phi \to E\in ℂ$$
11	7	recnd	$$⊢\phi \to G\in ℂ$$
12	6	recnd	$$⊢\phi \to F\in ℂ$$
13	11 12	subcld	$$⊢\phi \to G-F\in ℂ$$
14	3	recnd	$$⊢\phi \to C\in ℂ$$
15	2	recnd	$$⊢\phi \to B\in ℂ$$
16	14 15	subcld	$$⊢\phi \to C-B\in ℂ$$
17	4	necomd	$$⊢\phi \to C\ne B$$
18	14 15 17	subne0d	$$⊢\phi \to C-B\ne 0$$
19	13 16 18	divcld	$$⊢\phi \to \frac{G-F}{C-B}\in ℂ$$
20	1	recnd	$$⊢\phi \to A\in ℂ$$
21	20 15	subcld	$$⊢\phi \to A-B\in ℂ$$
22	19 21	mulcld	$$⊢\phi \to \left(\frac{G-F}{C-B}\right)\left(A-B\right)\in ℂ$$
23	22 12	addcld	$$⊢\phi \to \left(\frac{G-F}{C-B}\right)\left(A-B\right)+F\in ℂ$$
24	10 23 16 18	mulcand	$$⊢\phi \to \left(\left(C-B\right)E=\left(C-B\right)\left(\left(\frac{G-F}{C-B}\right)\left(A-B\right)+F\right)\leftrightarrow E=\left(\frac{G-F}{C-B}\right)\left(A-B\right)+F\right)$$
25	16 22 12	adddid	$$⊢\phi \to \left(C-B\right)\left(\left(\frac{G-F}{C-B}\right)\left(A-B\right)+F\right)=\left(C-B\right)\left(\frac{G-F}{C-B}\right)\left(A-B\right)+\left(C-B\right)F$$
26	13 16 18	divcan2d	$$⊢\phi \to \left(C-B\right)\left(\frac{G-F}{C-B}\right)=G-F$$
27	26	oveq1d	$$⊢\phi \to \left(C-B\right)\left(\frac{G-F}{C-B}\right)\left(A-B\right)=\left(G-F\right)\left(A-B\right)$$
28	16 19 21	mulassd	$$⊢\phi \to \left(C-B\right)\left(\frac{G-F}{C-B}\right)\left(A-B\right)=\left(C-B\right)\left(\frac{G-F}{C-B}\right)\left(A-B\right)$$
29	13 20 15	subdid	$$⊢\phi \to \left(G-F\right)\left(A-B\right)=\left(G-F\right)A-\left(G-F\right)B$$
30	27 28 29	3eqtr3d	$$⊢\phi \to \left(C-B\right)\left(\frac{G-F}{C-B}\right)\left(A-B\right)=\left(G-F\right)A-\left(G-F\right)B$$
31	14 15 12	subdird	$$⊢\phi \to \left(C-B\right)F=CF-BF$$
32	30 31	oveq12d	$$⊢\phi \to \left(C-B\right)\left(\frac{G-F}{C-B}\right)\left(A-B\right)+\left(C-B\right)F=\left(\left(G-F\right)A-\left(G-F\right)B\right)+CF-BF$$
33	13 20	mulcld	$$⊢\phi \to \left(G-F\right)A\in ℂ$$
34	13 15	mulcld	$$⊢\phi \to \left(G-F\right)B\in ℂ$$
35	14 12	mulcld	$$⊢\phi \to CF\in ℂ$$
36	15 12	mulcld	$$⊢\phi \to BF\in ℂ$$
37	35 36	subcld	$$⊢\phi \to CF-BF\in ℂ$$
38	33 34 37	subadd23d	$$⊢\phi \to \left(\left(G-F\right)A-\left(G-F\right)B\right)+CF-BF=\left(G-F\right)A+\left(CF-BF\right)-\left(G-F\right)B$$
39	32 38	eqtrd	$$⊢\phi \to \left(C-B\right)\left(\frac{G-F}{C-B}\right)\left(A-B\right)+\left(C-B\right)F=\left(G-F\right)A+\left(CF-BF\right)-\left(G-F\right)B$$
40	14 12	mulcomd	$$⊢\phi \to CF=FC$$
41	15 12	mulcomd	$$⊢\phi \to BF=FB$$
42	40 41	oveq12d	$$⊢\phi \to CF-BF=FC-FB$$
43	11 12 15	subdird	$$⊢\phi \to \left(G-F\right)B=GB-FB$$
44	42 43	oveq12d	$$⊢\phi \to CF-BF-\left(G-F\right)B=FC-FB-\left(GB-FB\right)$$
45	12 14	mulcld	$$⊢\phi \to FC\in ℂ$$
46	11 15	mulcld	$$⊢\phi \to GB\in ℂ$$
47	12 15	mulcld	$$⊢\phi \to FB\in ℂ$$
48	45 46 47	nnncan2d	$$⊢\phi \to FC-FB-\left(GB-FB\right)=FC-GB$$
49	11 15	mulcomd	$$⊢\phi \to GB=BG$$
50	49	oveq2d	$$⊢\phi \to FC-GB=FC-BG$$
51	44 48 50	3eqtrd	$$⊢\phi \to CF-BF-\left(G-F\right)B=FC-BG$$
52	51	oveq2d	$$⊢\phi \to \left(G-F\right)A+\left(CF-BF\right)-\left(G-F\right)B=\left(G-F\right)A+FC-BG$$
53	25 39 52	3eqtrd	$$⊢\phi \to \left(C-B\right)\left(\left(\frac{G-F}{C-B}\right)\left(A-B\right)+F\right)=\left(G-F\right)A+FC-BG$$
54	53	eqeq2d	$$⊢\phi \to \left(\left(C-B\right)E=\left(C-B\right)\left(\left(\frac{G-F}{C-B}\right)\left(A-B\right)+F\right)\leftrightarrow \left(C-B\right)E=\left(G-F\right)A+FC-BG\right)$$
55	9 24 54	3bitr2d	$$⊢\phi \to \left(\exists t\in ℝ\left(A=\left(1-t\right)B+tC\wedge E=\left(1-t\right)F+tG\right)\leftrightarrow \left(C-B\right)E=\left(G-F\right)A+FC-BG\right)$$