Metamath Proof Explorer


Theorem stoweidlem47

Description: Subtracting a constant from a real continuous function gives another continuous function. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem47.1 𝑡 𝐹
stoweidlem47.2 𝑡 𝑆
stoweidlem47.3 𝑡 𝜑
stoweidlem47.4 𝑇 = 𝐽
stoweidlem47.5 𝐺 = ( 𝑇 × { - 𝑆 } )
stoweidlem47.6 𝐾 = ( topGen ‘ ran (,) )
stoweidlem47.7 ( 𝜑𝐽 ∈ Top )
stoweidlem47.8 𝐶 = ( 𝐽 Cn 𝐾 )
stoweidlem47.9 ( 𝜑𝐹𝐶 )
stoweidlem47.10 ( 𝜑𝑆 ∈ ℝ )
Assertion stoweidlem47 ( 𝜑 → ( 𝑡𝑇 ↦ ( ( 𝐹𝑡 ) − 𝑆 ) ) ∈ 𝐶 )

Proof

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 ( 𝜑 → ( 𝑡𝑇 ↦ ( ( 𝐹𝑡 ) − 𝑆 ) ) ∈ 𝐶 )