Description: Exponential growth and decay model. The derivative of a functiony of variablet equals a constantk timesy itself, iffy equals some constantC times the exponential ofkt. This theorem and expgrowthi illustrate one of the simplest and most crucial classes of differential equations, equations that relate functions to their derivatives.
Section 6.3 of Strang p. 242 callsy' =ky "the most important differential equation in applied mathematics". In the field of population ecology it is known as theMalthusian growth model or exponential law, andC,k, andt correspond to initial population size, growth rate, and time respectively ( https://en.wikipedia.org/wiki/Malthusian_growth_model ); and in finance, the model appears in a similar role incontinuous compounding withC as the initial amount of money. Inexponential decay models, k is often expressed as the negative of a positive constant λ.
Herey' is given as ( SD Y ) , C_ as c , andky as ( ( S X. { K } ) oF x. Y ) . ( S X. { K } ) is the constant function that maps any real or complex input tok and oF x. is multiplication as a function operation.
The leftward direction of the biconditional is as given in http://www.saylor.org/site/wp-content/uploads/2011/06/MA221-2.1.1.pdf pp. 1-2, which also notes the reverse direction ("While we will not prove this here, it turns out that these are the only functions that satisfy this equation."). The rightward direction is Theorem 5.1 of LarsonHostetlerEdwards p. 375 (which notes "C is theinitial value ofy, andk is theproportionality constant.Exponential growth occurs whenk > 0, andexponential decay occurs whenk < 0."); its proof here closely follows the proof ofy' =y in https://proofwiki.org/wiki/Exponential_Growth_Equation/Special_Case .
Statements for this and expgrowthi formulated by Mario Carneiro. (Contributed by Steve Rodriguez, 24-Nov-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | expgrowth.s | ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } ) | |
expgrowth.k | ⊢ ( 𝜑 → 𝐾 ∈ ℂ ) | ||
expgrowth.y | ⊢ ( 𝜑 → 𝑌 : 𝑆 ⟶ ℂ ) | ||
expgrowth.dy | ⊢ ( 𝜑 → dom ( 𝑆 D 𝑌 ) = 𝑆 ) | ||
Assertion | expgrowth | ⊢ ( 𝜑 → ( ( 𝑆 D 𝑌 ) = ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ↔ ∃ 𝑐 ∈ ℂ 𝑌 = ( 𝑡 ∈ 𝑆 ↦ ( 𝑐 · ( exp ‘ ( 𝐾 · 𝑡 ) ) ) ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | expgrowth.s | ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } ) | |
2 | expgrowth.k | ⊢ ( 𝜑 → 𝐾 ∈ ℂ ) | |
3 | expgrowth.y | ⊢ ( 𝜑 → 𝑌 : 𝑆 ⟶ ℂ ) | |
4 | expgrowth.dy | ⊢ ( 𝜑 → dom ( 𝑆 D 𝑌 ) = 𝑆 ) | |
5 | cnelprrecn | ⊢ ℂ ∈ { ℝ , ℂ } | |
6 | 5 | a1i | ⊢ ( 𝜑 → ℂ ∈ { ℝ , ℂ } ) |
7 | recnprss | ⊢ ( 𝑆 ∈ { ℝ , ℂ } → 𝑆 ⊆ ℂ ) | |
8 | 1 7 | syl | ⊢ ( 𝜑 → 𝑆 ⊆ ℂ ) |
9 | 8 | sseld | ⊢ ( 𝜑 → ( 𝑢 ∈ 𝑆 → 𝑢 ∈ ℂ ) ) |
10 | mulcl | ⊢ ( ( 𝐾 ∈ ℂ ∧ 𝑢 ∈ ℂ ) → ( 𝐾 · 𝑢 ) ∈ ℂ ) | |
11 | 2 9 10 | syl6an | ⊢ ( 𝜑 → ( 𝑢 ∈ 𝑆 → ( 𝐾 · 𝑢 ) ∈ ℂ ) ) |
12 | 11 | imp | ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑆 ) → ( 𝐾 · 𝑢 ) ∈ ℂ ) |
13 | 12 | negcld | ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑆 ) → - ( 𝐾 · 𝑢 ) ∈ ℂ ) |
14 | 2 | negcld | ⊢ ( 𝜑 → - 𝐾 ∈ ℂ ) |
15 | 14 | adantr | ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑆 ) → - 𝐾 ∈ ℂ ) |
16 | efcl | ⊢ ( 𝑦 ∈ ℂ → ( exp ‘ 𝑦 ) ∈ ℂ ) | |
17 | 16 | adantl | ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( exp ‘ 𝑦 ) ∈ ℂ ) |
18 | 2 | adantr | ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑆 ) → 𝐾 ∈ ℂ ) |
19 | 9 | imp | ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑆 ) → 𝑢 ∈ ℂ ) |
20 | ax-1cn | ⊢ 1 ∈ ℂ | |
21 | 20 | a1i | ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑆 ) → 1 ∈ ℂ ) |
22 | 1 | dvmptid | ⊢ ( 𝜑 → ( 𝑆 D ( 𝑢 ∈ 𝑆 ↦ 𝑢 ) ) = ( 𝑢 ∈ 𝑆 ↦ 1 ) ) |
23 | 1 19 21 22 2 | dvmptcmul | ⊢ ( 𝜑 → ( 𝑆 D ( 𝑢 ∈ 𝑆 ↦ ( 𝐾 · 𝑢 ) ) ) = ( 𝑢 ∈ 𝑆 ↦ ( 𝐾 · 1 ) ) ) |
24 | 2 | mulid1d | ⊢ ( 𝜑 → ( 𝐾 · 1 ) = 𝐾 ) |
25 | 24 | mpteq2dv | ⊢ ( 𝜑 → ( 𝑢 ∈ 𝑆 ↦ ( 𝐾 · 1 ) ) = ( 𝑢 ∈ 𝑆 ↦ 𝐾 ) ) |
26 | 23 25 | eqtrd | ⊢ ( 𝜑 → ( 𝑆 D ( 𝑢 ∈ 𝑆 ↦ ( 𝐾 · 𝑢 ) ) ) = ( 𝑢 ∈ 𝑆 ↦ 𝐾 ) ) |
27 | 1 12 18 26 | dvmptneg | ⊢ ( 𝜑 → ( 𝑆 D ( 𝑢 ∈ 𝑆 ↦ - ( 𝐾 · 𝑢 ) ) ) = ( 𝑢 ∈ 𝑆 ↦ - 𝐾 ) ) |
28 | dvef | ⊢ ( ℂ D exp ) = exp | |
29 | eff | ⊢ exp : ℂ ⟶ ℂ | |
30 | ffn | ⊢ ( exp : ℂ ⟶ ℂ → exp Fn ℂ ) | |
31 | 29 30 | ax-mp | ⊢ exp Fn ℂ |
32 | dffn5 | ⊢ ( exp Fn ℂ ↔ exp = ( 𝑦 ∈ ℂ ↦ ( exp ‘ 𝑦 ) ) ) | |
33 | 31 32 | mpbi | ⊢ exp = ( 𝑦 ∈ ℂ ↦ ( exp ‘ 𝑦 ) ) |
34 | 33 | oveq2i | ⊢ ( ℂ D exp ) = ( ℂ D ( 𝑦 ∈ ℂ ↦ ( exp ‘ 𝑦 ) ) ) |
35 | 28 34 33 | 3eqtr3i | ⊢ ( ℂ D ( 𝑦 ∈ ℂ ↦ ( exp ‘ 𝑦 ) ) ) = ( 𝑦 ∈ ℂ ↦ ( exp ‘ 𝑦 ) ) |
36 | 35 | a1i | ⊢ ( 𝜑 → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( exp ‘ 𝑦 ) ) ) = ( 𝑦 ∈ ℂ ↦ ( exp ‘ 𝑦 ) ) ) |
37 | fveq2 | ⊢ ( 𝑦 = - ( 𝐾 · 𝑢 ) → ( exp ‘ 𝑦 ) = ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) | |
38 | 1 6 13 15 17 17 27 36 37 37 | dvmptco | ⊢ ( 𝜑 → ( 𝑆 D ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) = ( 𝑢 ∈ 𝑆 ↦ ( ( exp ‘ - ( 𝐾 · 𝑢 ) ) · - 𝐾 ) ) ) |
39 | 38 | oveq2d | ⊢ ( 𝜑 → ( 𝑌 ∘f · ( 𝑆 D ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ) = ( 𝑌 ∘f · ( 𝑢 ∈ 𝑆 ↦ ( ( exp ‘ - ( 𝐾 · 𝑢 ) ) · - 𝐾 ) ) ) ) |
40 | efcl | ⊢ ( - ( 𝐾 · 𝑢 ) ∈ ℂ → ( exp ‘ - ( 𝐾 · 𝑢 ) ) ∈ ℂ ) | |
41 | 13 40 | syl | ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑆 ) → ( exp ‘ - ( 𝐾 · 𝑢 ) ) ∈ ℂ ) |
42 | 41 15 | mulcld | ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑆 ) → ( ( exp ‘ - ( 𝐾 · 𝑢 ) ) · - 𝐾 ) ∈ ℂ ) |
43 | 42 | fmpttd | ⊢ ( 𝜑 → ( 𝑢 ∈ 𝑆 ↦ ( ( exp ‘ - ( 𝐾 · 𝑢 ) ) · - 𝐾 ) ) : 𝑆 ⟶ ℂ ) |
44 | 38 | feq1d | ⊢ ( 𝜑 → ( ( 𝑆 D ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) : 𝑆 ⟶ ℂ ↔ ( 𝑢 ∈ 𝑆 ↦ ( ( exp ‘ - ( 𝐾 · 𝑢 ) ) · - 𝐾 ) ) : 𝑆 ⟶ ℂ ) ) |
45 | 43 44 | mpbird | ⊢ ( 𝜑 → ( 𝑆 D ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) : 𝑆 ⟶ ℂ ) |
46 | mulcom | ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 · 𝑦 ) = ( 𝑦 · 𝑥 ) ) | |
47 | 46 | adantl | ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ) → ( 𝑥 · 𝑦 ) = ( 𝑦 · 𝑥 ) ) |
48 | 1 3 45 47 | caofcom | ⊢ ( 𝜑 → ( 𝑌 ∘f · ( 𝑆 D ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ) = ( ( 𝑆 D ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ∘f · 𝑌 ) ) |
49 | 39 48 | eqtr3d | ⊢ ( 𝜑 → ( 𝑌 ∘f · ( 𝑢 ∈ 𝑆 ↦ ( ( exp ‘ - ( 𝐾 · 𝑢 ) ) · - 𝐾 ) ) ) = ( ( 𝑆 D ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ∘f · 𝑌 ) ) |
50 | 49 | oveq2d | ⊢ ( 𝜑 → ( ( ( 𝑆 D 𝑌 ) ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ∘f + ( 𝑌 ∘f · ( 𝑢 ∈ 𝑆 ↦ ( ( exp ‘ - ( 𝐾 · 𝑢 ) ) · - 𝐾 ) ) ) ) = ( ( ( 𝑆 D 𝑌 ) ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ∘f + ( ( 𝑆 D ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ∘f · 𝑌 ) ) ) |
51 | fconst6g | ⊢ ( - 𝐾 ∈ ℂ → ( 𝑆 × { - 𝐾 } ) : 𝑆 ⟶ ℂ ) | |
52 | 14 51 | syl | ⊢ ( 𝜑 → ( 𝑆 × { - 𝐾 } ) : 𝑆 ⟶ ℂ ) |
53 | 41 | fmpttd | ⊢ ( 𝜑 → ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) : 𝑆 ⟶ ℂ ) |
54 | 1 52 53 47 | caofcom | ⊢ ( 𝜑 → ( ( 𝑆 × { - 𝐾 } ) ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) = ( ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ∘f · ( 𝑆 × { - 𝐾 } ) ) ) |
55 | eqidd | ⊢ ( 𝜑 → ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) = ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) | |
56 | fconstmpt | ⊢ ( 𝑆 × { - 𝐾 } ) = ( 𝑢 ∈ 𝑆 ↦ - 𝐾 ) | |
57 | 56 | a1i | ⊢ ( 𝜑 → ( 𝑆 × { - 𝐾 } ) = ( 𝑢 ∈ 𝑆 ↦ - 𝐾 ) ) |
58 | 1 41 15 55 57 | offval2 | ⊢ ( 𝜑 → ( ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ∘f · ( 𝑆 × { - 𝐾 } ) ) = ( 𝑢 ∈ 𝑆 ↦ ( ( exp ‘ - ( 𝐾 · 𝑢 ) ) · - 𝐾 ) ) ) |
59 | 54 58 | eqtrd | ⊢ ( 𝜑 → ( ( 𝑆 × { - 𝐾 } ) ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) = ( 𝑢 ∈ 𝑆 ↦ ( ( exp ‘ - ( 𝐾 · 𝑢 ) ) · - 𝐾 ) ) ) |
60 | 59 | oveq2d | ⊢ ( 𝜑 → ( 𝑌 ∘f · ( ( 𝑆 × { - 𝐾 } ) ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ) = ( 𝑌 ∘f · ( 𝑢 ∈ 𝑆 ↦ ( ( exp ‘ - ( 𝐾 · 𝑢 ) ) · - 𝐾 ) ) ) ) |
61 | 60 | oveq2d | ⊢ ( 𝜑 → ( ( ( 𝑆 D 𝑌 ) ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ∘f + ( 𝑌 ∘f · ( ( 𝑆 × { - 𝐾 } ) ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ) ) = ( ( ( 𝑆 D 𝑌 ) ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ∘f + ( 𝑌 ∘f · ( 𝑢 ∈ 𝑆 ↦ ( ( exp ‘ - ( 𝐾 · 𝑢 ) ) · - 𝐾 ) ) ) ) ) |
62 | 38 | dmeqd | ⊢ ( 𝜑 → dom ( 𝑆 D ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) = dom ( 𝑢 ∈ 𝑆 ↦ ( ( exp ‘ - ( 𝐾 · 𝑢 ) ) · - 𝐾 ) ) ) |
63 | eqid | ⊢ ( 𝑢 ∈ 𝑆 ↦ ( ( exp ‘ - ( 𝐾 · 𝑢 ) ) · - 𝐾 ) ) = ( 𝑢 ∈ 𝑆 ↦ ( ( exp ‘ - ( 𝐾 · 𝑢 ) ) · - 𝐾 ) ) | |
64 | 63 42 | dmmptd | ⊢ ( 𝜑 → dom ( 𝑢 ∈ 𝑆 ↦ ( ( exp ‘ - ( 𝐾 · 𝑢 ) ) · - 𝐾 ) ) = 𝑆 ) |
65 | 62 64 | eqtrd | ⊢ ( 𝜑 → dom ( 𝑆 D ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) = 𝑆 ) |
66 | 1 3 53 4 65 | dvmulf | ⊢ ( 𝜑 → ( 𝑆 D ( 𝑌 ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ) = ( ( ( 𝑆 D 𝑌 ) ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ∘f + ( ( 𝑆 D ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ∘f · 𝑌 ) ) ) |
67 | 50 61 66 | 3eqtr4rd | ⊢ ( 𝜑 → ( 𝑆 D ( 𝑌 ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ) = ( ( ( 𝑆 D 𝑌 ) ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ∘f + ( 𝑌 ∘f · ( ( 𝑆 × { - 𝐾 } ) ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ) ) ) |
68 | ofmul12 | ⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝑌 : 𝑆 ⟶ ℂ ) ∧ ( ( 𝑆 × { - 𝐾 } ) : 𝑆 ⟶ ℂ ∧ ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) : 𝑆 ⟶ ℂ ) ) → ( 𝑌 ∘f · ( ( 𝑆 × { - 𝐾 } ) ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ) = ( ( 𝑆 × { - 𝐾 } ) ∘f · ( 𝑌 ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ) ) | |
69 | 1 3 52 53 68 | syl22anc | ⊢ ( 𝜑 → ( 𝑌 ∘f · ( ( 𝑆 × { - 𝐾 } ) ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ) = ( ( 𝑆 × { - 𝐾 } ) ∘f · ( 𝑌 ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ) ) |
70 | 69 | oveq2d | ⊢ ( 𝜑 → ( ( ( 𝑆 D 𝑌 ) ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ∘f + ( 𝑌 ∘f · ( ( 𝑆 × { - 𝐾 } ) ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ) ) = ( ( ( 𝑆 D 𝑌 ) ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ∘f + ( ( 𝑆 × { - 𝐾 } ) ∘f · ( 𝑌 ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ) ) ) |
71 | 67 70 | eqtrd | ⊢ ( 𝜑 → ( 𝑆 D ( 𝑌 ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ) = ( ( ( 𝑆 D 𝑌 ) ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ∘f + ( ( 𝑆 × { - 𝐾 } ) ∘f · ( 𝑌 ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ) ) ) |
72 | oveq1 | ⊢ ( ( 𝑆 D 𝑌 ) = ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) → ( ( 𝑆 D 𝑌 ) ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) = ( ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ) | |
73 | 72 | oveq1d | ⊢ ( ( 𝑆 D 𝑌 ) = ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) → ( ( ( 𝑆 D 𝑌 ) ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ∘f + ( ( 𝑆 × { - 𝐾 } ) ∘f · ( 𝑌 ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ) ) = ( ( ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ∘f + ( ( 𝑆 × { - 𝐾 } ) ∘f · ( 𝑌 ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ) ) ) |
74 | 71 73 | sylan9eq | ⊢ ( ( 𝜑 ∧ ( 𝑆 D 𝑌 ) = ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ) → ( 𝑆 D ( 𝑌 ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ) = ( ( ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ∘f + ( ( 𝑆 × { - 𝐾 } ) ∘f · ( 𝑌 ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ) ) ) |
75 | mulass | ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 𝑥 · 𝑦 ) · 𝑧 ) = ( 𝑥 · ( 𝑦 · 𝑧 ) ) ) | |
76 | 75 | adantl | ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) ) → ( ( 𝑥 · 𝑦 ) · 𝑧 ) = ( 𝑥 · ( 𝑦 · 𝑧 ) ) ) |
77 | 1 52 3 53 76 | caofass | ⊢ ( 𝜑 → ( ( ( 𝑆 × { - 𝐾 } ) ∘f · 𝑌 ) ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) = ( ( 𝑆 × { - 𝐾 } ) ∘f · ( 𝑌 ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ) ) |
78 | 77 | oveq2d | ⊢ ( 𝜑 → ( ( ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ∘f + ( ( ( 𝑆 × { - 𝐾 } ) ∘f · 𝑌 ) ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ) = ( ( ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ∘f + ( ( 𝑆 × { - 𝐾 } ) ∘f · ( 𝑌 ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ) ) ) |
79 | 78 | eqeq2d | ⊢ ( 𝜑 → ( ( 𝑆 D ( 𝑌 ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ) = ( ( ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ∘f + ( ( ( 𝑆 × { - 𝐾 } ) ∘f · 𝑌 ) ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ) ↔ ( 𝑆 D ( 𝑌 ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ) = ( ( ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ∘f + ( ( 𝑆 × { - 𝐾 } ) ∘f · ( 𝑌 ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ) ) ) ) |
80 | 79 | adantr | ⊢ ( ( 𝜑 ∧ ( 𝑆 D 𝑌 ) = ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ) → ( ( 𝑆 D ( 𝑌 ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ) = ( ( ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ∘f + ( ( ( 𝑆 × { - 𝐾 } ) ∘f · 𝑌 ) ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ) ↔ ( 𝑆 D ( 𝑌 ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ) = ( ( ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ∘f + ( ( 𝑆 × { - 𝐾 } ) ∘f · ( 𝑌 ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ) ) ) ) |
81 | 74 80 | mpbird | ⊢ ( ( 𝜑 ∧ ( 𝑆 D 𝑌 ) = ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ) → ( 𝑆 D ( 𝑌 ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ) = ( ( ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ∘f + ( ( ( 𝑆 × { - 𝐾 } ) ∘f · 𝑌 ) ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ) ) |
82 | mulcl | ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 · 𝑦 ) ∈ ℂ ) | |
83 | 82 | adantl | ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ) → ( 𝑥 · 𝑦 ) ∈ ℂ ) |
84 | fconst6g | ⊢ ( 𝐾 ∈ ℂ → ( 𝑆 × { 𝐾 } ) : 𝑆 ⟶ ℂ ) | |
85 | 2 84 | syl | ⊢ ( 𝜑 → ( 𝑆 × { 𝐾 } ) : 𝑆 ⟶ ℂ ) |
86 | inidm | ⊢ ( 𝑆 ∩ 𝑆 ) = 𝑆 | |
87 | 83 85 3 1 1 86 | off | ⊢ ( 𝜑 → ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) : 𝑆 ⟶ ℂ ) |
88 | 83 52 3 1 1 86 | off | ⊢ ( 𝜑 → ( ( 𝑆 × { - 𝐾 } ) ∘f · 𝑌 ) : 𝑆 ⟶ ℂ ) |
89 | adddir | ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) | |
90 | 89 | adantl | ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) ) → ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) |
91 | 1 53 87 88 90 | caofdir | ⊢ ( 𝜑 → ( ( ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ∘f + ( ( 𝑆 × { - 𝐾 } ) ∘f · 𝑌 ) ) ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) = ( ( ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ∘f + ( ( ( 𝑆 × { - 𝐾 } ) ∘f · 𝑌 ) ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ) ) |
92 | 91 | eqeq2d | ⊢ ( 𝜑 → ( ( 𝑆 D ( 𝑌 ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ) = ( ( ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ∘f + ( ( 𝑆 × { - 𝐾 } ) ∘f · 𝑌 ) ) ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ↔ ( 𝑆 D ( 𝑌 ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ) = ( ( ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ∘f + ( ( ( 𝑆 × { - 𝐾 } ) ∘f · 𝑌 ) ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ) ) ) |
93 | 92 | adantr | ⊢ ( ( 𝜑 ∧ ( 𝑆 D 𝑌 ) = ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ) → ( ( 𝑆 D ( 𝑌 ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ) = ( ( ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ∘f + ( ( 𝑆 × { - 𝐾 } ) ∘f · 𝑌 ) ) ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ↔ ( 𝑆 D ( 𝑌 ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ) = ( ( ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ∘f + ( ( ( 𝑆 × { - 𝐾 } ) ∘f · 𝑌 ) ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ) ) ) |
94 | 81 93 | mpbird | ⊢ ( ( 𝜑 ∧ ( 𝑆 D 𝑌 ) = ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ) → ( 𝑆 D ( 𝑌 ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ) = ( ( ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ∘f + ( ( 𝑆 × { - 𝐾 } ) ∘f · 𝑌 ) ) ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ) |
95 | ofnegsub | ⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) : 𝑆 ⟶ ℂ ∧ ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) : 𝑆 ⟶ ℂ ) → ( ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ∘f + ( ( 𝑆 × { - 1 } ) ∘f · ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ) ) = ( ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ∘f − ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ) ) | |
96 | 1 87 87 95 | syl3anc | ⊢ ( 𝜑 → ( ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ∘f + ( ( 𝑆 × { - 1 } ) ∘f · ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ) ) = ( ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ∘f − ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ) ) |
97 | neg1cn | ⊢ - 1 ∈ ℂ | |
98 | 97 | fconst6 | ⊢ ( 𝑆 × { - 1 } ) : 𝑆 ⟶ ℂ |
99 | 98 | a1i | ⊢ ( 𝜑 → ( 𝑆 × { - 1 } ) : 𝑆 ⟶ ℂ ) |
100 | 1 99 85 3 76 | caofass | ⊢ ( 𝜑 → ( ( ( 𝑆 × { - 1 } ) ∘f · ( 𝑆 × { 𝐾 } ) ) ∘f · 𝑌 ) = ( ( 𝑆 × { - 1 } ) ∘f · ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ) ) |
101 | 97 | a1i | ⊢ ( 𝜑 → - 1 ∈ ℂ ) |
102 | 1 101 2 | ofc12 | ⊢ ( 𝜑 → ( ( 𝑆 × { - 1 } ) ∘f · ( 𝑆 × { 𝐾 } ) ) = ( 𝑆 × { ( - 1 · 𝐾 ) } ) ) |
103 | 2 | mulm1d | ⊢ ( 𝜑 → ( - 1 · 𝐾 ) = - 𝐾 ) |
104 | 103 | sneqd | ⊢ ( 𝜑 → { ( - 1 · 𝐾 ) } = { - 𝐾 } ) |
105 | 104 | xpeq2d | ⊢ ( 𝜑 → ( 𝑆 × { ( - 1 · 𝐾 ) } ) = ( 𝑆 × { - 𝐾 } ) ) |
106 | 102 105 | eqtrd | ⊢ ( 𝜑 → ( ( 𝑆 × { - 1 } ) ∘f · ( 𝑆 × { 𝐾 } ) ) = ( 𝑆 × { - 𝐾 } ) ) |
107 | 106 | oveq1d | ⊢ ( 𝜑 → ( ( ( 𝑆 × { - 1 } ) ∘f · ( 𝑆 × { 𝐾 } ) ) ∘f · 𝑌 ) = ( ( 𝑆 × { - 𝐾 } ) ∘f · 𝑌 ) ) |
108 | 100 107 | eqtr3d | ⊢ ( 𝜑 → ( ( 𝑆 × { - 1 } ) ∘f · ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ) = ( ( 𝑆 × { - 𝐾 } ) ∘f · 𝑌 ) ) |
109 | 108 | oveq2d | ⊢ ( 𝜑 → ( ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ∘f + ( ( 𝑆 × { - 1 } ) ∘f · ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ) ) = ( ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ∘f + ( ( 𝑆 × { - 𝐾 } ) ∘f · 𝑌 ) ) ) |
110 | ofsubid | ⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) : 𝑆 ⟶ ℂ ) → ( ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ∘f − ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ) = ( 𝑆 × { 0 } ) ) | |
111 | 1 87 110 | syl2anc | ⊢ ( 𝜑 → ( ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ∘f − ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ) = ( 𝑆 × { 0 } ) ) |
112 | 96 109 111 | 3eqtr3d | ⊢ ( 𝜑 → ( ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ∘f + ( ( 𝑆 × { - 𝐾 } ) ∘f · 𝑌 ) ) = ( 𝑆 × { 0 } ) ) |
113 | 112 | oveq1d | ⊢ ( 𝜑 → ( ( ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ∘f + ( ( 𝑆 × { - 𝐾 } ) ∘f · 𝑌 ) ) ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) = ( ( 𝑆 × { 0 } ) ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ) |
114 | 113 | eqeq2d | ⊢ ( 𝜑 → ( ( 𝑆 D ( 𝑌 ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ) = ( ( ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ∘f + ( ( 𝑆 × { - 𝐾 } ) ∘f · 𝑌 ) ) ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ↔ ( 𝑆 D ( 𝑌 ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ) = ( ( 𝑆 × { 0 } ) ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ) ) |
115 | 114 | adantr | ⊢ ( ( 𝜑 ∧ ( 𝑆 D 𝑌 ) = ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ) → ( ( 𝑆 D ( 𝑌 ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ) = ( ( ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ∘f + ( ( 𝑆 × { - 𝐾 } ) ∘f · 𝑌 ) ) ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ↔ ( 𝑆 D ( 𝑌 ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ) = ( ( 𝑆 × { 0 } ) ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ) ) |
116 | 94 115 | mpbid | ⊢ ( ( 𝜑 ∧ ( 𝑆 D 𝑌 ) = ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ) → ( 𝑆 D ( 𝑌 ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ) = ( ( 𝑆 × { 0 } ) ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ) |
117 | 0cnd | ⊢ ( 𝜑 → 0 ∈ ℂ ) | |
118 | mul02 | ⊢ ( 𝑥 ∈ ℂ → ( 0 · 𝑥 ) = 0 ) | |
119 | 118 | adantl | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 0 · 𝑥 ) = 0 ) |
120 | 1 53 117 117 119 | caofid2 | ⊢ ( 𝜑 → ( ( 𝑆 × { 0 } ) ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) = ( 𝑆 × { 0 } ) ) |
121 | 120 | adantr | ⊢ ( ( 𝜑 ∧ ( 𝑆 D 𝑌 ) = ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ) → ( ( 𝑆 × { 0 } ) ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) = ( 𝑆 × { 0 } ) ) |
122 | 116 121 | eqtrd | ⊢ ( ( 𝜑 ∧ ( 𝑆 D 𝑌 ) = ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ) → ( 𝑆 D ( 𝑌 ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ) = ( 𝑆 × { 0 } ) ) |
123 | 1 | adantr | ⊢ ( ( 𝜑 ∧ ( 𝑆 D 𝑌 ) = ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ) → 𝑆 ∈ { ℝ , ℂ } ) |
124 | 83 3 53 1 1 86 | off | ⊢ ( 𝜑 → ( 𝑌 ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) : 𝑆 ⟶ ℂ ) |
125 | 124 | adantr | ⊢ ( ( 𝜑 ∧ ( 𝑆 D 𝑌 ) = ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ) → ( 𝑌 ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) : 𝑆 ⟶ ℂ ) |
126 | 122 | dmeqd | ⊢ ( ( 𝜑 ∧ ( 𝑆 D 𝑌 ) = ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ) → dom ( 𝑆 D ( 𝑌 ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ) = dom ( 𝑆 × { 0 } ) ) |
127 | 0cn | ⊢ 0 ∈ ℂ | |
128 | 127 | fconst6 | ⊢ ( 𝑆 × { 0 } ) : 𝑆 ⟶ ℂ |
129 | 128 | fdmi | ⊢ dom ( 𝑆 × { 0 } ) = 𝑆 |
130 | 126 129 | eqtrdi | ⊢ ( ( 𝜑 ∧ ( 𝑆 D 𝑌 ) = ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ) → dom ( 𝑆 D ( 𝑌 ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ) = 𝑆 ) |
131 | 123 125 130 | dvconstbi | ⊢ ( ( 𝜑 ∧ ( 𝑆 D 𝑌 ) = ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ) → ( ( 𝑆 D ( 𝑌 ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ) = ( 𝑆 × { 0 } ) ↔ ∃ 𝑥 ∈ ℂ ( 𝑌 ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) = ( 𝑆 × { 𝑥 } ) ) ) |
132 | 122 131 | mpbid | ⊢ ( ( 𝜑 ∧ ( 𝑆 D 𝑌 ) = ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ) → ∃ 𝑥 ∈ ℂ ( 𝑌 ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) = ( 𝑆 × { 𝑥 } ) ) |
133 | oveq1 | ⊢ ( ( 𝑌 ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) = ( 𝑆 × { 𝑥 } ) → ( ( 𝑌 ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ∘f / ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) = ( ( 𝑆 × { 𝑥 } ) ∘f / ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ) | |
134 | efne0 | ⊢ ( - ( 𝐾 · 𝑢 ) ∈ ℂ → ( exp ‘ - ( 𝐾 · 𝑢 ) ) ≠ 0 ) | |
135 | eldifsn | ⊢ ( ( exp ‘ - ( 𝐾 · 𝑢 ) ) ∈ ( ℂ ∖ { 0 } ) ↔ ( ( exp ‘ - ( 𝐾 · 𝑢 ) ) ∈ ℂ ∧ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ≠ 0 ) ) | |
136 | 40 134 135 | sylanbrc | ⊢ ( - ( 𝐾 · 𝑢 ) ∈ ℂ → ( exp ‘ - ( 𝐾 · 𝑢 ) ) ∈ ( ℂ ∖ { 0 } ) ) |
137 | 13 136 | syl | ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑆 ) → ( exp ‘ - ( 𝐾 · 𝑢 ) ) ∈ ( ℂ ∖ { 0 } ) ) |
138 | 137 | fmpttd | ⊢ ( 𝜑 → ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) : 𝑆 ⟶ ( ℂ ∖ { 0 } ) ) |
139 | ofdivcan4 | ⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝑌 : 𝑆 ⟶ ℂ ∧ ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) : 𝑆 ⟶ ( ℂ ∖ { 0 } ) ) → ( ( 𝑌 ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ∘f / ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) = 𝑌 ) | |
140 | 1 3 138 139 | syl3anc | ⊢ ( 𝜑 → ( ( 𝑌 ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ∘f / ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) = 𝑌 ) |
141 | 140 | eqeq1d | ⊢ ( 𝜑 → ( ( ( 𝑌 ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ∘f / ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) = ( ( 𝑆 × { 𝑥 } ) ∘f / ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ↔ 𝑌 = ( ( 𝑆 × { 𝑥 } ) ∘f / ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ) ) |
142 | 133 141 | syl5ib | ⊢ ( 𝜑 → ( ( 𝑌 ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) = ( 𝑆 × { 𝑥 } ) → 𝑌 = ( ( 𝑆 × { 𝑥 } ) ∘f / ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ) ) |
143 | 142 | adantr | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( 𝑌 ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) = ( 𝑆 × { 𝑥 } ) → 𝑌 = ( ( 𝑆 × { 𝑥 } ) ∘f / ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ) ) |
144 | vex | ⊢ 𝑥 ∈ V | |
145 | 144 | a1i | ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑆 ) → 𝑥 ∈ V ) |
146 | ovexd | ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑆 ) → ( 1 / ( exp ‘ ( 𝐾 · 𝑢 ) ) ) ∈ V ) | |
147 | fconstmpt | ⊢ ( 𝑆 × { 𝑥 } ) = ( 𝑢 ∈ 𝑆 ↦ 𝑥 ) | |
148 | 147 | a1i | ⊢ ( 𝜑 → ( 𝑆 × { 𝑥 } ) = ( 𝑢 ∈ 𝑆 ↦ 𝑥 ) ) |
149 | efneg | ⊢ ( ( 𝐾 · 𝑢 ) ∈ ℂ → ( exp ‘ - ( 𝐾 · 𝑢 ) ) = ( 1 / ( exp ‘ ( 𝐾 · 𝑢 ) ) ) ) | |
150 | 12 149 | syl | ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑆 ) → ( exp ‘ - ( 𝐾 · 𝑢 ) ) = ( 1 / ( exp ‘ ( 𝐾 · 𝑢 ) ) ) ) |
151 | 150 | mpteq2dva | ⊢ ( 𝜑 → ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) = ( 𝑢 ∈ 𝑆 ↦ ( 1 / ( exp ‘ ( 𝐾 · 𝑢 ) ) ) ) ) |
152 | 1 145 146 148 151 | offval2 | ⊢ ( 𝜑 → ( ( 𝑆 × { 𝑥 } ) ∘f / ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) = ( 𝑢 ∈ 𝑆 ↦ ( 𝑥 / ( 1 / ( exp ‘ ( 𝐾 · 𝑢 ) ) ) ) ) ) |
153 | 152 | adantr | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( 𝑆 × { 𝑥 } ) ∘f / ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) = ( 𝑢 ∈ 𝑆 ↦ ( 𝑥 / ( 1 / ( exp ‘ ( 𝐾 · 𝑢 ) ) ) ) ) ) |
154 | efcl | ⊢ ( ( 𝐾 · 𝑢 ) ∈ ℂ → ( exp ‘ ( 𝐾 · 𝑢 ) ) ∈ ℂ ) | |
155 | efne0 | ⊢ ( ( 𝐾 · 𝑢 ) ∈ ℂ → ( exp ‘ ( 𝐾 · 𝑢 ) ) ≠ 0 ) | |
156 | 154 155 | jca | ⊢ ( ( 𝐾 · 𝑢 ) ∈ ℂ → ( ( exp ‘ ( 𝐾 · 𝑢 ) ) ∈ ℂ ∧ ( exp ‘ ( 𝐾 · 𝑢 ) ) ≠ 0 ) ) |
157 | 12 156 | syl | ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑆 ) → ( ( exp ‘ ( 𝐾 · 𝑢 ) ) ∈ ℂ ∧ ( exp ‘ ( 𝐾 · 𝑢 ) ) ≠ 0 ) ) |
158 | ax-1ne0 | ⊢ 1 ≠ 0 | |
159 | 20 158 | pm3.2i | ⊢ ( 1 ∈ ℂ ∧ 1 ≠ 0 ) |
160 | divdiv2 | ⊢ ( ( 𝑥 ∈ ℂ ∧ ( 1 ∈ ℂ ∧ 1 ≠ 0 ) ∧ ( ( exp ‘ ( 𝐾 · 𝑢 ) ) ∈ ℂ ∧ ( exp ‘ ( 𝐾 · 𝑢 ) ) ≠ 0 ) ) → ( 𝑥 / ( 1 / ( exp ‘ ( 𝐾 · 𝑢 ) ) ) ) = ( ( 𝑥 · ( exp ‘ ( 𝐾 · 𝑢 ) ) ) / 1 ) ) | |
161 | 159 160 | mp3an2 | ⊢ ( ( 𝑥 ∈ ℂ ∧ ( ( exp ‘ ( 𝐾 · 𝑢 ) ) ∈ ℂ ∧ ( exp ‘ ( 𝐾 · 𝑢 ) ) ≠ 0 ) ) → ( 𝑥 / ( 1 / ( exp ‘ ( 𝐾 · 𝑢 ) ) ) ) = ( ( 𝑥 · ( exp ‘ ( 𝐾 · 𝑢 ) ) ) / 1 ) ) |
162 | 157 161 | sylan2 | ⊢ ( ( 𝑥 ∈ ℂ ∧ ( 𝜑 ∧ 𝑢 ∈ 𝑆 ) ) → ( 𝑥 / ( 1 / ( exp ‘ ( 𝐾 · 𝑢 ) ) ) ) = ( ( 𝑥 · ( exp ‘ ( 𝐾 · 𝑢 ) ) ) / 1 ) ) |
163 | 12 154 | syl | ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑆 ) → ( exp ‘ ( 𝐾 · 𝑢 ) ) ∈ ℂ ) |
164 | mulcl | ⊢ ( ( 𝑥 ∈ ℂ ∧ ( exp ‘ ( 𝐾 · 𝑢 ) ) ∈ ℂ ) → ( 𝑥 · ( exp ‘ ( 𝐾 · 𝑢 ) ) ) ∈ ℂ ) | |
165 | 163 164 | sylan2 | ⊢ ( ( 𝑥 ∈ ℂ ∧ ( 𝜑 ∧ 𝑢 ∈ 𝑆 ) ) → ( 𝑥 · ( exp ‘ ( 𝐾 · 𝑢 ) ) ) ∈ ℂ ) |
166 | 165 | div1d | ⊢ ( ( 𝑥 ∈ ℂ ∧ ( 𝜑 ∧ 𝑢 ∈ 𝑆 ) ) → ( ( 𝑥 · ( exp ‘ ( 𝐾 · 𝑢 ) ) ) / 1 ) = ( 𝑥 · ( exp ‘ ( 𝐾 · 𝑢 ) ) ) ) |
167 | 162 166 | eqtrd | ⊢ ( ( 𝑥 ∈ ℂ ∧ ( 𝜑 ∧ 𝑢 ∈ 𝑆 ) ) → ( 𝑥 / ( 1 / ( exp ‘ ( 𝐾 · 𝑢 ) ) ) ) = ( 𝑥 · ( exp ‘ ( 𝐾 · 𝑢 ) ) ) ) |
168 | 167 | ancoms | ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑆 ) ∧ 𝑥 ∈ ℂ ) → ( 𝑥 / ( 1 / ( exp ‘ ( 𝐾 · 𝑢 ) ) ) ) = ( 𝑥 · ( exp ‘ ( 𝐾 · 𝑢 ) ) ) ) |
169 | 168 | an32s | ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑢 ∈ 𝑆 ) → ( 𝑥 / ( 1 / ( exp ‘ ( 𝐾 · 𝑢 ) ) ) ) = ( 𝑥 · ( exp ‘ ( 𝐾 · 𝑢 ) ) ) ) |
170 | 169 | mpteq2dva | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 𝑢 ∈ 𝑆 ↦ ( 𝑥 / ( 1 / ( exp ‘ ( 𝐾 · 𝑢 ) ) ) ) ) = ( 𝑢 ∈ 𝑆 ↦ ( 𝑥 · ( exp ‘ ( 𝐾 · 𝑢 ) ) ) ) ) |
171 | 153 170 | eqtrd | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( 𝑆 × { 𝑥 } ) ∘f / ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) = ( 𝑢 ∈ 𝑆 ↦ ( 𝑥 · ( exp ‘ ( 𝐾 · 𝑢 ) ) ) ) ) |
172 | 171 | eqeq2d | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 𝑌 = ( ( 𝑆 × { 𝑥 } ) ∘f / ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) ↔ 𝑌 = ( 𝑢 ∈ 𝑆 ↦ ( 𝑥 · ( exp ‘ ( 𝐾 · 𝑢 ) ) ) ) ) ) |
173 | 143 172 | sylibd | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( 𝑌 ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) = ( 𝑆 × { 𝑥 } ) → 𝑌 = ( 𝑢 ∈ 𝑆 ↦ ( 𝑥 · ( exp ‘ ( 𝐾 · 𝑢 ) ) ) ) ) ) |
174 | 173 | reximdva | ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℂ ( 𝑌 ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) = ( 𝑆 × { 𝑥 } ) → ∃ 𝑥 ∈ ℂ 𝑌 = ( 𝑢 ∈ 𝑆 ↦ ( 𝑥 · ( exp ‘ ( 𝐾 · 𝑢 ) ) ) ) ) ) |
175 | 174 | adantr | ⊢ ( ( 𝜑 ∧ ( 𝑆 D 𝑌 ) = ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ) → ( ∃ 𝑥 ∈ ℂ ( 𝑌 ∘f · ( 𝑢 ∈ 𝑆 ↦ ( exp ‘ - ( 𝐾 · 𝑢 ) ) ) ) = ( 𝑆 × { 𝑥 } ) → ∃ 𝑥 ∈ ℂ 𝑌 = ( 𝑢 ∈ 𝑆 ↦ ( 𝑥 · ( exp ‘ ( 𝐾 · 𝑢 ) ) ) ) ) ) |
176 | 132 175 | mpd | ⊢ ( ( 𝜑 ∧ ( 𝑆 D 𝑌 ) = ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ) → ∃ 𝑥 ∈ ℂ 𝑌 = ( 𝑢 ∈ 𝑆 ↦ ( 𝑥 · ( exp ‘ ( 𝐾 · 𝑢 ) ) ) ) ) |
177 | 176 | ex | ⊢ ( 𝜑 → ( ( 𝑆 D 𝑌 ) = ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) → ∃ 𝑥 ∈ ℂ 𝑌 = ( 𝑢 ∈ 𝑆 ↦ ( 𝑥 · ( exp ‘ ( 𝐾 · 𝑢 ) ) ) ) ) ) |
178 | 1 | adantr | ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ 𝑌 = ( 𝑢 ∈ 𝑆 ↦ ( 𝑥 · ( exp ‘ ( 𝐾 · 𝑢 ) ) ) ) ) ) → 𝑆 ∈ { ℝ , ℂ } ) |
179 | 2 | adantr | ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ 𝑌 = ( 𝑢 ∈ 𝑆 ↦ ( 𝑥 · ( exp ‘ ( 𝐾 · 𝑢 ) ) ) ) ) ) → 𝐾 ∈ ℂ ) |
180 | simprl | ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ 𝑌 = ( 𝑢 ∈ 𝑆 ↦ ( 𝑥 · ( exp ‘ ( 𝐾 · 𝑢 ) ) ) ) ) ) → 𝑥 ∈ ℂ ) | |
181 | eqid | ⊢ ( 𝑢 ∈ 𝑆 ↦ ( 𝑥 · ( exp ‘ ( 𝐾 · 𝑢 ) ) ) ) = ( 𝑢 ∈ 𝑆 ↦ ( 𝑥 · ( exp ‘ ( 𝐾 · 𝑢 ) ) ) ) | |
182 | 178 179 180 181 | expgrowthi | ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ 𝑌 = ( 𝑢 ∈ 𝑆 ↦ ( 𝑥 · ( exp ‘ ( 𝐾 · 𝑢 ) ) ) ) ) ) → ( 𝑆 D ( 𝑢 ∈ 𝑆 ↦ ( 𝑥 · ( exp ‘ ( 𝐾 · 𝑢 ) ) ) ) ) = ( ( 𝑆 × { 𝐾 } ) ∘f · ( 𝑢 ∈ 𝑆 ↦ ( 𝑥 · ( exp ‘ ( 𝐾 · 𝑢 ) ) ) ) ) ) |
183 | 182 | 3impb | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ∧ 𝑌 = ( 𝑢 ∈ 𝑆 ↦ ( 𝑥 · ( exp ‘ ( 𝐾 · 𝑢 ) ) ) ) ) → ( 𝑆 D ( 𝑢 ∈ 𝑆 ↦ ( 𝑥 · ( exp ‘ ( 𝐾 · 𝑢 ) ) ) ) ) = ( ( 𝑆 × { 𝐾 } ) ∘f · ( 𝑢 ∈ 𝑆 ↦ ( 𝑥 · ( exp ‘ ( 𝐾 · 𝑢 ) ) ) ) ) ) |
184 | oveq2 | ⊢ ( 𝑌 = ( 𝑢 ∈ 𝑆 ↦ ( 𝑥 · ( exp ‘ ( 𝐾 · 𝑢 ) ) ) ) → ( 𝑆 D 𝑌 ) = ( 𝑆 D ( 𝑢 ∈ 𝑆 ↦ ( 𝑥 · ( exp ‘ ( 𝐾 · 𝑢 ) ) ) ) ) ) | |
185 | oveq2 | ⊢ ( 𝑌 = ( 𝑢 ∈ 𝑆 ↦ ( 𝑥 · ( exp ‘ ( 𝐾 · 𝑢 ) ) ) ) → ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) = ( ( 𝑆 × { 𝐾 } ) ∘f · ( 𝑢 ∈ 𝑆 ↦ ( 𝑥 · ( exp ‘ ( 𝐾 · 𝑢 ) ) ) ) ) ) | |
186 | 184 185 | eqeq12d | ⊢ ( 𝑌 = ( 𝑢 ∈ 𝑆 ↦ ( 𝑥 · ( exp ‘ ( 𝐾 · 𝑢 ) ) ) ) → ( ( 𝑆 D 𝑌 ) = ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ↔ ( 𝑆 D ( 𝑢 ∈ 𝑆 ↦ ( 𝑥 · ( exp ‘ ( 𝐾 · 𝑢 ) ) ) ) ) = ( ( 𝑆 × { 𝐾 } ) ∘f · ( 𝑢 ∈ 𝑆 ↦ ( 𝑥 · ( exp ‘ ( 𝐾 · 𝑢 ) ) ) ) ) ) ) |
187 | 186 | 3ad2ant3 | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ∧ 𝑌 = ( 𝑢 ∈ 𝑆 ↦ ( 𝑥 · ( exp ‘ ( 𝐾 · 𝑢 ) ) ) ) ) → ( ( 𝑆 D 𝑌 ) = ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ↔ ( 𝑆 D ( 𝑢 ∈ 𝑆 ↦ ( 𝑥 · ( exp ‘ ( 𝐾 · 𝑢 ) ) ) ) ) = ( ( 𝑆 × { 𝐾 } ) ∘f · ( 𝑢 ∈ 𝑆 ↦ ( 𝑥 · ( exp ‘ ( 𝐾 · 𝑢 ) ) ) ) ) ) ) |
188 | 183 187 | mpbird | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ∧ 𝑌 = ( 𝑢 ∈ 𝑆 ↦ ( 𝑥 · ( exp ‘ ( 𝐾 · 𝑢 ) ) ) ) ) → ( 𝑆 D 𝑌 ) = ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ) |
189 | 188 | rexlimdv3a | ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℂ 𝑌 = ( 𝑢 ∈ 𝑆 ↦ ( 𝑥 · ( exp ‘ ( 𝐾 · 𝑢 ) ) ) ) → ( 𝑆 D 𝑌 ) = ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ) ) |
190 | 177 189 | impbid | ⊢ ( 𝜑 → ( ( 𝑆 D 𝑌 ) = ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ↔ ∃ 𝑥 ∈ ℂ 𝑌 = ( 𝑢 ∈ 𝑆 ↦ ( 𝑥 · ( exp ‘ ( 𝐾 · 𝑢 ) ) ) ) ) ) |
191 | oveq2 | ⊢ ( 𝑢 = 𝑡 → ( 𝐾 · 𝑢 ) = ( 𝐾 · 𝑡 ) ) | |
192 | 191 | fveq2d | ⊢ ( 𝑢 = 𝑡 → ( exp ‘ ( 𝐾 · 𝑢 ) ) = ( exp ‘ ( 𝐾 · 𝑡 ) ) ) |
193 | 192 | oveq2d | ⊢ ( 𝑢 = 𝑡 → ( 𝑥 · ( exp ‘ ( 𝐾 · 𝑢 ) ) ) = ( 𝑥 · ( exp ‘ ( 𝐾 · 𝑡 ) ) ) ) |
194 | 193 | cbvmptv | ⊢ ( 𝑢 ∈ 𝑆 ↦ ( 𝑥 · ( exp ‘ ( 𝐾 · 𝑢 ) ) ) ) = ( 𝑡 ∈ 𝑆 ↦ ( 𝑥 · ( exp ‘ ( 𝐾 · 𝑡 ) ) ) ) |
195 | oveq1 | ⊢ ( 𝑥 = 𝑐 → ( 𝑥 · ( exp ‘ ( 𝐾 · 𝑡 ) ) ) = ( 𝑐 · ( exp ‘ ( 𝐾 · 𝑡 ) ) ) ) | |
196 | 195 | mpteq2dv | ⊢ ( 𝑥 = 𝑐 → ( 𝑡 ∈ 𝑆 ↦ ( 𝑥 · ( exp ‘ ( 𝐾 · 𝑡 ) ) ) ) = ( 𝑡 ∈ 𝑆 ↦ ( 𝑐 · ( exp ‘ ( 𝐾 · 𝑡 ) ) ) ) ) |
197 | 194 196 | eqtrid | ⊢ ( 𝑥 = 𝑐 → ( 𝑢 ∈ 𝑆 ↦ ( 𝑥 · ( exp ‘ ( 𝐾 · 𝑢 ) ) ) ) = ( 𝑡 ∈ 𝑆 ↦ ( 𝑐 · ( exp ‘ ( 𝐾 · 𝑡 ) ) ) ) ) |
198 | 197 | eqeq2d | ⊢ ( 𝑥 = 𝑐 → ( 𝑌 = ( 𝑢 ∈ 𝑆 ↦ ( 𝑥 · ( exp ‘ ( 𝐾 · 𝑢 ) ) ) ) ↔ 𝑌 = ( 𝑡 ∈ 𝑆 ↦ ( 𝑐 · ( exp ‘ ( 𝐾 · 𝑡 ) ) ) ) ) ) |
199 | 198 | cbvrexvw | ⊢ ( ∃ 𝑥 ∈ ℂ 𝑌 = ( 𝑢 ∈ 𝑆 ↦ ( 𝑥 · ( exp ‘ ( 𝐾 · 𝑢 ) ) ) ) ↔ ∃ 𝑐 ∈ ℂ 𝑌 = ( 𝑡 ∈ 𝑆 ↦ ( 𝑐 · ( exp ‘ ( 𝐾 · 𝑡 ) ) ) ) ) |
200 | 190 199 | bitrdi | ⊢ ( 𝜑 → ( ( 𝑆 D 𝑌 ) = ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ↔ ∃ 𝑐 ∈ ℂ 𝑌 = ( 𝑡 ∈ 𝑆 ↦ ( 𝑐 · ( exp ‘ ( 𝐾 · 𝑡 ) ) ) ) ) ) |