Metamath Proof Explorer

Theorem affinecomb1

Description: Combination of two real affine combinations, one class variable resolved. (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 ∈ ℝ
affinecomb1.s ⊢ S = G − F C − B
Assertion affinecomb1 ⊢ φ → ∃ t ∈ ℝ A = 1 − t ⁢ B + t ⁢ C ∧ E = 1 − t ⁢ F + t ⁢ G ↔ E = S ⁢ A − B + F

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