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	$$⊢\underset{\_}{Ⅎ}tF$$
	stoweidlem47.2	$$⊢\underset{\_}{Ⅎ}tS$$
	stoweidlem47.3	$$⊢Ⅎt\phi$$
	stoweidlem47.4	$$⊢T=\bigcup J$$
	stoweidlem47.5	$$⊢G=T\times \left\{-S\right\}$$
	stoweidlem47.6	$$⊢K=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
	stoweidlem47.7	$$⊢\phi \to J\in \mathrm{Top}$$
	stoweidlem47.8	$$⊢C=J\mathrm{Cn}K$$
	stoweidlem47.9	$$⊢\phi \to F\in C$$
	stoweidlem47.10	$$⊢\phi \to S\in ℝ$$
Assertion	stoweidlem47	$$⊢\phi \to \left(t\in T⟼F\left(t\right)-S\right)\in C$$

Proof

Step	Hyp	Ref	Expression
1		stoweidlem47.1	$$⊢\underset{\_}{Ⅎ}tF$$
2		stoweidlem47.2	$$⊢\underset{\_}{Ⅎ}tS$$
3		stoweidlem47.3	$$⊢Ⅎt\phi$$
4		stoweidlem47.4	$$⊢T=\bigcup J$$
5		stoweidlem47.5	$$⊢G=T\times \left\{-S\right\}$$
6		stoweidlem47.6	$$⊢K=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
7		stoweidlem47.7	$$⊢\phi \to J\in \mathrm{Top}$$
8		stoweidlem47.8	$$⊢C=J\mathrm{Cn}K$$
9		stoweidlem47.9	$$⊢\phi \to F\in C$$
10		stoweidlem47.10	$$⊢\phi \to S\in ℝ$$
11	5	fveq1i	$$⊢G\left(t\right)=\left(T\times \left\{-S\right\}\right)\left(t\right)$$
12	10	renegcld	$$⊢\phi \to -S\in ℝ$$
13		fvconst2g	$$⊢\left(-S\in ℝ\wedge t\in T\right)\to \left(T\times \left\{-S\right\}\right)\left(t\right)=-S$$
14	12 13	sylan	$$⊢\left(\phi \wedge t\in T\right)\to \left(T\times \left\{-S\right\}\right)\left(t\right)=-S$$
15	11 14	eqtrid	$$⊢\left(\phi \wedge t\in T\right)\to G\left(t\right)=-S$$
16	15	oveq2d	$$⊢\left(\phi \wedge t\in T\right)\to F\left(t\right)+G\left(t\right)=F\left(t\right)+\left(-S\right)$$
17	6 4 8 9	fcnre	$$⊢\phi \to F:T⟶ℝ$$
18	17	ffvelcdmda	$$⊢\left(\phi \wedge t\in T\right)\to F\left(t\right)\in ℝ$$
19	18	recnd	$$⊢\left(\phi \wedge t\in T\right)\to F\left(t\right)\in ℂ$$
20	10	recnd	$$⊢\phi \to S\in ℂ$$
21	20	adantr	$$⊢\left(\phi \wedge t\in T\right)\to S\in ℂ$$
22	19 21	negsubd	$$⊢\left(\phi \wedge t\in T\right)\to F\left(t\right)+\left(-S\right)=F\left(t\right)-S$$
23	16 22	eqtrd	$$⊢\left(\phi \wedge t\in T\right)\to F\left(t\right)+G\left(t\right)=F\left(t\right)-S$$
24	3 23	mpteq2da	$$⊢\phi \to \left(t\in T⟼F\left(t\right)+G\left(t\right)\right)=\left(t\in T⟼F\left(t\right)-S\right)$$
25		nfcv	$$⊢\underset{\_}{Ⅎ}tT$$
26	2	nfneg	$$⊢\underset{\_}{Ⅎ}t\left(-S\right)$$
27	26	nfsn	$$⊢\underset{\_}{Ⅎ}t\left\{-S\right\}$$
28	25 27	nfxp	$$⊢\underset{\_}{Ⅎ}t\left(T\times \left\{-S\right\}\right)$$
29	5 28	nfcxfr	$$⊢\underset{\_}{Ⅎ}tG$$
30	4	a1i	$$⊢\phi \to T=\bigcup J$$
31		istopon	$$⊢J\in \mathrm{TopOn}\left(T\right)\leftrightarrow \left(J\in \mathrm{Top}\wedge T=\bigcup J\right)$$
32	7 30 31	sylanbrc	$$⊢\phi \to J\in \mathrm{TopOn}\left(T\right)$$
33	9 8	eleqtrdi	$$⊢\phi \to F\in \left(J\mathrm{Cn}K\right)$$
34		retopon	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{TopOn}\left(ℝ\right)$$
35	6 34	eqeltri	$$⊢K\in \mathrm{TopOn}\left(ℝ\right)$$
36	35	a1i	$$⊢\phi \to K\in \mathrm{TopOn}\left(ℝ\right)$$
37		cnconst2	$$⊢\left(J\in \mathrm{TopOn}\left(T\right)\wedge K\in \mathrm{TopOn}\left(ℝ\right)\wedge -S\in ℝ\right)\to T\times \left\{-S\right\}\in \left(J\mathrm{Cn}K\right)$$
38	32 36 12 37	syl3anc	$$⊢\phi \to T\times \left\{-S\right\}\in \left(J\mathrm{Cn}K\right)$$
39	5 38	eqeltrid	$$⊢\phi \to G\in \left(J\mathrm{Cn}K\right)$$
40	1 29 3 6 32 33 39	refsum2cn	$$⊢\phi \to \left(t\in T⟼F\left(t\right)+G\left(t\right)\right)\in \left(J\mathrm{Cn}K\right)$$
41	40 8	eleqtrrdi	$$⊢\phi \to \left(t\in T⟼F\left(t\right)+G\left(t\right)\right)\in C$$
42	24 41	eqeltrrd	$$⊢\phi \to \left(t\in T⟼F\left(t\right)-S\right)\in C$$