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 )