Metamath Proof Explorer

Theorem affinecomb2

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

Ref Expression
Hypotheses affinecomb1.a ⊢ φ → A ∈ ℝ
affinecomb1.b ⊢ φ → B ∈ ℝ
affinecomb1.c ⊢ φ → C ∈ ℝ
affinecomb1.d ⊢ φ → B ≠ C
affinecomb1.e ⊢ φ → E ∈ ℝ
affinecomb1.f ⊢ φ → F ∈ ℝ
affinecomb1.g ⊢ φ → G ∈ ℝ
Assertion affinecomb2 ⊢ φ → ∃ t ∈ ℝ A = 1 − t ⁢ B + t ⁢ C ∧ E = 1 − t ⁢ F + t ⁢ G ↔ C − B ⁢ E = G − F ⁢ A + F ⁢ C - B ⁢ G

Proof

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