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 ) |