Step |
Hyp |
Ref |
Expression |
1 |
|
stoweidlem22.8 |
⊢ Ⅎ 𝑡 𝜑 |
2 |
|
stoweidlem22.9 |
⊢ Ⅎ 𝑡 𝐹 |
3 |
|
stoweidlem22.10 |
⊢ Ⅎ 𝑡 𝐺 |
4 |
|
stoweidlem22.1 |
⊢ 𝐻 = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐺 ‘ 𝑡 ) ) ) |
5 |
|
stoweidlem22.2 |
⊢ 𝐼 = ( 𝑡 ∈ 𝑇 ↦ - 1 ) |
6 |
|
stoweidlem22.3 |
⊢ 𝐿 = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐼 ‘ 𝑡 ) · ( 𝐺 ‘ 𝑡 ) ) ) |
7 |
|
stoweidlem22.4 |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ ) |
8 |
|
stoweidlem22.5 |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 ) |
9 |
|
stoweidlem22.6 |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 ) |
10 |
|
stoweidlem22.7 |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) ∈ 𝐴 ) |
11 |
2
|
nfel1 |
⊢ Ⅎ 𝑡 𝐹 ∈ 𝐴 |
12 |
3
|
nfel1 |
⊢ Ⅎ 𝑡 𝐺 ∈ 𝐴 |
13 |
1 11 12
|
nf3an |
⊢ Ⅎ 𝑡 ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) |
14 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → 𝑡 ∈ 𝑇 ) |
15 |
|
simpl1 |
⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → 𝜑 ) |
16 |
|
neg1rr |
⊢ - 1 ∈ ℝ |
17 |
10
|
stoweidlem4 |
⊢ ( ( 𝜑 ∧ - 1 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ - 1 ) ∈ 𝐴 ) |
18 |
16 17
|
mpan2 |
⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ - 1 ) ∈ 𝐴 ) |
19 |
5 18
|
eqeltrid |
⊢ ( 𝜑 → 𝐼 ∈ 𝐴 ) |
20 |
|
eleq1 |
⊢ ( 𝑓 = 𝐼 → ( 𝑓 ∈ 𝐴 ↔ 𝐼 ∈ 𝐴 ) ) |
21 |
20
|
anbi2d |
⊢ ( 𝑓 = 𝐼 → ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝐼 ∈ 𝐴 ) ) ) |
22 |
|
feq1 |
⊢ ( 𝑓 = 𝐼 → ( 𝑓 : 𝑇 ⟶ ℝ ↔ 𝐼 : 𝑇 ⟶ ℝ ) ) |
23 |
21 22
|
imbi12d |
⊢ ( 𝑓 = 𝐼 → ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ ) ↔ ( ( 𝜑 ∧ 𝐼 ∈ 𝐴 ) → 𝐼 : 𝑇 ⟶ ℝ ) ) ) |
24 |
23 7
|
vtoclg |
⊢ ( 𝐼 ∈ 𝐴 → ( ( 𝜑 ∧ 𝐼 ∈ 𝐴 ) → 𝐼 : 𝑇 ⟶ ℝ ) ) |
25 |
24
|
anabsi7 |
⊢ ( ( 𝜑 ∧ 𝐼 ∈ 𝐴 ) → 𝐼 : 𝑇 ⟶ ℝ ) |
26 |
15 19 25
|
syl2anc2 |
⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → 𝐼 : 𝑇 ⟶ ℝ ) |
27 |
26 14
|
ffvelrnd |
⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → ( 𝐼 ‘ 𝑡 ) ∈ ℝ ) |
28 |
|
simpl3 |
⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → 𝐺 ∈ 𝐴 ) |
29 |
|
eleq1 |
⊢ ( 𝑓 = 𝐺 → ( 𝑓 ∈ 𝐴 ↔ 𝐺 ∈ 𝐴 ) ) |
30 |
29
|
anbi2d |
⊢ ( 𝑓 = 𝐺 → ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝐺 ∈ 𝐴 ) ) ) |
31 |
|
feq1 |
⊢ ( 𝑓 = 𝐺 → ( 𝑓 : 𝑇 ⟶ ℝ ↔ 𝐺 : 𝑇 ⟶ ℝ ) ) |
32 |
30 31
|
imbi12d |
⊢ ( 𝑓 = 𝐺 → ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ ) ↔ ( ( 𝜑 ∧ 𝐺 ∈ 𝐴 ) → 𝐺 : 𝑇 ⟶ ℝ ) ) ) |
33 |
32 7
|
vtoclg |
⊢ ( 𝐺 ∈ 𝐴 → ( ( 𝜑 ∧ 𝐺 ∈ 𝐴 ) → 𝐺 : 𝑇 ⟶ ℝ ) ) |
34 |
33
|
anabsi7 |
⊢ ( ( 𝜑 ∧ 𝐺 ∈ 𝐴 ) → 𝐺 : 𝑇 ⟶ ℝ ) |
35 |
34
|
3adant3 |
⊢ ( ( 𝜑 ∧ 𝐺 ∈ 𝐴 ∧ 𝑡 ∈ 𝑇 ) → 𝐺 : 𝑇 ⟶ ℝ ) |
36 |
|
simp3 |
⊢ ( ( 𝜑 ∧ 𝐺 ∈ 𝐴 ∧ 𝑡 ∈ 𝑇 ) → 𝑡 ∈ 𝑇 ) |
37 |
35 36
|
ffvelrnd |
⊢ ( ( 𝜑 ∧ 𝐺 ∈ 𝐴 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐺 ‘ 𝑡 ) ∈ ℝ ) |
38 |
15 28 14 37
|
syl3anc |
⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → ( 𝐺 ‘ 𝑡 ) ∈ ℝ ) |
39 |
27 38
|
remulcld |
⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝐼 ‘ 𝑡 ) · ( 𝐺 ‘ 𝑡 ) ) ∈ ℝ ) |
40 |
6
|
fvmpt2 |
⊢ ( ( 𝑡 ∈ 𝑇 ∧ ( ( 𝐼 ‘ 𝑡 ) · ( 𝐺 ‘ 𝑡 ) ) ∈ ℝ ) → ( 𝐿 ‘ 𝑡 ) = ( ( 𝐼 ‘ 𝑡 ) · ( 𝐺 ‘ 𝑡 ) ) ) |
41 |
14 39 40
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → ( 𝐿 ‘ 𝑡 ) = ( ( 𝐼 ‘ 𝑡 ) · ( 𝐺 ‘ 𝑡 ) ) ) |
42 |
5
|
fvmpt2 |
⊢ ( ( 𝑡 ∈ 𝑇 ∧ - 1 ∈ ℝ ) → ( 𝐼 ‘ 𝑡 ) = - 1 ) |
43 |
16 42
|
mpan2 |
⊢ ( 𝑡 ∈ 𝑇 → ( 𝐼 ‘ 𝑡 ) = - 1 ) |
44 |
43
|
adantl |
⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → ( 𝐼 ‘ 𝑡 ) = - 1 ) |
45 |
44
|
oveq1d |
⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝐼 ‘ 𝑡 ) · ( 𝐺 ‘ 𝑡 ) ) = ( - 1 · ( 𝐺 ‘ 𝑡 ) ) ) |
46 |
38
|
recnd |
⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → ( 𝐺 ‘ 𝑡 ) ∈ ℂ ) |
47 |
46
|
mulm1d |
⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → ( - 1 · ( 𝐺 ‘ 𝑡 ) ) = - ( 𝐺 ‘ 𝑡 ) ) |
48 |
41 45 47
|
3eqtrd |
⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → ( 𝐿 ‘ 𝑡 ) = - ( 𝐺 ‘ 𝑡 ) ) |
49 |
48
|
oveq2d |
⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝐹 ‘ 𝑡 ) + ( 𝐿 ‘ 𝑡 ) ) = ( ( 𝐹 ‘ 𝑡 ) + - ( 𝐺 ‘ 𝑡 ) ) ) |
50 |
|
simpl2 |
⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → 𝐹 ∈ 𝐴 ) |
51 |
|
eleq1 |
⊢ ( 𝑓 = 𝐹 → ( 𝑓 ∈ 𝐴 ↔ 𝐹 ∈ 𝐴 ) ) |
52 |
51
|
anbi2d |
⊢ ( 𝑓 = 𝐹 → ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝐹 ∈ 𝐴 ) ) ) |
53 |
|
feq1 |
⊢ ( 𝑓 = 𝐹 → ( 𝑓 : 𝑇 ⟶ ℝ ↔ 𝐹 : 𝑇 ⟶ ℝ ) ) |
54 |
52 53
|
imbi12d |
⊢ ( 𝑓 = 𝐹 → ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ ) ↔ ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ) → 𝐹 : 𝑇 ⟶ ℝ ) ) ) |
55 |
54 7
|
vtoclg |
⊢ ( 𝐹 ∈ 𝐴 → ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ) → 𝐹 : 𝑇 ⟶ ℝ ) ) |
56 |
55
|
anabsi7 |
⊢ ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ) → 𝐹 : 𝑇 ⟶ ℝ ) |
57 |
15 50 56
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → 𝐹 : 𝑇 ⟶ ℝ ) |
58 |
57 14
|
ffvelrnd |
⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑡 ) ∈ ℝ ) |
59 |
58
|
recnd |
⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑡 ) ∈ ℂ ) |
60 |
59 46
|
negsubd |
⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝐹 ‘ 𝑡 ) + - ( 𝐺 ‘ 𝑡 ) ) = ( ( 𝐹 ‘ 𝑡 ) − ( 𝐺 ‘ 𝑡 ) ) ) |
61 |
49 60
|
eqtr2d |
⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝐹 ‘ 𝑡 ) − ( 𝐺 ‘ 𝑡 ) ) = ( ( 𝐹 ‘ 𝑡 ) + ( 𝐿 ‘ 𝑡 ) ) ) |
62 |
13 61
|
mpteq2da |
⊢ ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐺 ‘ 𝑡 ) ) ) = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) + ( 𝐿 ‘ 𝑡 ) ) ) ) |
63 |
19
|
3ad2ant1 |
⊢ ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) → 𝐼 ∈ 𝐴 ) |
64 |
|
nfmpt1 |
⊢ Ⅎ 𝑡 ( 𝑡 ∈ 𝑇 ↦ - 1 ) |
65 |
5 64
|
nfcxfr |
⊢ Ⅎ 𝑡 𝐼 |
66 |
65
|
nfeq2 |
⊢ Ⅎ 𝑡 𝑓 = 𝐼 |
67 |
3
|
nfeq2 |
⊢ Ⅎ 𝑡 𝑔 = 𝐺 |
68 |
66 67 9
|
stoweidlem6 |
⊢ ( ( 𝜑 ∧ 𝐼 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐼 ‘ 𝑡 ) · ( 𝐺 ‘ 𝑡 ) ) ) ∈ 𝐴 ) |
69 |
63 68
|
syld3an2 |
⊢ ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐼 ‘ 𝑡 ) · ( 𝐺 ‘ 𝑡 ) ) ) ∈ 𝐴 ) |
70 |
6 69
|
eqeltrid |
⊢ ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) → 𝐿 ∈ 𝐴 ) |
71 |
|
nfmpt1 |
⊢ Ⅎ 𝑡 ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐼 ‘ 𝑡 ) · ( 𝐺 ‘ 𝑡 ) ) ) |
72 |
6 71
|
nfcxfr |
⊢ Ⅎ 𝑡 𝐿 |
73 |
8 2 72
|
stoweidlem8 |
⊢ ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐿 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) + ( 𝐿 ‘ 𝑡 ) ) ) ∈ 𝐴 ) |
74 |
70 73
|
syld3an3 |
⊢ ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) + ( 𝐿 ‘ 𝑡 ) ) ) ∈ 𝐴 ) |
75 |
62 74
|
eqeltrd |
⊢ ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐺 ‘ 𝑡 ) ) ) ∈ 𝐴 ) |