Step | Hyp | Ref
| Expression |
1 | | stoweidlem2.1 |
. . 3
⊢
Ⅎ𝑡𝜑 |
2 | | simpr 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑡 ∈ 𝑇) |
3 | | stoweidlem2.5 |
. . . . . . 7
⊢ (𝜑 → 𝐸 ∈ ℝ) |
4 | 3 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝐸 ∈ ℝ) |
5 | | eqidd 2739 |
. . . . . . . 8
⊢ (𝑠 = 𝑡 → 𝐸 = 𝐸) |
6 | 5 | cbvmptv 5187 |
. . . . . . 7
⊢ (𝑠 ∈ 𝑇 ↦ 𝐸) = (𝑡 ∈ 𝑇 ↦ 𝐸) |
7 | 6 | fvmpt2 6886 |
. . . . . 6
⊢ ((𝑡 ∈ 𝑇 ∧ 𝐸 ∈ ℝ) → ((𝑠 ∈ 𝑇 ↦ 𝐸)‘𝑡) = 𝐸) |
8 | 2, 4, 7 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝑠 ∈ 𝑇 ↦ 𝐸)‘𝑡) = 𝐸) |
9 | 8 | eqcomd 2744 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝐸 = ((𝑠 ∈ 𝑇 ↦ 𝐸)‘𝑡)) |
10 | 9 | oveq1d 7290 |
. . 3
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐸 · (𝐹‘𝑡)) = (((𝑠 ∈ 𝑇 ↦ 𝐸)‘𝑡) · (𝐹‘𝑡))) |
11 | 1, 10 | mpteq2da 5172 |
. 2
⊢ (𝜑 → (𝑡 ∈ 𝑇 ↦ (𝐸 · (𝐹‘𝑡))) = (𝑡 ∈ 𝑇 ↦ (((𝑠 ∈ 𝑇 ↦ 𝐸)‘𝑡) · (𝐹‘𝑡)))) |
12 | | id 22 |
. . . . . . . . 9
⊢ (𝑥 = 𝐸 → 𝑥 = 𝐸) |
13 | 12 | mpteq2dv 5176 |
. . . . . . . 8
⊢ (𝑥 = 𝐸 → (𝑡 ∈ 𝑇 ↦ 𝑥) = (𝑡 ∈ 𝑇 ↦ 𝐸)) |
14 | 13 | eleq1d 2823 |
. . . . . . 7
⊢ (𝑥 = 𝐸 → ((𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴 ↔ (𝑡 ∈ 𝑇 ↦ 𝐸) ∈ 𝐴)) |
15 | 14 | imbi2d 341 |
. . . . . 6
⊢ (𝑥 = 𝐸 → ((𝜑 → (𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴) ↔ (𝜑 → (𝑡 ∈ 𝑇 ↦ 𝐸) ∈ 𝐴))) |
16 | | stoweidlem2.3 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴) |
17 | 16 | expcom 414 |
. . . . . 6
⊢ (𝑥 ∈ ℝ → (𝜑 → (𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴)) |
18 | 15, 17 | vtoclga 3513 |
. . . . 5
⊢ (𝐸 ∈ ℝ → (𝜑 → (𝑡 ∈ 𝑇 ↦ 𝐸) ∈ 𝐴)) |
19 | 3, 18 | mpcom 38 |
. . . 4
⊢ (𝜑 → (𝑡 ∈ 𝑇 ↦ 𝐸) ∈ 𝐴) |
20 | 6, 19 | eqeltrid 2843 |
. . 3
⊢ (𝜑 → (𝑠 ∈ 𝑇 ↦ 𝐸) ∈ 𝐴) |
21 | | fveq1 6773 |
. . . . . . . 8
⊢ (𝑓 = (𝑠 ∈ 𝑇 ↦ 𝐸) → (𝑓‘𝑡) = ((𝑠 ∈ 𝑇 ↦ 𝐸)‘𝑡)) |
22 | 21 | oveq1d 7290 |
. . . . . . 7
⊢ (𝑓 = (𝑠 ∈ 𝑇 ↦ 𝐸) → ((𝑓‘𝑡) · (𝐹‘𝑡)) = (((𝑠 ∈ 𝑇 ↦ 𝐸)‘𝑡) · (𝐹‘𝑡))) |
23 | 22 | mpteq2dv 5176 |
. . . . . 6
⊢ (𝑓 = (𝑠 ∈ 𝑇 ↦ 𝐸) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝐹‘𝑡))) = (𝑡 ∈ 𝑇 ↦ (((𝑠 ∈ 𝑇 ↦ 𝐸)‘𝑡) · (𝐹‘𝑡)))) |
24 | 23 | eleq1d 2823 |
. . . . 5
⊢ (𝑓 = (𝑠 ∈ 𝑇 ↦ 𝐸) → ((𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝐹‘𝑡))) ∈ 𝐴 ↔ (𝑡 ∈ 𝑇 ↦ (((𝑠 ∈ 𝑇 ↦ 𝐸)‘𝑡) · (𝐹‘𝑡))) ∈ 𝐴)) |
25 | 24 | imbi2d 341 |
. . . 4
⊢ (𝑓 = (𝑠 ∈ 𝑇 ↦ 𝐸) → ((𝜑 → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝐹‘𝑡))) ∈ 𝐴) ↔ (𝜑 → (𝑡 ∈ 𝑇 ↦ (((𝑠 ∈ 𝑇 ↦ 𝐸)‘𝑡) · (𝐹‘𝑡))) ∈ 𝐴))) |
26 | | stoweidlem2.6 |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈ 𝐴) |
27 | 26 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝐹 ∈ 𝐴) |
28 | | fveq1 6773 |
. . . . . . . . . . 11
⊢ (𝑔 = 𝐹 → (𝑔‘𝑡) = (𝐹‘𝑡)) |
29 | 28 | oveq2d 7291 |
. . . . . . . . . 10
⊢ (𝑔 = 𝐹 → ((𝑓‘𝑡) · (𝑔‘𝑡)) = ((𝑓‘𝑡) · (𝐹‘𝑡))) |
30 | 29 | mpteq2dv 5176 |
. . . . . . . . 9
⊢ (𝑔 = 𝐹 → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) = (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝐹‘𝑡)))) |
31 | 30 | eleq1d 2823 |
. . . . . . . 8
⊢ (𝑔 = 𝐹 → ((𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴 ↔ (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝐹‘𝑡))) ∈ 𝐴)) |
32 | 31 | imbi2d 341 |
. . . . . . 7
⊢ (𝑔 = 𝐹 → (((𝜑 ∧ 𝑓 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴) ↔ ((𝜑 ∧ 𝑓 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝐹‘𝑡))) ∈ 𝐴))) |
33 | | stoweidlem2.2 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴) |
34 | 33 | 3comr 1124 |
. . . . . . . 8
⊢ ((𝑔 ∈ 𝐴 ∧ 𝜑 ∧ 𝑓 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴) |
35 | 34 | 3expib 1121 |
. . . . . . 7
⊢ (𝑔 ∈ 𝐴 → ((𝜑 ∧ 𝑓 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴)) |
36 | 32, 35 | vtoclga 3513 |
. . . . . 6
⊢ (𝐹 ∈ 𝐴 → ((𝜑 ∧ 𝑓 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝐹‘𝑡))) ∈ 𝐴)) |
37 | 27, 36 | mpcom 38 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝐹‘𝑡))) ∈ 𝐴) |
38 | 37 | expcom 414 |
. . . 4
⊢ (𝑓 ∈ 𝐴 → (𝜑 → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝐹‘𝑡))) ∈ 𝐴)) |
39 | 25, 38 | vtoclga 3513 |
. . 3
⊢ ((𝑠 ∈ 𝑇 ↦ 𝐸) ∈ 𝐴 → (𝜑 → (𝑡 ∈ 𝑇 ↦ (((𝑠 ∈ 𝑇 ↦ 𝐸)‘𝑡) · (𝐹‘𝑡))) ∈ 𝐴)) |
40 | 20, 39 | mpcom 38 |
. 2
⊢ (𝜑 → (𝑡 ∈ 𝑇 ↦ (((𝑠 ∈ 𝑇 ↦ 𝐸)‘𝑡) · (𝐹‘𝑡))) ∈ 𝐴) |
41 | 11, 40 | eqeltrd 2839 |
1
⊢ (𝜑 → (𝑡 ∈ 𝑇 ↦ (𝐸 · (𝐹‘𝑡))) ∈ 𝐴) |