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 ( 𝜑𝐴 ∈ ℝ )
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 − 𝑡 ) · 𝐹 ) + ( 𝑡 · 𝐺 ) ) ) ↔ 𝐸 = ( ( 𝑆 · ( 𝐴𝐵 ) ) + 𝐹 ) ) )