Step | Hyp | Ref
| Expression |
1 | | stoweidlem21.5 |
. . . 4
⊢ 𝐺 = (𝑡 ∈ 𝑇 ↦ ((𝐻‘𝑡) + 𝑆)) |
2 | | stoweidlem21.4 |
. . . . 5
⊢
Ⅎ𝑡𝜑 |
3 | | stoweidlem21.7 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ∈ ℝ) |
4 | | fvconst2g 7022 |
. . . . . . . 8
⊢ ((𝑆 ∈ ℝ ∧ 𝑡 ∈ 𝑇) → ((𝑇 × {𝑆})‘𝑡) = 𝑆) |
5 | 3, 4 | sylan 583 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝑇 × {𝑆})‘𝑡) = 𝑆) |
6 | 5 | eqcomd 2743 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑆 = ((𝑇 × {𝑆})‘𝑡)) |
7 | 6 | oveq2d 7234 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝐻‘𝑡) + 𝑆) = ((𝐻‘𝑡) + ((𝑇 × {𝑆})‘𝑡))) |
8 | 2, 7 | mpteq2da 5154 |
. . . 4
⊢ (𝜑 → (𝑡 ∈ 𝑇 ↦ ((𝐻‘𝑡) + 𝑆)) = (𝑡 ∈ 𝑇 ↦ ((𝐻‘𝑡) + ((𝑇 × {𝑆})‘𝑡)))) |
9 | 1, 8 | syl5eq 2790 |
. . 3
⊢ (𝜑 → 𝐺 = (𝑡 ∈ 𝑇 ↦ ((𝐻‘𝑡) + ((𝑇 × {𝑆})‘𝑡)))) |
10 | | stoweidlem21.11 |
. . . 4
⊢ (𝜑 → 𝐻 ∈ 𝐴) |
11 | | fconstmpt 5616 |
. . . . . 6
⊢ (𝑇 × {𝑆}) = (𝑠 ∈ 𝑇 ↦ 𝑆) |
12 | | stoweidlem21.3 |
. . . . . . 7
⊢
Ⅎ𝑡𝑆 |
13 | | nfcv 2904 |
. . . . . . 7
⊢
Ⅎ𝑠𝑆 |
14 | | eqidd 2738 |
. . . . . . 7
⊢ (𝑠 = 𝑡 → 𝑆 = 𝑆) |
15 | 12, 13, 14 | cbvmpt 5161 |
. . . . . 6
⊢ (𝑠 ∈ 𝑇 ↦ 𝑆) = (𝑡 ∈ 𝑇 ↦ 𝑆) |
16 | 11, 15 | eqtri 2765 |
. . . . 5
⊢ (𝑇 × {𝑆}) = (𝑡 ∈ 𝑇 ↦ 𝑆) |
17 | 12 | nfeq2 2921 |
. . . . . . . . . 10
⊢
Ⅎ𝑡 𝑥 = 𝑆 |
18 | | simpl 486 |
. . . . . . . . . 10
⊢ ((𝑥 = 𝑆 ∧ 𝑡 ∈ 𝑇) → 𝑥 = 𝑆) |
19 | 17, 18 | mpteq2da 5154 |
. . . . . . . . 9
⊢ (𝑥 = 𝑆 → (𝑡 ∈ 𝑇 ↦ 𝑥) = (𝑡 ∈ 𝑇 ↦ 𝑆)) |
20 | 19 | eleq1d 2822 |
. . . . . . . 8
⊢ (𝑥 = 𝑆 → ((𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴 ↔ (𝑡 ∈ 𝑇 ↦ 𝑆) ∈ 𝐴)) |
21 | 20 | imbi2d 344 |
. . . . . . 7
⊢ (𝑥 = 𝑆 → ((𝜑 → (𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴) ↔ (𝜑 → (𝑡 ∈ 𝑇 ↦ 𝑆) ∈ 𝐴))) |
22 | | stoweidlem21.9 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴) |
23 | 22 | expcom 417 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ → (𝜑 → (𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴)) |
24 | 21, 23 | vtoclga 3494 |
. . . . . 6
⊢ (𝑆 ∈ ℝ → (𝜑 → (𝑡 ∈ 𝑇 ↦ 𝑆) ∈ 𝐴)) |
25 | 3, 24 | mpcom 38 |
. . . . 5
⊢ (𝜑 → (𝑡 ∈ 𝑇 ↦ 𝑆) ∈ 𝐴) |
26 | 16, 25 | eqeltrid 2842 |
. . . 4
⊢ (𝜑 → (𝑇 × {𝑆}) ∈ 𝐴) |
27 | | stoweidlem21.8 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴) |
28 | | stoweidlem21.2 |
. . . . 5
⊢
Ⅎ𝑡𝐻 |
29 | | nfcv 2904 |
. . . . . 6
⊢
Ⅎ𝑡𝑇 |
30 | 12 | nfsn 4628 |
. . . . . 6
⊢
Ⅎ𝑡{𝑆} |
31 | 29, 30 | nfxp 5589 |
. . . . 5
⊢
Ⅎ𝑡(𝑇 × {𝑆}) |
32 | 27, 28, 31 | stoweidlem8 43232 |
. . . 4
⊢ ((𝜑 ∧ 𝐻 ∈ 𝐴 ∧ (𝑇 × {𝑆}) ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝐻‘𝑡) + ((𝑇 × {𝑆})‘𝑡))) ∈ 𝐴) |
33 | 10, 26, 32 | mpd3an23 1465 |
. . 3
⊢ (𝜑 → (𝑡 ∈ 𝑇 ↦ ((𝐻‘𝑡) + ((𝑇 × {𝑆})‘𝑡))) ∈ 𝐴) |
34 | 9, 33 | eqeltrd 2838 |
. 2
⊢ (𝜑 → 𝐺 ∈ 𝐴) |
35 | | simpr 488 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑡 ∈ 𝑇) |
36 | | stoweidlem21.10 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑓 ∈ 𝐴 𝑓:𝑇⟶ℝ) |
37 | | feq1 6531 |
. . . . . . . . . . . . 13
⊢ (𝑓 = 𝐻 → (𝑓:𝑇⟶ℝ ↔ 𝐻:𝑇⟶ℝ)) |
38 | 37 | rspccva 3541 |
. . . . . . . . . . . 12
⊢
((∀𝑓 ∈
𝐴 𝑓:𝑇⟶ℝ ∧ 𝐻 ∈ 𝐴) → 𝐻:𝑇⟶ℝ) |
39 | 36, 10, 38 | syl2anc 587 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐻:𝑇⟶ℝ) |
40 | 39 | ffvelrnda 6909 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐻‘𝑡) ∈ ℝ) |
41 | 3 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑆 ∈ ℝ) |
42 | 40, 41 | readdcld 10867 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝐻‘𝑡) + 𝑆) ∈ ℝ) |
43 | 1 | fvmpt2 6834 |
. . . . . . . . 9
⊢ ((𝑡 ∈ 𝑇 ∧ ((𝐻‘𝑡) + 𝑆) ∈ ℝ) → (𝐺‘𝑡) = ((𝐻‘𝑡) + 𝑆)) |
44 | 35, 42, 43 | syl2anc 587 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐺‘𝑡) = ((𝐻‘𝑡) + 𝑆)) |
45 | 44 | oveq1d 7233 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝐺‘𝑡) − (𝐹‘𝑡)) = (((𝐻‘𝑡) + 𝑆) − (𝐹‘𝑡))) |
46 | 40 | recnd 10866 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐻‘𝑡) ∈ ℂ) |
47 | | stoweidlem21.6 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:𝑇⟶ℝ) |
48 | 47 | ffvelrnda 6909 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐹‘𝑡) ∈ ℝ) |
49 | 48 | recnd 10866 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐹‘𝑡) ∈ ℂ) |
50 | 3 | recnd 10866 |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 ∈ ℂ) |
51 | 50 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑆 ∈ ℂ) |
52 | 46, 49, 51 | subsub3d 11224 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝐻‘𝑡) − ((𝐹‘𝑡) − 𝑆)) = (((𝐻‘𝑡) + 𝑆) − (𝐹‘𝑡))) |
53 | 45, 52 | eqtr4d 2780 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝐺‘𝑡) − (𝐹‘𝑡)) = ((𝐻‘𝑡) − ((𝐹‘𝑡) − 𝑆))) |
54 | 53 | fveq2d 6726 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (abs‘((𝐺‘𝑡) − (𝐹‘𝑡))) = (abs‘((𝐻‘𝑡) − ((𝐹‘𝑡) − 𝑆)))) |
55 | | stoweidlem21.12 |
. . . . . 6
⊢ (𝜑 → ∀𝑡 ∈ 𝑇 (abs‘((𝐻‘𝑡) − ((𝐹‘𝑡) − 𝑆))) < 𝐸) |
56 | 55 | r19.21bi 3130 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (abs‘((𝐻‘𝑡) − ((𝐹‘𝑡) − 𝑆))) < 𝐸) |
57 | 54, 56 | eqbrtrd 5080 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (abs‘((𝐺‘𝑡) − (𝐹‘𝑡))) < 𝐸) |
58 | 57 | ex 416 |
. . 3
⊢ (𝜑 → (𝑡 ∈ 𝑇 → (abs‘((𝐺‘𝑡) − (𝐹‘𝑡))) < 𝐸)) |
59 | 2, 58 | ralrimi 3137 |
. 2
⊢ (𝜑 → ∀𝑡 ∈ 𝑇 (abs‘((𝐺‘𝑡) − (𝐹‘𝑡))) < 𝐸) |
60 | | stoweidlem21.1 |
. . . . 5
⊢
Ⅎ𝑡𝐺 |
61 | 60 | nfeq2 2921 |
. . . 4
⊢
Ⅎ𝑡 𝑓 = 𝐺 |
62 | | fveq1 6721 |
. . . . . . 7
⊢ (𝑓 = 𝐺 → (𝑓‘𝑡) = (𝐺‘𝑡)) |
63 | 62 | oveq1d 7233 |
. . . . . 6
⊢ (𝑓 = 𝐺 → ((𝑓‘𝑡) − (𝐹‘𝑡)) = ((𝐺‘𝑡) − (𝐹‘𝑡))) |
64 | 63 | fveq2d 6726 |
. . . . 5
⊢ (𝑓 = 𝐺 → (abs‘((𝑓‘𝑡) − (𝐹‘𝑡))) = (abs‘((𝐺‘𝑡) − (𝐹‘𝑡)))) |
65 | 64 | breq1d 5068 |
. . . 4
⊢ (𝑓 = 𝐺 → ((abs‘((𝑓‘𝑡) − (𝐹‘𝑡))) < 𝐸 ↔ (abs‘((𝐺‘𝑡) − (𝐹‘𝑡))) < 𝐸)) |
66 | 61, 65 | ralbid 3156 |
. . 3
⊢ (𝑓 = 𝐺 → (∀𝑡 ∈ 𝑇 (abs‘((𝑓‘𝑡) − (𝐹‘𝑡))) < 𝐸 ↔ ∀𝑡 ∈ 𝑇 (abs‘((𝐺‘𝑡) − (𝐹‘𝑡))) < 𝐸)) |
67 | 66 | rspcev 3542 |
. 2
⊢ ((𝐺 ∈ 𝐴 ∧ ∀𝑡 ∈ 𝑇 (abs‘((𝐺‘𝑡) − (𝐹‘𝑡))) < 𝐸) → ∃𝑓 ∈ 𝐴 ∀𝑡 ∈ 𝑇 (abs‘((𝑓‘𝑡) − (𝐹‘𝑡))) < 𝐸) |
68 | 34, 59, 67 | syl2anc 587 |
1
⊢ (𝜑 → ∃𝑓 ∈ 𝐴 ∀𝑡 ∈ 𝑇 (abs‘((𝑓‘𝑡) − (𝐹‘𝑡))) < 𝐸) |