| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | stoweidlem32.2 | . . 3
⊢ 𝑃 = (𝑡 ∈ 𝑇 ↦ (𝑌 · Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡))) | 
| 2 |  | stoweidlem32.1 | . . . 4
⊢
Ⅎ𝑡𝜑 | 
| 3 |  | stoweidlem32.3 | . . . . . . . . . 10
⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡)) | 
| 4 |  | fveq2 6906 | . . . . . . . . . . . 12
⊢ (𝑡 = 𝑠 → ((𝐺‘𝑖)‘𝑡) = ((𝐺‘𝑖)‘𝑠)) | 
| 5 | 4 | sumeq2sdv 15739 | . . . . . . . . . . 11
⊢ (𝑡 = 𝑠 → Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡) = Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑠)) | 
| 6 | 5 | cbvmptv 5255 | . . . . . . . . . 10
⊢ (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡)) = (𝑠 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑠)) | 
| 7 | 3, 6 | eqtri 2765 | . . . . . . . . 9
⊢ 𝐹 = (𝑠 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑠)) | 
| 8 |  | fveq2 6906 | . . . . . . . . . 10
⊢ (𝑠 = 𝑡 → ((𝐺‘𝑖)‘𝑠) = ((𝐺‘𝑖)‘𝑡)) | 
| 9 | 8 | sumeq2sdv 15739 | . . . . . . . . 9
⊢ (𝑠 = 𝑡 → Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑠) = Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡)) | 
| 10 |  | simpr 484 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑡 ∈ 𝑇) | 
| 11 |  | fzfid 14014 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (1...𝑀) ∈ Fin) | 
| 12 |  | simpl 482 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝜑) | 
| 13 |  | stoweidlem32.7 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐺:(1...𝑀)⟶𝐴) | 
| 14 | 13 | ffvelcdmda 7104 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐺‘𝑖) ∈ 𝐴) | 
| 15 |  | eleq1 2829 | . . . . . . . . . . . . . . . . 17
⊢ (𝑓 = (𝐺‘𝑖) → (𝑓 ∈ 𝐴 ↔ (𝐺‘𝑖) ∈ 𝐴)) | 
| 16 | 15 | anbi2d 630 | . . . . . . . . . . . . . . . 16
⊢ (𝑓 = (𝐺‘𝑖) → ((𝜑 ∧ 𝑓 ∈ 𝐴) ↔ (𝜑 ∧ (𝐺‘𝑖) ∈ 𝐴))) | 
| 17 |  | feq1 6716 | . . . . . . . . . . . . . . . 16
⊢ (𝑓 = (𝐺‘𝑖) → (𝑓:𝑇⟶ℝ ↔ (𝐺‘𝑖):𝑇⟶ℝ)) | 
| 18 | 16, 17 | imbi12d 344 | . . . . . . . . . . . . . . 15
⊢ (𝑓 = (𝐺‘𝑖) → (((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ) ↔ ((𝜑 ∧ (𝐺‘𝑖) ∈ 𝐴) → (𝐺‘𝑖):𝑇⟶ℝ))) | 
| 19 |  | stoweidlem32.11 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ) | 
| 20 | 18, 19 | vtoclg 3554 | . . . . . . . . . . . . . 14
⊢ ((𝐺‘𝑖) ∈ 𝐴 → ((𝜑 ∧ (𝐺‘𝑖) ∈ 𝐴) → (𝐺‘𝑖):𝑇⟶ℝ)) | 
| 21 | 14, 20 | syl 17 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝜑 ∧ (𝐺‘𝑖) ∈ 𝐴) → (𝐺‘𝑖):𝑇⟶ℝ)) | 
| 22 | 12, 14, 21 | mp2and 699 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐺‘𝑖):𝑇⟶ℝ) | 
| 23 | 22 | adantlr 715 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → (𝐺‘𝑖):𝑇⟶ℝ) | 
| 24 |  | simplr 769 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → 𝑡 ∈ 𝑇) | 
| 25 | 23, 24 | ffvelcdmd 7105 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐺‘𝑖)‘𝑡) ∈ ℝ) | 
| 26 | 11, 25 | fsumrecl 15770 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡) ∈ ℝ) | 
| 27 | 7, 9, 10, 26 | fvmptd3 7039 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐹‘𝑡) = Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡)) | 
| 28 | 27, 26 | eqeltrd 2841 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐹‘𝑡) ∈ ℝ) | 
| 29 | 28 | recnd 11289 | . . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐹‘𝑡) ∈ ℂ) | 
| 30 |  | stoweidlem32.4 | . . . . . . . . . 10
⊢ 𝐻 = (𝑡 ∈ 𝑇 ↦ 𝑌) | 
| 31 |  | eqidd 2738 | . . . . . . . . . . 11
⊢ (𝑠 = 𝑡 → 𝑌 = 𝑌) | 
| 32 | 31 | cbvmptv 5255 | . . . . . . . . . 10
⊢ (𝑠 ∈ 𝑇 ↦ 𝑌) = (𝑡 ∈ 𝑇 ↦ 𝑌) | 
| 33 | 30, 32 | eqtr4i 2768 | . . . . . . . . 9
⊢ 𝐻 = (𝑠 ∈ 𝑇 ↦ 𝑌) | 
| 34 |  | stoweidlem32.6 | . . . . . . . . . 10
⊢ (𝜑 → 𝑌 ∈ ℝ) | 
| 35 | 34 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑌 ∈ ℝ) | 
| 36 | 33, 31, 10, 35 | fvmptd3 7039 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐻‘𝑡) = 𝑌) | 
| 37 | 36, 35 | eqeltrd 2841 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐻‘𝑡) ∈ ℝ) | 
| 38 | 37 | recnd 11289 | . . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐻‘𝑡) ∈ ℂ) | 
| 39 | 29, 38 | mulcomd 11282 | . . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝐹‘𝑡) · (𝐻‘𝑡)) = ((𝐻‘𝑡) · (𝐹‘𝑡))) | 
| 40 | 36, 27 | oveq12d 7449 | . . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝐻‘𝑡) · (𝐹‘𝑡)) = (𝑌 · Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡))) | 
| 41 | 39, 40 | eqtr2d 2778 | . . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝑌 · Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡)) = ((𝐹‘𝑡) · (𝐻‘𝑡))) | 
| 42 | 2, 41 | mpteq2da 5240 | . . 3
⊢ (𝜑 → (𝑡 ∈ 𝑇 ↦ (𝑌 · Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡))) = (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡) · (𝐻‘𝑡)))) | 
| 43 | 1, 42 | eqtrid 2789 | . 2
⊢ (𝜑 → 𝑃 = (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡) · (𝐻‘𝑡)))) | 
| 44 |  | stoweidlem32.5 | . . . 4
⊢ (𝜑 → 𝑀 ∈ ℕ) | 
| 45 |  | stoweidlem32.8 | . . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴) | 
| 46 | 2, 3, 44, 13, 45, 19 | stoweidlem20 46035 | . . 3
⊢ (𝜑 → 𝐹 ∈ 𝐴) | 
| 47 |  | stoweidlem32.10 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴) | 
| 48 | 47 | stoweidlem4 46019 | . . . . 5
⊢ ((𝜑 ∧ 𝑌 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑌) ∈ 𝐴) | 
| 49 | 34, 48 | mpdan 687 | . . . 4
⊢ (𝜑 → (𝑡 ∈ 𝑇 ↦ 𝑌) ∈ 𝐴) | 
| 50 | 30, 49 | eqeltrid 2845 | . . 3
⊢ (𝜑 → 𝐻 ∈ 𝐴) | 
| 51 |  | nfmpt1 5250 | . . . . . 6
⊢
Ⅎ𝑡(𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡)) | 
| 52 | 3, 51 | nfcxfr 2903 | . . . . 5
⊢
Ⅎ𝑡𝐹 | 
| 53 | 52 | nfeq2 2923 | . . . 4
⊢
Ⅎ𝑡 𝑓 = 𝐹 | 
| 54 |  | nfmpt1 5250 | . . . . . 6
⊢
Ⅎ𝑡(𝑡 ∈ 𝑇 ↦ 𝑌) | 
| 55 | 30, 54 | nfcxfr 2903 | . . . . 5
⊢
Ⅎ𝑡𝐻 | 
| 56 | 55 | nfeq2 2923 | . . . 4
⊢
Ⅎ𝑡 𝑔 = 𝐻 | 
| 57 |  | stoweidlem32.9 | . . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴) | 
| 58 | 53, 56, 57 | stoweidlem6 46021 | . . 3
⊢ ((𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐻 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡) · (𝐻‘𝑡))) ∈ 𝐴) | 
| 59 | 46, 50, 58 | mpd3an23 1465 | . 2
⊢ (𝜑 → (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡) · (𝐻‘𝑡))) ∈ 𝐴) | 
| 60 | 43, 59 | eqeltrd 2841 | 1
⊢ (𝜑 → 𝑃 ∈ 𝐴) |