Step | Hyp | Ref
| Expression |
1 | | stoweidlem32.2 |
. . 3
⊢ 𝑃 = (𝑡 ∈ 𝑇 ↦ (𝑌 · Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡))) |
2 | | stoweidlem32.1 |
. . . 4
⊢
Ⅎ𝑡𝜑 |
3 | | stoweidlem32.3 |
. . . . . . . . . . 11
⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡)) |
4 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝑠 → ((𝐺‘𝑖)‘𝑡) = ((𝐺‘𝑖)‘𝑠)) |
5 | 4 | sumeq2sdv 14282 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑠 → Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡) = Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑠)) |
6 | 5 | cbvmptv 4678 |
. . . . . . . . . . 11
⊢ (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡)) = (𝑠 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑠)) |
7 | 3, 6 | eqtri 2632 |
. . . . . . . . . 10
⊢ 𝐹 = (𝑠 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑠)) |
8 | 7 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝐹 = (𝑠 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑠))) |
9 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑠 = 𝑡 → ((𝐺‘𝑖)‘𝑠) = ((𝐺‘𝑖)‘𝑡)) |
10 | 9 | sumeq2sdv 14282 |
. . . . . . . . . 10
⊢ (𝑠 = 𝑡 → Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑠) = Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡)) |
11 | 10 | adantl 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑠 = 𝑡) → Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑠) = Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡)) |
12 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑡 ∈ 𝑇) |
13 | | fzfid 12634 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (1...𝑀) ∈ Fin) |
14 | | simpl 472 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝜑) |
15 | | stoweidlem32.7 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐺:(1...𝑀)⟶𝐴) |
16 | 15 | fnvinran 38196 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐺‘𝑖) ∈ 𝐴) |
17 | | eleq1 2676 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 = (𝐺‘𝑖) → (𝑓 ∈ 𝐴 ↔ (𝐺‘𝑖) ∈ 𝐴)) |
18 | 17 | anbi2d 736 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 = (𝐺‘𝑖) → ((𝜑 ∧ 𝑓 ∈ 𝐴) ↔ (𝜑 ∧ (𝐺‘𝑖) ∈ 𝐴))) |
19 | | feq1 5939 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 = (𝐺‘𝑖) → (𝑓:𝑇⟶ℝ ↔ (𝐺‘𝑖):𝑇⟶ℝ)) |
20 | 18, 19 | imbi12d 333 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = (𝐺‘𝑖) → (((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ) ↔ ((𝜑 ∧ (𝐺‘𝑖) ∈ 𝐴) → (𝐺‘𝑖):𝑇⟶ℝ))) |
21 | | stoweidlem32.11 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ) |
22 | 20, 21 | vtoclg 3239 |
. . . . . . . . . . . . . 14
⊢ ((𝐺‘𝑖) ∈ 𝐴 → ((𝜑 ∧ (𝐺‘𝑖) ∈ 𝐴) → (𝐺‘𝑖):𝑇⟶ℝ)) |
23 | 16, 22 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝜑 ∧ (𝐺‘𝑖) ∈ 𝐴) → (𝐺‘𝑖):𝑇⟶ℝ)) |
24 | 14, 16, 23 | mp2and 711 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐺‘𝑖):𝑇⟶ℝ) |
25 | 24 | adantlr 747 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → (𝐺‘𝑖):𝑇⟶ℝ) |
26 | | simplr 788 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → 𝑡 ∈ 𝑇) |
27 | 25, 26 | ffvelrnd 6268 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐺‘𝑖)‘𝑡) ∈ ℝ) |
28 | 13, 27 | fsumrecl 14312 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡) ∈ ℝ) |
29 | 8, 11, 12, 28 | fvmptd 6197 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐹‘𝑡) = Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡)) |
30 | 29, 28 | eqeltrd 2688 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐹‘𝑡) ∈ ℝ) |
31 | 30 | recnd 9947 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐹‘𝑡) ∈ ℂ) |
32 | | stoweidlem32.4 |
. . . . . . . . . . 11
⊢ 𝐻 = (𝑡 ∈ 𝑇 ↦ 𝑌) |
33 | | eqidd 2611 |
. . . . . . . . . . . 12
⊢ (𝑠 = 𝑡 → 𝑌 = 𝑌) |
34 | 33 | cbvmptv 4678 |
. . . . . . . . . . 11
⊢ (𝑠 ∈ 𝑇 ↦ 𝑌) = (𝑡 ∈ 𝑇 ↦ 𝑌) |
35 | 32, 34 | eqtr4i 2635 |
. . . . . . . . . 10
⊢ 𝐻 = (𝑠 ∈ 𝑇 ↦ 𝑌) |
36 | 35 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝐻 = (𝑠 ∈ 𝑇 ↦ 𝑌)) |
37 | | eqidd 2611 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑠 = 𝑡) → 𝑌 = 𝑌) |
38 | | stoweidlem32.6 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌 ∈ ℝ) |
39 | 38 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑌 ∈ ℝ) |
40 | 36, 37, 12, 39 | fvmptd 6197 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐻‘𝑡) = 𝑌) |
41 | 40, 39 | eqeltrd 2688 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐻‘𝑡) ∈ ℝ) |
42 | 41 | recnd 9947 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐻‘𝑡) ∈ ℂ) |
43 | 31, 42 | mulcomd 9940 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝐹‘𝑡) · (𝐻‘𝑡)) = ((𝐻‘𝑡) · (𝐹‘𝑡))) |
44 | 40, 29 | oveq12d 6567 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝐻‘𝑡) · (𝐹‘𝑡)) = (𝑌 · Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡))) |
45 | 43, 44 | eqtr2d 2645 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝑌 · Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡)) = ((𝐹‘𝑡) · (𝐻‘𝑡))) |
46 | 2, 45 | mpteq2da 4671 |
. . 3
⊢ (𝜑 → (𝑡 ∈ 𝑇 ↦ (𝑌 · Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡))) = (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡) · (𝐻‘𝑡)))) |
47 | 1, 46 | syl5eq 2656 |
. 2
⊢ (𝜑 → 𝑃 = (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡) · (𝐻‘𝑡)))) |
48 | | stoweidlem32.5 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℕ) |
49 | | stoweidlem32.8 |
. . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴) |
50 | 2, 3, 48, 15, 49, 21 | stoweidlem20 38913 |
. . 3
⊢ (𝜑 → 𝐹 ∈ 𝐴) |
51 | | stoweidlem32.10 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴) |
52 | 51 | stoweidlem4 38897 |
. . . . 5
⊢ ((𝜑 ∧ 𝑌 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑌) ∈ 𝐴) |
53 | 38, 52 | mpdan 699 |
. . . 4
⊢ (𝜑 → (𝑡 ∈ 𝑇 ↦ 𝑌) ∈ 𝐴) |
54 | 32, 53 | syl5eqel 2692 |
. . 3
⊢ (𝜑 → 𝐻 ∈ 𝐴) |
55 | | nfmpt1 4675 |
. . . . . 6
⊢
Ⅎ𝑡(𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡)) |
56 | 3, 55 | nfcxfr 2749 |
. . . . 5
⊢
Ⅎ𝑡𝐹 |
57 | 56 | nfeq2 2766 |
. . . 4
⊢
Ⅎ𝑡 𝑓 = 𝐹 |
58 | | nfmpt1 4675 |
. . . . . 6
⊢
Ⅎ𝑡(𝑡 ∈ 𝑇 ↦ 𝑌) |
59 | 32, 58 | nfcxfr 2749 |
. . . . 5
⊢
Ⅎ𝑡𝐻 |
60 | 59 | nfeq2 2766 |
. . . 4
⊢
Ⅎ𝑡 𝑔 = 𝐻 |
61 | | stoweidlem32.9 |
. . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴) |
62 | 57, 60, 61 | stoweidlem6 38899 |
. . 3
⊢ ((𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐻 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡) · (𝐻‘𝑡))) ∈ 𝐴) |
63 | 50, 54, 62 | mpd3an23 1418 |
. 2
⊢ (𝜑 → (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡) · (𝐻‘𝑡))) ∈ 𝐴) |
64 | 47, 63 | eqeltrd 2688 |
1
⊢ (𝜑 → 𝑃 ∈ 𝐴) |