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 | syl5eq | ⊢ ( 𝑥 = 𝑐 → ( 𝑢 ∈ 𝑆 ↦ ( 𝑥 · ( exp ‘ ( 𝐾 · 𝑢 ) ) ) ) = ( 𝑡 ∈ 𝑆 ↦ ( 𝑐 · ( exp ‘ ( 𝐾 · 𝑡 ) ) ) ) ) |
| 198 | 197 | eqeq2d | ⊢ ( 𝑥 = 𝑐 → ( 𝑌 = ( 𝑢 ∈ 𝑆 ↦ ( 𝑥 · ( exp ‘ ( 𝐾 · 𝑢 ) ) ) ) ↔ 𝑌 = ( 𝑡 ∈ 𝑆 ↦ ( 𝑐 · ( exp ‘ ( 𝐾 · 𝑡 ) ) ) ) ) ) |
| 199 | 198 | cbvrexvw | ⊢ ( ∃ 𝑥 ∈ ℂ 𝑌 = ( 𝑢 ∈ 𝑆 ↦ ( 𝑥 · ( exp ‘ ( 𝐾 · 𝑢 ) ) ) ) ↔ ∃ 𝑐 ∈ ℂ 𝑌 = ( 𝑡 ∈ 𝑆 ↦ ( 𝑐 · ( exp ‘ ( 𝐾 · 𝑡 ) ) ) ) ) |
| 200 | 190 199 | bitrdi | ⊢ ( 𝜑 → ( ( 𝑆 D 𝑌 ) = ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) ↔ ∃ 𝑐 ∈ ℂ 𝑌 = ( 𝑡 ∈ 𝑆 ↦ ( 𝑐 · ( exp ‘ ( 𝐾 · 𝑡 ) ) ) ) ) ) |