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 
|- F/_ t F
stoweidlem47.2 
|- F/_ t S
stoweidlem47.3 
|- F/ t ph
stoweidlem47.4 
|- T = U. J
stoweidlem47.5 
|- G = ( T X. { -u S } )
stoweidlem47.6 
|- K = ( topGen ` ran (,) )
stoweidlem47.7 
|- ( ph -> J e. Top )
stoweidlem47.8 
|- C = ( J Cn K )
stoweidlem47.9 
|- ( ph -> F e. C )
stoweidlem47.10 
|- ( ph -> S e. RR )
Assertion stoweidlem47 
|- ( ph -> ( t e. T |-> ( ( F ` t ) - S ) ) e. C )

Proof

Step Hyp Ref Expression
1 stoweidlem47.1 
 |-  F/_ t F
2 stoweidlem47.2 
 |-  F/_ t S
3 stoweidlem47.3 
 |-  F/ t ph
4 stoweidlem47.4 
 |-  T = U. J
5 stoweidlem47.5 
 |-  G = ( T X. { -u S } )
6 stoweidlem47.6 
 |-  K = ( topGen ` ran (,) )
7 stoweidlem47.7 
 |-  ( ph -> J e. Top )
8 stoweidlem47.8 
 |-  C = ( J Cn K )
9 stoweidlem47.9 
 |-  ( ph -> F e. C )
10 stoweidlem47.10 
 |-  ( ph -> S e. RR )
11 5 fveq1i 
 |-  ( G ` t ) = ( ( T X. { -u S } ) ` t )
12 10 renegcld 
 |-  ( ph -> -u S e. RR )
13 fvconst2g 
 |-  ( ( -u S e. RR /\ t e. T ) -> ( ( T X. { -u S } ) ` t ) = -u S )
14 12 13 sylan 
 |-  ( ( ph /\ t e. T ) -> ( ( T X. { -u S } ) ` t ) = -u S )
15 11 14 syl5eq 
 |-  ( ( ph /\ t e. T ) -> ( G ` t ) = -u S )
16 15 oveq2d 
 |-  ( ( ph /\ t e. T ) -> ( ( F ` t ) + ( G ` t ) ) = ( ( F ` t ) + -u S ) )
17 6 4 8 9 fcnre 
 |-  ( ph -> F : T --> RR )
18 17 ffvelrnda 
 |-  ( ( ph /\ t e. T ) -> ( F ` t ) e. RR )
19 18 recnd 
 |-  ( ( ph /\ t e. T ) -> ( F ` t ) e. CC )
20 10 recnd 
 |-  ( ph -> S e. CC )
21 20 adantr 
 |-  ( ( ph /\ t e. T ) -> S e. CC )
22 19 21 negsubd 
 |-  ( ( ph /\ t e. T ) -> ( ( F ` t ) + -u S ) = ( ( F ` t ) - S ) )
23 16 22 eqtrd 
 |-  ( ( ph /\ t e. T ) -> ( ( F ` t ) + ( G ` t ) ) = ( ( F ` t ) - S ) )
24 3 23 mpteq2da 
 |-  ( ph -> ( t e. T |-> ( ( F ` t ) + ( G ` t ) ) ) = ( t e. T |-> ( ( F ` t ) - S ) ) )
25 nfcv 
 |-  F/_ t T
26 2 nfneg 
 |-  F/_ t -u S
27 26 nfsn 
 |-  F/_ t { -u S }
28 25 27 nfxp 
 |-  F/_ t ( T X. { -u S } )
29 5 28 nfcxfr 
 |-  F/_ t G
30 4 a1i 
 |-  ( ph -> T = U. J )
31 istopon 
 |-  ( J e. ( TopOn ` T ) <-> ( J e. Top /\ T = U. J ) )
32 7 30 31 sylanbrc 
 |-  ( ph -> J e. ( TopOn ` T ) )
33 9 8 eleqtrdi 
 |-  ( ph -> F e. ( J Cn K ) )
34 retopon 
 |-  ( topGen ` ran (,) ) e. ( TopOn ` RR )
35 6 34 eqeltri 
 |-  K e. ( TopOn ` RR )
36 35 a1i 
 |-  ( ph -> K e. ( TopOn ` RR ) )
37 cnconst2 
 |-  ( ( J e. ( TopOn ` T ) /\ K e. ( TopOn ` RR ) /\ -u S e. RR ) -> ( T X. { -u S } ) e. ( J Cn K ) )
38 32 36 12 37 syl3anc 
 |-  ( ph -> ( T X. { -u S } ) e. ( J Cn K ) )
39 5 38 eqeltrid 
 |-  ( ph -> G e. ( J Cn K ) )
40 1 29 3 6 32 33 39 refsum2cn 
 |-  ( ph -> ( t e. T |-> ( ( F ` t ) + ( G ` t ) ) ) e. ( J Cn K ) )
41 40 8 eleqtrrdi 
 |-  ( ph -> ( t e. T |-> ( ( F ` t ) + ( G ` t ) ) ) e. C )
42 24 41 eqeltrrd 
 |-  ( ph -> ( t e. T |-> ( ( F ` t ) - S ) ) e. C )