Step | Hyp | Ref
| Expression |
1 | | stoweidlem32.2 |
. . 3
⊢ 𝑃 = (𝑡 ∈ 𝑇 ↦ (𝑌 · Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡))) |
2 | | stoweidlem32.1 |
. . . 4
⊢
Ⅎ𝑡𝜑 |
3 | | stoweidlem32.3 |
. . . . . . . . . . 11
⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡)) |
4 | | fveq2 6191 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝑠 → ((𝐺‘𝑖)‘𝑡) = ((𝐺‘𝑖)‘𝑠)) |
5 | 4 | sumeq2sdv 14435 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑠 → Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡) = Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑠)) |
6 | 5 | cbvmptv 4750 |
. . . . . . . . . . 11
⊢ (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡)) = (𝑠 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑠)) |
7 | 3, 6 | eqtri 2644 |
. . . . . . . . . 10
⊢ 𝐹 = (𝑠 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑠)) |
8 | 7 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝐹 = (𝑠 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑠))) |
9 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑠 = 𝑡 → ((𝐺‘𝑖)‘𝑠) = ((𝐺‘𝑖)‘𝑡)) |
10 | 9 | sumeq2sdv 14435 |
. . . . . . . . . 10
⊢ (𝑠 = 𝑡 → Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑠) = Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡)) |
11 | 10 | adantl 482 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑠 = 𝑡) → Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑠) = Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡)) |
12 | | simpr 477 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑡 ∈ 𝑇) |
13 | | fzfid 12772 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (1...𝑀) ∈ Fin) |
14 | | simpl 473 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝜑) |
15 | | stoweidlem32.7 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐺:(1...𝑀)⟶𝐴) |
16 | 15 | ffvelrnda 6359 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐺‘𝑖) ∈ 𝐴) |
17 | | eleq1 2689 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 = (𝐺‘𝑖) → (𝑓 ∈ 𝐴 ↔ (𝐺‘𝑖) ∈ 𝐴)) |
18 | 17 | anbi2d 740 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 = (𝐺‘𝑖) → ((𝜑 ∧ 𝑓 ∈ 𝐴) ↔ (𝜑 ∧ (𝐺‘𝑖) ∈ 𝐴))) |
19 | | feq1 6026 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 = (𝐺‘𝑖) → (𝑓:𝑇⟶ℝ ↔ (𝐺‘𝑖):𝑇⟶ℝ)) |
20 | 18, 19 | imbi12d 334 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = (𝐺‘𝑖) → (((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ) ↔ ((𝜑 ∧ (𝐺‘𝑖) ∈ 𝐴) → (𝐺‘𝑖):𝑇⟶ℝ))) |
21 | | stoweidlem32.11 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ) |
22 | 20, 21 | vtoclg 3266 |
. . . . . . . . . . . . . 14
⊢ ((𝐺‘𝑖) ∈ 𝐴 → ((𝜑 ∧ (𝐺‘𝑖) ∈ 𝐴) → (𝐺‘𝑖):𝑇⟶ℝ)) |
23 | 16, 22 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝜑 ∧ (𝐺‘𝑖) ∈ 𝐴) → (𝐺‘𝑖):𝑇⟶ℝ)) |
24 | 14, 16, 23 | mp2and 715 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐺‘𝑖):𝑇⟶ℝ) |
25 | 24 | adantlr 751 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → (𝐺‘𝑖):𝑇⟶ℝ) |
26 | | simplr 792 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → 𝑡 ∈ 𝑇) |
27 | 25, 26 | ffvelrnd 6360 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐺‘𝑖)‘𝑡) ∈ ℝ) |
28 | 13, 27 | fsumrecl 14465 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡) ∈ ℝ) |
29 | 8, 11, 12, 28 | fvmptd 6288 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐹‘𝑡) = Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡)) |
30 | 29, 28 | eqeltrd 2701 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐹‘𝑡) ∈ ℝ) |
31 | 30 | recnd 10068 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐹‘𝑡) ∈ ℂ) |
32 | | stoweidlem32.4 |
. . . . . . . . . . 11
⊢ 𝐻 = (𝑡 ∈ 𝑇 ↦ 𝑌) |
33 | | eqidd 2623 |
. . . . . . . . . . . 12
⊢ (𝑠 = 𝑡 → 𝑌 = 𝑌) |
34 | 33 | cbvmptv 4750 |
. . . . . . . . . . 11
⊢ (𝑠 ∈ 𝑇 ↦ 𝑌) = (𝑡 ∈ 𝑇 ↦ 𝑌) |
35 | 32, 34 | eqtr4i 2647 |
. . . . . . . . . 10
⊢ 𝐻 = (𝑠 ∈ 𝑇 ↦ 𝑌) |
36 | 35 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝐻 = (𝑠 ∈ 𝑇 ↦ 𝑌)) |
37 | | eqidd 2623 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑠 = 𝑡) → 𝑌 = 𝑌) |
38 | | stoweidlem32.6 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌 ∈ ℝ) |
39 | 38 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑌 ∈ ℝ) |
40 | 36, 37, 12, 39 | fvmptd 6288 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐻‘𝑡) = 𝑌) |
41 | 40, 39 | eqeltrd 2701 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐻‘𝑡) ∈ ℝ) |
42 | 41 | recnd 10068 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐻‘𝑡) ∈ ℂ) |
43 | 31, 42 | mulcomd 10061 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝐹‘𝑡) · (𝐻‘𝑡)) = ((𝐻‘𝑡) · (𝐹‘𝑡))) |
44 | 40, 29 | oveq12d 6668 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝐻‘𝑡) · (𝐹‘𝑡)) = (𝑌 · Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡))) |
45 | 43, 44 | eqtr2d 2657 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝑌 · Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡)) = ((𝐹‘𝑡) · (𝐻‘𝑡))) |
46 | 2, 45 | mpteq2da 4743 |
. . 3
⊢ (𝜑 → (𝑡 ∈ 𝑇 ↦ (𝑌 · Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡))) = (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡) · (𝐻‘𝑡)))) |
47 | 1, 46 | syl5eq 2668 |
. 2
⊢ (𝜑 → 𝑃 = (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡) · (𝐻‘𝑡)))) |
48 | | stoweidlem32.5 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℕ) |
49 | | stoweidlem32.8 |
. . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴) |
50 | 2, 3, 48, 15, 49, 21 | stoweidlem20 40237 |
. . 3
⊢ (𝜑 → 𝐹 ∈ 𝐴) |
51 | | stoweidlem32.10 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴) |
52 | 51 | stoweidlem4 40221 |
. . . . 5
⊢ ((𝜑 ∧ 𝑌 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑌) ∈ 𝐴) |
53 | 38, 52 | mpdan 702 |
. . . 4
⊢ (𝜑 → (𝑡 ∈ 𝑇 ↦ 𝑌) ∈ 𝐴) |
54 | 32, 53 | syl5eqel 2705 |
. . 3
⊢ (𝜑 → 𝐻 ∈ 𝐴) |
55 | | nfmpt1 4747 |
. . . . . 6
⊢
Ⅎ𝑡(𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡)) |
56 | 3, 55 | nfcxfr 2762 |
. . . . 5
⊢
Ⅎ𝑡𝐹 |
57 | 56 | nfeq2 2780 |
. . . 4
⊢
Ⅎ𝑡 𝑓 = 𝐹 |
58 | | nfmpt1 4747 |
. . . . . 6
⊢
Ⅎ𝑡(𝑡 ∈ 𝑇 ↦ 𝑌) |
59 | 32, 58 | nfcxfr 2762 |
. . . . 5
⊢
Ⅎ𝑡𝐻 |
60 | 59 | nfeq2 2780 |
. . . 4
⊢
Ⅎ𝑡 𝑔 = 𝐻 |
61 | | stoweidlem32.9 |
. . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴) |
62 | 57, 60, 61 | stoweidlem6 40223 |
. . 3
⊢ ((𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐻 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡) · (𝐻‘𝑡))) ∈ 𝐴) |
63 | 50, 54, 62 | mpd3an23 1426 |
. 2
⊢ (𝜑 → (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡) · (𝐻‘𝑡))) ∈ 𝐴) |
64 | 47, 63 | eqeltrd 2701 |
1
⊢ (𝜑 → 𝑃 ∈ 𝐴) |