Proof of Theorem stoweidlem22
Step | Hyp | Ref
| Expression |
1 | | stoweidlem22.8 |
. . . 4
⊢
Ⅎ𝑡𝜑 |
2 | | stoweidlem22.9 |
. . . . 5
⊢
Ⅎ𝑡𝐹 |
3 | 2 | nfel1 2765 |
. . . 4
⊢
Ⅎ𝑡 𝐹 ∈ 𝐴 |
4 | | stoweidlem22.10 |
. . . . 5
⊢
Ⅎ𝑡𝐺 |
5 | 4 | nfel1 2765 |
. . . 4
⊢
Ⅎ𝑡 𝐺 ∈ 𝐴 |
6 | 1, 3, 5 | nf3an 1819 |
. . 3
⊢
Ⅎ𝑡(𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴) |
7 | | simpr 476 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴) ∧ 𝑡 ∈ 𝑇) → 𝑡 ∈ 𝑇) |
8 | | simpl1 1057 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴) ∧ 𝑡 ∈ 𝑇) → 𝜑) |
9 | | stoweidlem22.2 |
. . . . . . . . . . . 12
⊢ 𝐼 = (𝑡 ∈ 𝑇 ↦ -1) |
10 | | neg1rr 11002 |
. . . . . . . . . . . . 13
⊢ -1 ∈
ℝ |
11 | | stoweidlem22.7 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴) |
12 | 11 | stoweidlem4 38897 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ -1 ∈ ℝ) →
(𝑡 ∈ 𝑇 ↦ -1) ∈ 𝐴) |
13 | 10, 12 | mpan2 703 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑡 ∈ 𝑇 ↦ -1) ∈ 𝐴) |
14 | 9, 13 | syl5eqel 2692 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐼 ∈ 𝐴) |
15 | | eleq1 2676 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = 𝐼 → (𝑓 ∈ 𝐴 ↔ 𝐼 ∈ 𝐴)) |
16 | 15 | anbi2d 736 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = 𝐼 → ((𝜑 ∧ 𝑓 ∈ 𝐴) ↔ (𝜑 ∧ 𝐼 ∈ 𝐴))) |
17 | | feq1 5939 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = 𝐼 → (𝑓:𝑇⟶ℝ ↔ 𝐼:𝑇⟶ℝ)) |
18 | 16, 17 | imbi12d 333 |
. . . . . . . . . . . . 13
⊢ (𝑓 = 𝐼 → (((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ) ↔ ((𝜑 ∧ 𝐼 ∈ 𝐴) → 𝐼:𝑇⟶ℝ))) |
19 | | stoweidlem22.4 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ) |
20 | 18, 19 | vtoclg 3239 |
. . . . . . . . . . . 12
⊢ (𝐼 ∈ 𝐴 → ((𝜑 ∧ 𝐼 ∈ 𝐴) → 𝐼:𝑇⟶ℝ)) |
21 | 20 | anabsi7 856 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐼 ∈ 𝐴) → 𝐼:𝑇⟶ℝ) |
22 | 14, 21 | mpdan 699 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐼:𝑇⟶ℝ) |
23 | 8, 22 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴) ∧ 𝑡 ∈ 𝑇) → 𝐼:𝑇⟶ℝ) |
24 | 23, 7 | ffvelrnd 6268 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴) ∧ 𝑡 ∈ 𝑇) → (𝐼‘𝑡) ∈ ℝ) |
25 | | simpl3 1059 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴) ∧ 𝑡 ∈ 𝑇) → 𝐺 ∈ 𝐴) |
26 | | eleq1 2676 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = 𝐺 → (𝑓 ∈ 𝐴 ↔ 𝐺 ∈ 𝐴)) |
27 | 26 | anbi2d 736 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = 𝐺 → ((𝜑 ∧ 𝑓 ∈ 𝐴) ↔ (𝜑 ∧ 𝐺 ∈ 𝐴))) |
28 | | feq1 5939 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = 𝐺 → (𝑓:𝑇⟶ℝ ↔ 𝐺:𝑇⟶ℝ)) |
29 | 27, 28 | imbi12d 333 |
. . . . . . . . . . . . 13
⊢ (𝑓 = 𝐺 → (((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ) ↔ ((𝜑 ∧ 𝐺 ∈ 𝐴) → 𝐺:𝑇⟶ℝ))) |
30 | 29, 19 | vtoclg 3239 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ 𝐴 → ((𝜑 ∧ 𝐺 ∈ 𝐴) → 𝐺:𝑇⟶ℝ)) |
31 | 30 | anabsi7 856 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐺 ∈ 𝐴) → 𝐺:𝑇⟶ℝ) |
32 | 31 | 3adant3 1074 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐺 ∈ 𝐴 ∧ 𝑡 ∈ 𝑇) → 𝐺:𝑇⟶ℝ) |
33 | | simp3 1056 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐺 ∈ 𝐴 ∧ 𝑡 ∈ 𝑇) → 𝑡 ∈ 𝑇) |
34 | 32, 33 | ffvelrnd 6268 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐺 ∈ 𝐴 ∧ 𝑡 ∈ 𝑇) → (𝐺‘𝑡) ∈ ℝ) |
35 | 8, 25, 7, 34 | syl3anc 1318 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴) ∧ 𝑡 ∈ 𝑇) → (𝐺‘𝑡) ∈ ℝ) |
36 | 24, 35 | remulcld 9949 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴) ∧ 𝑡 ∈ 𝑇) → ((𝐼‘𝑡) · (𝐺‘𝑡)) ∈ ℝ) |
37 | | stoweidlem22.3 |
. . . . . . . 8
⊢ 𝐿 = (𝑡 ∈ 𝑇 ↦ ((𝐼‘𝑡) · (𝐺‘𝑡))) |
38 | 37 | fvmpt2 6200 |
. . . . . . 7
⊢ ((𝑡 ∈ 𝑇 ∧ ((𝐼‘𝑡) · (𝐺‘𝑡)) ∈ ℝ) → (𝐿‘𝑡) = ((𝐼‘𝑡) · (𝐺‘𝑡))) |
39 | 7, 36, 38 | syl2anc 691 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴) ∧ 𝑡 ∈ 𝑇) → (𝐿‘𝑡) = ((𝐼‘𝑡) · (𝐺‘𝑡))) |
40 | 9 | fvmpt2 6200 |
. . . . . . . . 9
⊢ ((𝑡 ∈ 𝑇 ∧ -1 ∈ ℝ) → (𝐼‘𝑡) = -1) |
41 | 10, 40 | mpan2 703 |
. . . . . . . 8
⊢ (𝑡 ∈ 𝑇 → (𝐼‘𝑡) = -1) |
42 | 41 | adantl 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴) ∧ 𝑡 ∈ 𝑇) → (𝐼‘𝑡) = -1) |
43 | 42 | oveq1d 6564 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴) ∧ 𝑡 ∈ 𝑇) → ((𝐼‘𝑡) · (𝐺‘𝑡)) = (-1 · (𝐺‘𝑡))) |
44 | 35 | recnd 9947 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴) ∧ 𝑡 ∈ 𝑇) → (𝐺‘𝑡) ∈ ℂ) |
45 | 44 | mulm1d 10361 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴) ∧ 𝑡 ∈ 𝑇) → (-1 · (𝐺‘𝑡)) = -(𝐺‘𝑡)) |
46 | 39, 43, 45 | 3eqtrd 2648 |
. . . . 5
⊢ (((𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴) ∧ 𝑡 ∈ 𝑇) → (𝐿‘𝑡) = -(𝐺‘𝑡)) |
47 | 46 | oveq2d 6565 |
. . . 4
⊢ (((𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴) ∧ 𝑡 ∈ 𝑇) → ((𝐹‘𝑡) + (𝐿‘𝑡)) = ((𝐹‘𝑡) + -(𝐺‘𝑡))) |
48 | | simpl2 1058 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴) ∧ 𝑡 ∈ 𝑇) → 𝐹 ∈ 𝐴) |
49 | | eleq1 2676 |
. . . . . . . . . . . 12
⊢ (𝑓 = 𝐹 → (𝑓 ∈ 𝐴 ↔ 𝐹 ∈ 𝐴)) |
50 | 49 | anbi2d 736 |
. . . . . . . . . . 11
⊢ (𝑓 = 𝐹 → ((𝜑 ∧ 𝑓 ∈ 𝐴) ↔ (𝜑 ∧ 𝐹 ∈ 𝐴))) |
51 | | feq1 5939 |
. . . . . . . . . . 11
⊢ (𝑓 = 𝐹 → (𝑓:𝑇⟶ℝ ↔ 𝐹:𝑇⟶ℝ)) |
52 | 50, 51 | imbi12d 333 |
. . . . . . . . . 10
⊢ (𝑓 = 𝐹 → (((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ) ↔ ((𝜑 ∧ 𝐹 ∈ 𝐴) → 𝐹:𝑇⟶ℝ))) |
53 | 52, 19 | vtoclg 3239 |
. . . . . . . . 9
⊢ (𝐹 ∈ 𝐴 → ((𝜑 ∧ 𝐹 ∈ 𝐴) → 𝐹:𝑇⟶ℝ)) |
54 | 53 | anabsi7 856 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐹 ∈ 𝐴) → 𝐹:𝑇⟶ℝ) |
55 | 8, 48, 54 | syl2anc 691 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴) ∧ 𝑡 ∈ 𝑇) → 𝐹:𝑇⟶ℝ) |
56 | 55, 7 | ffvelrnd 6268 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴) ∧ 𝑡 ∈ 𝑇) → (𝐹‘𝑡) ∈ ℝ) |
57 | 56 | recnd 9947 |
. . . . 5
⊢ (((𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴) ∧ 𝑡 ∈ 𝑇) → (𝐹‘𝑡) ∈ ℂ) |
58 | 57, 44 | negsubd 10277 |
. . . 4
⊢ (((𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴) ∧ 𝑡 ∈ 𝑇) → ((𝐹‘𝑡) + -(𝐺‘𝑡)) = ((𝐹‘𝑡) − (𝐺‘𝑡))) |
59 | 47, 58 | eqtr2d 2645 |
. . 3
⊢ (((𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴) ∧ 𝑡 ∈ 𝑇) → ((𝐹‘𝑡) − (𝐺‘𝑡)) = ((𝐹‘𝑡) + (𝐿‘𝑡))) |
60 | 6, 59 | mpteq2da 4671 |
. 2
⊢ ((𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡) − (𝐺‘𝑡))) = (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡) + (𝐿‘𝑡)))) |
61 | 14 | 3ad2ant1 1075 |
. . . . 5
⊢ ((𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴) → 𝐼 ∈ 𝐴) |
62 | | nfmpt1 4675 |
. . . . . . . 8
⊢
Ⅎ𝑡(𝑡 ∈ 𝑇 ↦ -1) |
63 | 9, 62 | nfcxfr 2749 |
. . . . . . 7
⊢
Ⅎ𝑡𝐼 |
64 | 63 | nfeq2 2766 |
. . . . . 6
⊢
Ⅎ𝑡 𝑓 = 𝐼 |
65 | 4 | nfeq2 2766 |
. . . . . 6
⊢
Ⅎ𝑡 𝑔 = 𝐺 |
66 | | stoweidlem22.6 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴) |
67 | 64, 65, 66 | stoweidlem6 38899 |
. . . . 5
⊢ ((𝜑 ∧ 𝐼 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝐼‘𝑡) · (𝐺‘𝑡))) ∈ 𝐴) |
68 | 61, 67 | syld3an2 1365 |
. . . 4
⊢ ((𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝐼‘𝑡) · (𝐺‘𝑡))) ∈ 𝐴) |
69 | 37, 68 | syl5eqel 2692 |
. . 3
⊢ ((𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴) → 𝐿 ∈ 𝐴) |
70 | | stoweidlem22.5 |
. . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴) |
71 | | nfmpt1 4675 |
. . . . 5
⊢
Ⅎ𝑡(𝑡 ∈ 𝑇 ↦ ((𝐼‘𝑡) · (𝐺‘𝑡))) |
72 | 37, 71 | nfcxfr 2749 |
. . . 4
⊢
Ⅎ𝑡𝐿 |
73 | 70, 2, 72 | stoweidlem8 38901 |
. . 3
⊢ ((𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐿 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡) + (𝐿‘𝑡))) ∈ 𝐴) |
74 | 69, 73 | syld3an3 1363 |
. 2
⊢ ((𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡) + (𝐿‘𝑡))) ∈ 𝐴) |
75 | 60, 74 | eqeltrd 2688 |
1
⊢ ((𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡) − (𝐺‘𝑡))) ∈ 𝐴) |