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