| Step | Hyp | Ref
| Expression |
| 1 | | stoweidlem48.2 |
. 2
⊢
Ⅎ𝑡𝜑 |
| 2 | | stoweidlem48.12 |
. . . . . 6
⊢ (𝜑 → 𝐷 ⊆ 𝑇) |
| 3 | 2 | sselda 3983 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → 𝑡 ∈ 𝑇) |
| 4 | | stoweidlem48.1 |
. . . . . 6
⊢
Ⅎ𝑖𝜑 |
| 5 | | stoweidlem48.3 |
. . . . . . 7
⊢ 𝑌 = {ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)} |
| 6 | | nfra1 3284 |
. . . . . . . 8
⊢
Ⅎ𝑡∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) |
| 7 | | nfcv 2905 |
. . . . . . . 8
⊢
Ⅎ𝑡𝐴 |
| 8 | 6, 7 | nfrabw 3475 |
. . . . . . 7
⊢
Ⅎ𝑡{ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)} |
| 9 | 5, 8 | nfcxfr 2903 |
. . . . . 6
⊢
Ⅎ𝑡𝑌 |
| 10 | | stoweidlem48.4 |
. . . . . 6
⊢ 𝑃 = (𝑓 ∈ 𝑌, 𝑔 ∈ 𝑌 ↦ (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡)))) |
| 11 | | stoweidlem48.5 |
. . . . . 6
⊢ 𝑋 = (seq1(𝑃, 𝑈)‘𝑀) |
| 12 | | stoweidlem48.6 |
. . . . . 6
⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))) |
| 13 | | stoweidlem48.7 |
. . . . . 6
⊢ 𝑍 = (𝑡 ∈ 𝑇 ↦ (seq1( · , (𝐹‘𝑡))‘𝑀)) |
| 14 | | stoweidlem48.14 |
. . . . . 6
⊢ (𝜑 → 𝑇 ∈ V) |
| 15 | | stoweidlem48.8 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℕ) |
| 16 | | stoweidlem48.10 |
. . . . . 6
⊢ (𝜑 → 𝑈:(1...𝑀)⟶𝑌) |
| 17 | 5 | eleq2i 2833 |
. . . . . . . . 9
⊢ (𝑓 ∈ 𝑌 ↔ 𝑓 ∈ {ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)}) |
| 18 | | fveq1 6905 |
. . . . . . . . . . . . 13
⊢ (ℎ = 𝑓 → (ℎ‘𝑡) = (𝑓‘𝑡)) |
| 19 | 18 | breq2d 5155 |
. . . . . . . . . . . 12
⊢ (ℎ = 𝑓 → (0 ≤ (ℎ‘𝑡) ↔ 0 ≤ (𝑓‘𝑡))) |
| 20 | 18 | breq1d 5153 |
. . . . . . . . . . . 12
⊢ (ℎ = 𝑓 → ((ℎ‘𝑡) ≤ 1 ↔ (𝑓‘𝑡) ≤ 1)) |
| 21 | 19, 20 | anbi12d 632 |
. . . . . . . . . . 11
⊢ (ℎ = 𝑓 → ((0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ↔ (0 ≤ (𝑓‘𝑡) ∧ (𝑓‘𝑡) ≤ 1))) |
| 22 | 21 | ralbidv 3178 |
. . . . . . . . . 10
⊢ (ℎ = 𝑓 → (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ↔ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑓‘𝑡) ∧ (𝑓‘𝑡) ≤ 1))) |
| 23 | 22 | elrab 3692 |
. . . . . . . . 9
⊢ (𝑓 ∈ {ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)} ↔ (𝑓 ∈ 𝐴 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑓‘𝑡) ∧ (𝑓‘𝑡) ≤ 1))) |
| 24 | 17, 23 | sylbb 219 |
. . . . . . . 8
⊢ (𝑓 ∈ 𝑌 → (𝑓 ∈ 𝐴 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑓‘𝑡) ∧ (𝑓‘𝑡) ≤ 1))) |
| 25 | 24 | simpld 494 |
. . . . . . 7
⊢ (𝑓 ∈ 𝑌 → 𝑓 ∈ 𝐴) |
| 26 | | stoweidlem48.15 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ) |
| 27 | 25, 26 | sylan2 593 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑌) → 𝑓:𝑇⟶ℝ) |
| 28 | | eqid 2737 |
. . . . . . 7
⊢ (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) = (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) |
| 29 | | stoweidlem48.16 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴) |
| 30 | 1, 5, 28, 26, 29 | stoweidlem16 46031 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝑌) |
| 31 | 4, 9, 10, 11, 12, 13, 14, 15, 16, 27, 30 | fmuldfeq 45598 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝑋‘𝑡) = (𝑍‘𝑡)) |
| 32 | 3, 31 | syldan 591 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (𝑋‘𝑡) = (𝑍‘𝑡)) |
| 33 | | elnnuz 12922 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ ↔ 𝑀 ∈
(ℤ≥‘1)) |
| 34 | 15, 33 | sylib 218 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘1)) |
| 35 | 34 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → 𝑀 ∈
(ℤ≥‘1)) |
| 36 | | nfv 1914 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑖 𝑡 ∈ 𝑇 |
| 37 | 4, 36 | nfan 1899 |
. . . . . . . . . . 11
⊢
Ⅎ𝑖(𝜑 ∧ 𝑡 ∈ 𝑇) |
| 38 | 16 | ffvelcdmda 7104 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑈‘𝑖) ∈ 𝑌) |
| 39 | | fveq1 6905 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (ℎ = (𝑈‘𝑖) → (ℎ‘𝑡) = ((𝑈‘𝑖)‘𝑡)) |
| 40 | 39 | breq2d 5155 |
. . . . . . . . . . . . . . . . . . 19
⊢ (ℎ = (𝑈‘𝑖) → (0 ≤ (ℎ‘𝑡) ↔ 0 ≤ ((𝑈‘𝑖)‘𝑡))) |
| 41 | 39 | breq1d 5153 |
. . . . . . . . . . . . . . . . . . 19
⊢ (ℎ = (𝑈‘𝑖) → ((ℎ‘𝑡) ≤ 1 ↔ ((𝑈‘𝑖)‘𝑡) ≤ 1)) |
| 42 | 40, 41 | anbi12d 632 |
. . . . . . . . . . . . . . . . . 18
⊢ (ℎ = (𝑈‘𝑖) → ((0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ↔ (0 ≤ ((𝑈‘𝑖)‘𝑡) ∧ ((𝑈‘𝑖)‘𝑡) ≤ 1))) |
| 43 | 42 | ralbidv 3178 |
. . . . . . . . . . . . . . . . 17
⊢ (ℎ = (𝑈‘𝑖) → (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ↔ ∀𝑡 ∈ 𝑇 (0 ≤ ((𝑈‘𝑖)‘𝑡) ∧ ((𝑈‘𝑖)‘𝑡) ≤ 1))) |
| 44 | 43, 5 | elrab2 3695 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑈‘𝑖) ∈ 𝑌 ↔ ((𝑈‘𝑖) ∈ 𝐴 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ ((𝑈‘𝑖)‘𝑡) ∧ ((𝑈‘𝑖)‘𝑡) ≤ 1))) |
| 45 | 38, 44 | sylib 218 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝑈‘𝑖) ∈ 𝐴 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ ((𝑈‘𝑖)‘𝑡) ∧ ((𝑈‘𝑖)‘𝑡) ≤ 1))) |
| 46 | 45 | simpld 494 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑈‘𝑖) ∈ 𝐴) |
| 47 | | simpl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝜑) |
| 48 | 47, 46 | jca 511 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝜑 ∧ (𝑈‘𝑖) ∈ 𝐴)) |
| 49 | | eleq1 2829 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 = (𝑈‘𝑖) → (𝑓 ∈ 𝐴 ↔ (𝑈‘𝑖) ∈ 𝐴)) |
| 50 | 49 | anbi2d 630 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 = (𝑈‘𝑖) → ((𝜑 ∧ 𝑓 ∈ 𝐴) ↔ (𝜑 ∧ (𝑈‘𝑖) ∈ 𝐴))) |
| 51 | | feq1 6716 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 = (𝑈‘𝑖) → (𝑓:𝑇⟶ℝ ↔ (𝑈‘𝑖):𝑇⟶ℝ)) |
| 52 | 50, 51 | imbi12d 344 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = (𝑈‘𝑖) → (((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ) ↔ ((𝜑 ∧ (𝑈‘𝑖) ∈ 𝐴) → (𝑈‘𝑖):𝑇⟶ℝ))) |
| 53 | 52, 26 | vtoclg 3554 |
. . . . . . . . . . . . . 14
⊢ ((𝑈‘𝑖) ∈ 𝐴 → ((𝜑 ∧ (𝑈‘𝑖) ∈ 𝐴) → (𝑈‘𝑖):𝑇⟶ℝ)) |
| 54 | 46, 48, 53 | sylc 65 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑈‘𝑖):𝑇⟶ℝ) |
| 55 | 54 | adantlr 715 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → (𝑈‘𝑖):𝑇⟶ℝ) |
| 56 | | simplr 769 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → 𝑡 ∈ 𝑇) |
| 57 | 55, 56 | ffvelcdmd 7105 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝑈‘𝑖)‘𝑡) ∈ ℝ) |
| 58 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡)) = (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡)) |
| 59 | 37, 57, 58 | fmptdf 7137 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡)):(1...𝑀)⟶ℝ) |
| 60 | | simpr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑡 ∈ 𝑇) |
| 61 | | ovex 7464 |
. . . . . . . . . . . . 13
⊢
(1...𝑀) ∈
V |
| 62 | | mptexg 7241 |
. . . . . . . . . . . . 13
⊢
((1...𝑀) ∈ V
→ (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡)) ∈ V) |
| 63 | 61, 62 | mp1i 13 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡)) ∈ V) |
| 64 | 12 | fvmpt2 7027 |
. . . . . . . . . . . 12
⊢ ((𝑡 ∈ 𝑇 ∧ (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡)) ∈ V) → (𝐹‘𝑡) = (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))) |
| 65 | 60, 63, 64 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐹‘𝑡) = (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))) |
| 66 | 65 | feq1d 6720 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝐹‘𝑡):(1...𝑀)⟶ℝ ↔ (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡)):(1...𝑀)⟶ℝ)) |
| 67 | 59, 66 | mpbird 257 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐹‘𝑡):(1...𝑀)⟶ℝ) |
| 68 | 3, 67 | syldan 591 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡):(1...𝑀)⟶ℝ) |
| 69 | 68 | ffvelcdmda 7104 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ 𝐷) ∧ 𝑘 ∈ (1...𝑀)) → ((𝐹‘𝑡)‘𝑘) ∈ ℝ) |
| 70 | | remulcl 11240 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℝ ∧ 𝑗 ∈ ℝ) → (𝑘 · 𝑗) ∈ ℝ) |
| 71 | 70 | adantl 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ 𝐷) ∧ (𝑘 ∈ ℝ ∧ 𝑗 ∈ ℝ)) → (𝑘 · 𝑗) ∈ ℝ) |
| 72 | 35, 69, 71 | seqcl 14063 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (seq1( · , (𝐹‘𝑡))‘𝑀) ∈ ℝ) |
| 73 | 13 | fvmpt2 7027 |
. . . . . 6
⊢ ((𝑡 ∈ 𝑇 ∧ (seq1( · , (𝐹‘𝑡))‘𝑀) ∈ ℝ) → (𝑍‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑀)) |
| 74 | 3, 72, 73 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (𝑍‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑀)) |
| 75 | | nfcv 2905 |
. . . . . . . . 9
⊢
Ⅎ𝑖𝑇 |
| 76 | | nfmpt1 5250 |
. . . . . . . . 9
⊢
Ⅎ𝑖(𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡)) |
| 77 | 75, 76 | nfmpt 5249 |
. . . . . . . 8
⊢
Ⅎ𝑖(𝑡 ∈ 𝑇 ↦ (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))) |
| 78 | 12, 77 | nfcxfr 2903 |
. . . . . . 7
⊢
Ⅎ𝑖𝐹 |
| 79 | | nfcv 2905 |
. . . . . . 7
⊢
Ⅎ𝑖𝑡 |
| 80 | 78, 79 | nffv 6916 |
. . . . . 6
⊢
Ⅎ𝑖(𝐹‘𝑡) |
| 81 | | nfv 1914 |
. . . . . . 7
⊢
Ⅎ𝑖 𝑡 ∈ 𝐷 |
| 82 | 4, 81 | nfan 1899 |
. . . . . 6
⊢
Ⅎ𝑖(𝜑 ∧ 𝑡 ∈ 𝐷) |
| 83 | | nfcv 2905 |
. . . . . 6
⊢
Ⅎ𝑗seq1(
· , (𝐹‘𝑡)) |
| 84 | | eqid 2737 |
. . . . . 6
⊢ seq1(
· , (𝐹‘𝑡)) = seq1( · , (𝐹‘𝑡)) |
| 85 | 15 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → 𝑀 ∈ ℕ) |
| 86 | | simpll 767 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ 𝐷) ∧ 𝑖 ∈ (1...𝑀)) → 𝜑) |
| 87 | | simpr 484 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ 𝐷) ∧ 𝑖 ∈ (1...𝑀)) → 𝑖 ∈ (1...𝑀)) |
| 88 | 3 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ 𝐷) ∧ 𝑖 ∈ (1...𝑀)) → 𝑡 ∈ 𝑇) |
| 89 | 45 | simprd 495 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ∀𝑡 ∈ 𝑇 (0 ≤ ((𝑈‘𝑖)‘𝑡) ∧ ((𝑈‘𝑖)‘𝑡) ≤ 1)) |
| 90 | 89 | r19.21bi 3251 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑡 ∈ 𝑇) → (0 ≤ ((𝑈‘𝑖)‘𝑡) ∧ ((𝑈‘𝑖)‘𝑡) ≤ 1)) |
| 91 | 90 | simpld 494 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑡 ∈ 𝑇) → 0 ≤ ((𝑈‘𝑖)‘𝑡)) |
| 92 | 86, 87, 88, 91 | syl21anc 838 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ 𝐷) ∧ 𝑖 ∈ (1...𝑀)) → 0 ≤ ((𝑈‘𝑖)‘𝑡)) |
| 93 | 65 | fveq1d 6908 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝐹‘𝑡)‘𝑖) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘𝑖)) |
| 94 | 86, 88, 93 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ 𝐷) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐹‘𝑡)‘𝑖) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘𝑖)) |
| 95 | 86, 88, 87, 57 | syl21anc 838 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ 𝐷) ∧ 𝑖 ∈ (1...𝑀)) → ((𝑈‘𝑖)‘𝑡) ∈ ℝ) |
| 96 | 58 | fvmpt2 7027 |
. . . . . . . . 9
⊢ ((𝑖 ∈ (1...𝑀) ∧ ((𝑈‘𝑖)‘𝑡) ∈ ℝ) → ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘𝑖) = ((𝑈‘𝑖)‘𝑡)) |
| 97 | 87, 95, 96 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ 𝐷) ∧ 𝑖 ∈ (1...𝑀)) → ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘𝑖) = ((𝑈‘𝑖)‘𝑡)) |
| 98 | 94, 97 | eqtrd 2777 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ 𝐷) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐹‘𝑡)‘𝑖) = ((𝑈‘𝑖)‘𝑡)) |
| 99 | 92, 98 | breqtrrd 5171 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑡 ∈ 𝐷) ∧ 𝑖 ∈ (1...𝑀)) → 0 ≤ ((𝐹‘𝑡)‘𝑖)) |
| 100 | 90 | simprd 495 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑡 ∈ 𝑇) → ((𝑈‘𝑖)‘𝑡) ≤ 1) |
| 101 | 86, 87, 88, 100 | syl21anc 838 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ 𝐷) ∧ 𝑖 ∈ (1...𝑀)) → ((𝑈‘𝑖)‘𝑡) ≤ 1) |
| 102 | 98, 101 | eqbrtrd 5165 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑡 ∈ 𝐷) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐹‘𝑡)‘𝑖) ≤ 1) |
| 103 | | stoweidlem48.17 |
. . . . . . 7
⊢ (𝜑 → 𝐸 ∈
ℝ+) |
| 104 | 103 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → 𝐸 ∈
ℝ+) |
| 105 | | stoweidlem48.11 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐷 ⊆ ∪ ran
𝑊) |
| 106 | 105 | sselda 3983 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → 𝑡 ∈ ∪ ran
𝑊) |
| 107 | | eluni 4910 |
. . . . . . . . . 10
⊢ (𝑡 ∈ ∪ ran 𝑊 ↔ ∃𝑤(𝑡 ∈ 𝑤 ∧ 𝑤 ∈ ran 𝑊)) |
| 108 | 106, 107 | sylib 218 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → ∃𝑤(𝑡 ∈ 𝑤 ∧ 𝑤 ∈ ran 𝑊)) |
| 109 | | stoweidlem48.9 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑊:(1...𝑀)⟶𝑉) |
| 110 | | ffn 6736 |
. . . . . . . . . . . . . . . 16
⊢ (𝑊:(1...𝑀)⟶𝑉 → 𝑊 Fn (1...𝑀)) |
| 111 | | fvelrnb 6969 |
. . . . . . . . . . . . . . . 16
⊢ (𝑊 Fn (1...𝑀) → (𝑤 ∈ ran 𝑊 ↔ ∃𝑗 ∈ (1...𝑀)(𝑊‘𝑗) = 𝑤)) |
| 112 | 109, 110,
111 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑤 ∈ ran 𝑊 ↔ ∃𝑗 ∈ (1...𝑀)(𝑊‘𝑗) = 𝑤)) |
| 113 | 112 | biimpa 476 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ ran 𝑊) → ∃𝑗 ∈ (1...𝑀)(𝑊‘𝑗) = 𝑤) |
| 114 | 113 | adantrl 716 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ ran 𝑊)) → ∃𝑗 ∈ (1...𝑀)(𝑊‘𝑗) = 𝑤) |
| 115 | | simplr 769 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑤) ∧ (𝑊‘𝑗) = 𝑤) → 𝑡 ∈ 𝑤) |
| 116 | | simpr 484 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑤) ∧ (𝑊‘𝑗) = 𝑤) → (𝑊‘𝑗) = 𝑤) |
| 117 | 115, 116 | eleqtrrd 2844 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑤) ∧ (𝑊‘𝑗) = 𝑤) → 𝑡 ∈ (𝑊‘𝑗)) |
| 118 | 117 | ex 412 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑤) → ((𝑊‘𝑗) = 𝑤 → 𝑡 ∈ (𝑊‘𝑗))) |
| 119 | 118 | reximdv 3170 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑤) → (∃𝑗 ∈ (1...𝑀)(𝑊‘𝑗) = 𝑤 → ∃𝑗 ∈ (1...𝑀)𝑡 ∈ (𝑊‘𝑗))) |
| 120 | 119 | adantrr 717 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ ran 𝑊)) → (∃𝑗 ∈ (1...𝑀)(𝑊‘𝑗) = 𝑤 → ∃𝑗 ∈ (1...𝑀)𝑡 ∈ (𝑊‘𝑗))) |
| 121 | 114, 120 | mpd 15 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ ran 𝑊)) → ∃𝑗 ∈ (1...𝑀)𝑡 ∈ (𝑊‘𝑗)) |
| 122 | 121 | ex 412 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑡 ∈ 𝑤 ∧ 𝑤 ∈ ran 𝑊) → ∃𝑗 ∈ (1...𝑀)𝑡 ∈ (𝑊‘𝑗))) |
| 123 | 122 | exlimdv 1933 |
. . . . . . . . . 10
⊢ (𝜑 → (∃𝑤(𝑡 ∈ 𝑤 ∧ 𝑤 ∈ ran 𝑊) → ∃𝑗 ∈ (1...𝑀)𝑡 ∈ (𝑊‘𝑗))) |
| 124 | 123 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (∃𝑤(𝑡 ∈ 𝑤 ∧ 𝑤 ∈ ran 𝑊) → ∃𝑗 ∈ (1...𝑀)𝑡 ∈ (𝑊‘𝑗))) |
| 125 | 108, 124 | mpd 15 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → ∃𝑗 ∈ (1...𝑀)𝑡 ∈ (𝑊‘𝑗)) |
| 126 | | simplll 775 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝐷) ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑡 ∈ (𝑊‘𝑗)) → 𝜑) |
| 127 | | simplr 769 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝐷) ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑡 ∈ (𝑊‘𝑗)) → 𝑗 ∈ (1...𝑀)) |
| 128 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝐷) ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑡 ∈ (𝑊‘𝑗)) → 𝑡 ∈ (𝑊‘𝑗)) |
| 129 | | nfv 1914 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑖 𝑗 ∈ (1...𝑀) |
| 130 | | nfv 1914 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑖 𝑡 ∈ (𝑊‘𝑗) |
| 131 | 4, 129, 130 | nf3an 1901 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑖(𝜑 ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑡 ∈ (𝑊‘𝑗)) |
| 132 | | nfv 1914 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑖((𝑈‘𝑗)‘𝑡) < 𝐸 |
| 133 | 131, 132 | nfim 1896 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑖((𝜑 ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑡 ∈ (𝑊‘𝑗)) → ((𝑈‘𝑗)‘𝑡) < 𝐸) |
| 134 | | eleq1 2829 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑗 → (𝑖 ∈ (1...𝑀) ↔ 𝑗 ∈ (1...𝑀))) |
| 135 | | fveq2 6906 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = 𝑗 → (𝑊‘𝑖) = (𝑊‘𝑗)) |
| 136 | 135 | eleq2d 2827 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑗 → (𝑡 ∈ (𝑊‘𝑖) ↔ 𝑡 ∈ (𝑊‘𝑗))) |
| 137 | 134, 136 | 3anbi23d 1441 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑗 → ((𝜑 ∧ 𝑖 ∈ (1...𝑀) ∧ 𝑡 ∈ (𝑊‘𝑖)) ↔ (𝜑 ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑡 ∈ (𝑊‘𝑗)))) |
| 138 | | fveq2 6906 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = 𝑗 → (𝑈‘𝑖) = (𝑈‘𝑗)) |
| 139 | 138 | fveq1d 6908 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑗 → ((𝑈‘𝑖)‘𝑡) = ((𝑈‘𝑗)‘𝑡)) |
| 140 | 139 | breq1d 5153 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑗 → (((𝑈‘𝑖)‘𝑡) < 𝐸 ↔ ((𝑈‘𝑗)‘𝑡) < 𝐸)) |
| 141 | 137, 140 | imbi12d 344 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑗 → (((𝜑 ∧ 𝑖 ∈ (1...𝑀) ∧ 𝑡 ∈ (𝑊‘𝑖)) → ((𝑈‘𝑖)‘𝑡) < 𝐸) ↔ ((𝜑 ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑡 ∈ (𝑊‘𝑗)) → ((𝑈‘𝑗)‘𝑡) < 𝐸))) |
| 142 | | stoweidlem48.13 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ∀𝑡 ∈ (𝑊‘𝑖)((𝑈‘𝑖)‘𝑡) < 𝐸) |
| 143 | 142 | r19.21bi 3251 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑡 ∈ (𝑊‘𝑖)) → ((𝑈‘𝑖)‘𝑡) < 𝐸) |
| 144 | 143 | 3impa 1110 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀) ∧ 𝑡 ∈ (𝑊‘𝑖)) → ((𝑈‘𝑖)‘𝑡) < 𝐸) |
| 145 | 133, 141,
144 | chvarfv 2240 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑡 ∈ (𝑊‘𝑗)) → ((𝑈‘𝑗)‘𝑡) < 𝐸) |
| 146 | 126, 127,
128, 145 | syl3anc 1373 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝐷) ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑡 ∈ (𝑊‘𝑗)) → ((𝑈‘𝑗)‘𝑡) < 𝐸) |
| 147 | 146 | ex 412 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ 𝐷) ∧ 𝑗 ∈ (1...𝑀)) → (𝑡 ∈ (𝑊‘𝑗) → ((𝑈‘𝑗)‘𝑡) < 𝐸)) |
| 148 | 147 | reximdva 3168 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (∃𝑗 ∈ (1...𝑀)𝑡 ∈ (𝑊‘𝑗) → ∃𝑗 ∈ (1...𝑀)((𝑈‘𝑗)‘𝑡) < 𝐸)) |
| 149 | 125, 148 | mpd 15 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → ∃𝑗 ∈ (1...𝑀)((𝑈‘𝑗)‘𝑡) < 𝐸) |
| 150 | 82, 129 | nfan 1899 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑖((𝜑 ∧ 𝑡 ∈ 𝐷) ∧ 𝑗 ∈ (1...𝑀)) |
| 151 | | nfcv 2905 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑖𝑗 |
| 152 | 80, 151 | nffv 6916 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑖((𝐹‘𝑡)‘𝑗) |
| 153 | 152 | nfeq1 2921 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑖((𝐹‘𝑡)‘𝑗) = ((𝑈‘𝑗)‘𝑡) |
| 154 | 150, 153 | nfim 1896 |
. . . . . . . . . . 11
⊢
Ⅎ𝑖(((𝜑 ∧ 𝑡 ∈ 𝐷) ∧ 𝑗 ∈ (1...𝑀)) → ((𝐹‘𝑡)‘𝑗) = ((𝑈‘𝑗)‘𝑡)) |
| 155 | 134 | anbi2d 630 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑗 → (((𝜑 ∧ 𝑡 ∈ 𝐷) ∧ 𝑖 ∈ (1...𝑀)) ↔ ((𝜑 ∧ 𝑡 ∈ 𝐷) ∧ 𝑗 ∈ (1...𝑀)))) |
| 156 | | fveq2 6906 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑗 → ((𝐹‘𝑡)‘𝑖) = ((𝐹‘𝑡)‘𝑗)) |
| 157 | 156, 139 | eqeq12d 2753 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑗 → (((𝐹‘𝑡)‘𝑖) = ((𝑈‘𝑖)‘𝑡) ↔ ((𝐹‘𝑡)‘𝑗) = ((𝑈‘𝑗)‘𝑡))) |
| 158 | 155, 157 | imbi12d 344 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑗 → ((((𝜑 ∧ 𝑡 ∈ 𝐷) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐹‘𝑡)‘𝑖) = ((𝑈‘𝑖)‘𝑡)) ↔ (((𝜑 ∧ 𝑡 ∈ 𝐷) ∧ 𝑗 ∈ (1...𝑀)) → ((𝐹‘𝑡)‘𝑗) = ((𝑈‘𝑗)‘𝑡)))) |
| 159 | 154, 158,
98 | chvarfv 2240 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ 𝐷) ∧ 𝑗 ∈ (1...𝑀)) → ((𝐹‘𝑡)‘𝑗) = ((𝑈‘𝑗)‘𝑡)) |
| 160 | 159 | breq1d 5153 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ 𝐷) ∧ 𝑗 ∈ (1...𝑀)) → (((𝐹‘𝑡)‘𝑗) < 𝐸 ↔ ((𝑈‘𝑗)‘𝑡) < 𝐸)) |
| 161 | 160 | biimprd 248 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ 𝐷) ∧ 𝑗 ∈ (1...𝑀)) → (((𝑈‘𝑗)‘𝑡) < 𝐸 → ((𝐹‘𝑡)‘𝑗) < 𝐸)) |
| 162 | 161 | reximdva 3168 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (∃𝑗 ∈ (1...𝑀)((𝑈‘𝑗)‘𝑡) < 𝐸 → ∃𝑗 ∈ (1...𝑀)((𝐹‘𝑡)‘𝑗) < 𝐸)) |
| 163 | 149, 162 | mpd 15 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → ∃𝑗 ∈ (1...𝑀)((𝐹‘𝑡)‘𝑗) < 𝐸) |
| 164 | 80, 82, 83, 84, 85, 68, 99, 102, 104, 163 | fmul01lt1 45601 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (seq1( · , (𝐹‘𝑡))‘𝑀) < 𝐸) |
| 165 | 74, 164 | eqbrtrd 5165 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (𝑍‘𝑡) < 𝐸) |
| 166 | 32, 165 | eqbrtrd 5165 |
. . 3
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (𝑋‘𝑡) < 𝐸) |
| 167 | 166 | ex 412 |
. 2
⊢ (𝜑 → (𝑡 ∈ 𝐷 → (𝑋‘𝑡) < 𝐸)) |
| 168 | 1, 167 | ralrimi 3257 |
1
⊢ (𝜑 → ∀𝑡 ∈ 𝐷 (𝑋‘𝑡) < 𝐸) |