Step |
Hyp |
Ref |
Expression |
1 |
|
stoweidlem47.1 |
⊢ Ⅎ 𝑡 𝐹 |
2 |
|
stoweidlem47.2 |
⊢ Ⅎ 𝑡 𝑆 |
3 |
|
stoweidlem47.3 |
⊢ Ⅎ 𝑡 𝜑 |
4 |
|
stoweidlem47.4 |
⊢ 𝑇 = ∪ 𝐽 |
5 |
|
stoweidlem47.5 |
⊢ 𝐺 = ( 𝑇 × { - 𝑆 } ) |
6 |
|
stoweidlem47.6 |
⊢ 𝐾 = ( topGen ‘ ran (,) ) |
7 |
|
stoweidlem47.7 |
⊢ ( 𝜑 → 𝐽 ∈ Top ) |
8 |
|
stoweidlem47.8 |
⊢ 𝐶 = ( 𝐽 Cn 𝐾 ) |
9 |
|
stoweidlem47.9 |
⊢ ( 𝜑 → 𝐹 ∈ 𝐶 ) |
10 |
|
stoweidlem47.10 |
⊢ ( 𝜑 → 𝑆 ∈ ℝ ) |
11 |
5
|
fveq1i |
⊢ ( 𝐺 ‘ 𝑡 ) = ( ( 𝑇 × { - 𝑆 } ) ‘ 𝑡 ) |
12 |
10
|
renegcld |
⊢ ( 𝜑 → - 𝑆 ∈ ℝ ) |
13 |
|
fvconst2g |
⊢ ( ( - 𝑆 ∈ ℝ ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝑇 × { - 𝑆 } ) ‘ 𝑡 ) = - 𝑆 ) |
14 |
12 13
|
sylan |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝑇 × { - 𝑆 } ) ‘ 𝑡 ) = - 𝑆 ) |
15 |
11 14
|
syl5eq |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐺 ‘ 𝑡 ) = - 𝑆 ) |
16 |
15
|
oveq2d |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝐹 ‘ 𝑡 ) + ( 𝐺 ‘ 𝑡 ) ) = ( ( 𝐹 ‘ 𝑡 ) + - 𝑆 ) ) |
17 |
6 4 8 9
|
fcnre |
⊢ ( 𝜑 → 𝐹 : 𝑇 ⟶ ℝ ) |
18 |
17
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑡 ) ∈ ℝ ) |
19 |
18
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑡 ) ∈ ℂ ) |
20 |
10
|
recnd |
⊢ ( 𝜑 → 𝑆 ∈ ℂ ) |
21 |
20
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 𝑆 ∈ ℂ ) |
22 |
19 21
|
negsubd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝐹 ‘ 𝑡 ) + - 𝑆 ) = ( ( 𝐹 ‘ 𝑡 ) − 𝑆 ) ) |
23 |
16 22
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝐹 ‘ 𝑡 ) + ( 𝐺 ‘ 𝑡 ) ) = ( ( 𝐹 ‘ 𝑡 ) − 𝑆 ) ) |
24 |
3 23
|
mpteq2da |
⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) + ( 𝐺 ‘ 𝑡 ) ) ) = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) − 𝑆 ) ) ) |
25 |
|
nfcv |
⊢ Ⅎ 𝑡 𝑇 |
26 |
2
|
nfneg |
⊢ Ⅎ 𝑡 - 𝑆 |
27 |
26
|
nfsn |
⊢ Ⅎ 𝑡 { - 𝑆 } |
28 |
25 27
|
nfxp |
⊢ Ⅎ 𝑡 ( 𝑇 × { - 𝑆 } ) |
29 |
5 28
|
nfcxfr |
⊢ Ⅎ 𝑡 𝐺 |
30 |
4
|
a1i |
⊢ ( 𝜑 → 𝑇 = ∪ 𝐽 ) |
31 |
|
istopon |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑇 ) ↔ ( 𝐽 ∈ Top ∧ 𝑇 = ∪ 𝐽 ) ) |
32 |
7 30 31
|
sylanbrc |
⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑇 ) ) |
33 |
9 8
|
eleqtrdi |
⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) |
34 |
|
retopon |
⊢ ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ ) |
35 |
6 34
|
eqeltri |
⊢ 𝐾 ∈ ( TopOn ‘ ℝ ) |
36 |
35
|
a1i |
⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ ℝ ) ) |
37 |
|
cnconst2 |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑇 ) ∧ 𝐾 ∈ ( TopOn ‘ ℝ ) ∧ - 𝑆 ∈ ℝ ) → ( 𝑇 × { - 𝑆 } ) ∈ ( 𝐽 Cn 𝐾 ) ) |
38 |
32 36 12 37
|
syl3anc |
⊢ ( 𝜑 → ( 𝑇 × { - 𝑆 } ) ∈ ( 𝐽 Cn 𝐾 ) ) |
39 |
5 38
|
eqeltrid |
⊢ ( 𝜑 → 𝐺 ∈ ( 𝐽 Cn 𝐾 ) ) |
40 |
1 29 3 6 32 33 39
|
refsum2cn |
⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) + ( 𝐺 ‘ 𝑡 ) ) ) ∈ ( 𝐽 Cn 𝐾 ) ) |
41 |
40 8
|
eleqtrrdi |
⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) + ( 𝐺 ‘ 𝑡 ) ) ) ∈ 𝐶 ) |
42 |
24 41
|
eqeltrrd |
⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) − 𝑆 ) ) ∈ 𝐶 ) |