Metamath Proof Explorer

Theorem ftc1cn

Description: Strengthen the assumptions of ftc1 to when the function F is continuous on the entire interval ( A , B ) ; in this case we can calculate _D G exactly. (Contributed by Mario Carneiro, 1-Sep-2014)

Ref Expression
Hypotheses ftc1cn.g 
|- G = ( x e. ( A [,] B ) |-> S. ( A (,) x ) ( F ` t ) _d t )
ftc1cn.a 
|- ( ph -> A e. RR )
ftc1cn.b 
|- ( ph -> B e. RR )
ftc1cn.le 
|- ( ph -> A <_ B )
ftc1cn.f 
|- ( ph -> F e. ( ( A (,) B ) -cn-> CC ) )
ftc1cn.i 
|- ( ph -> F e. L^1 )
Assertion ftc1cn 
|- ( ph -> ( RR _D G ) = F )

Proof

Step Hyp Ref Expression
1 ftc1cn.g 
 |-  G = ( x e. ( A [,] B ) |-> S. ( A (,) x ) ( F ` t ) _d t )
2 ftc1cn.a 
 |-  ( ph -> A e. RR )
3 ftc1cn.b 
 |-  ( ph -> B e. RR )
4 ftc1cn.le 
 |-  ( ph -> A <_ B )
5 ftc1cn.f 
 |-  ( ph -> F e. ( ( A (,) B ) -cn-> CC ) )
6 ftc1cn.i 
 |-  ( ph -> F e. L^1 )
7 dvf 
 |-  ( RR _D G ) : dom ( RR _D G ) --> CC
8 7 a1i 
 |-  ( ph -> ( RR _D G ) : dom ( RR _D G ) --> CC )
9 8 ffund 
 |-  ( ph -> Fun ( RR _D G ) )
10 ax-resscn 
 |-  RR C_ CC
11 10 a1i 
 |-  ( ph -> RR C_ CC )
12 ssidd 
 |-  ( ph -> ( A (,) B ) C_ ( A (,) B ) )
13 ioossre 
 |-  ( A (,) B ) C_ RR
14 13 a1i 
 |-  ( ph -> ( A (,) B ) C_ RR )
15 cncff 
 |-  ( F e. ( ( A (,) B ) -cn-> CC ) -> F : ( A (,) B ) --> CC )
16 5 15 syl 
 |-  ( ph -> F : ( A (,) B ) --> CC )
17 1 2 3 4 12 14 6 16 ftc1lem2 
 |-  ( ph -> G : ( A [,] B ) --> CC )
18 iccssre 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
19 2 3 18 syl2anc 
 |-  ( ph -> ( A [,] B ) C_ RR )
20 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
21 20 tgioo2 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
22 11 17 19 21 20 dvbssntr 
 |-  ( ph -> dom ( RR _D G ) C_ ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) )
23 iccntr 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) = ( A (,) B ) )
24 2 3 23 syl2anc 
 |-  ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) = ( A (,) B ) )
25 22 24 sseqtrd 
 |-  ( ph -> dom ( RR _D G ) C_ ( A (,) B ) )
26 2 adantr 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> A e. RR )
27 3 adantr 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> B e. RR )
28 4 adantr 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> A <_ B )
29 ssidd 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( A (,) B ) C_ ( A (,) B ) )
30 13 a1i 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( A (,) B ) C_ RR )
31 6 adantr 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> F e. L^1 )
32 simpr 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> y e. ( A (,) B ) )
33 13 10 sstri 
 |-  ( A (,) B ) C_ CC
34 ssid 
 |-  CC C_ CC
35 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) = ( ( TopOpen ` CCfld ) |`t ( A (,) B ) )
36 20 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
37 36 toponrestid 
 |-  ( TopOpen ` CCfld ) = ( ( TopOpen ` CCfld ) |`t CC )
38 20 35 37 cncfcn 
 |-  ( ( ( A (,) B ) C_ CC /\ CC C_ CC ) -> ( ( A (,) B ) -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) Cn ( TopOpen ` CCfld ) ) )
39 33 34 38 mp2an 
 |-  ( ( A (,) B ) -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) Cn ( TopOpen ` CCfld ) )
40 5 39 eleqtrdi 
 |-  ( ph -> F e. ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) Cn ( TopOpen ` CCfld ) ) )
41 40 adantr 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> F e. ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) Cn ( TopOpen ` CCfld ) ) )
42 33 a1i 
 |-  ( ph -> ( A (,) B ) C_ CC )
43 resttopon 
 |-  ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ ( A (,) B ) C_ CC ) -> ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) e. ( TopOn ` ( A (,) B ) ) )
44 36 42 43 sylancr 
 |-  ( ph -> ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) e. ( TopOn ` ( A (,) B ) ) )
45 toponuni 
 |-  ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) e. ( TopOn ` ( A (,) B ) ) -> ( A (,) B ) = U. ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) )
46 44 45 syl 
 |-  ( ph -> ( A (,) B ) = U. ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) )
47 46 eleq2d 
 |-  ( ph -> ( y e. ( A (,) B ) <-> y e. U. ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) ) )
48 47 biimpa 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> y e. U. ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) )
49 eqid 
 |-  U. ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) = U. ( ( TopOpen ` CCfld ) |`t ( A (,) B ) )
50 49 cncnpi 
 |-  ( ( F e. ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) Cn ( TopOpen ` CCfld ) ) /\ y e. U. ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) ) -> F e. ( ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) ` y ) )
51 41 48 50 syl2anc 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> F e. ( ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) ` y ) )
52 1 26 27 28 29 30 31 32 51 21 35 20 ftc1 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> y ( RR _D G ) ( F ` y ) )
53 vex 
 |-  y e. _V
54 fvex 
 |-  ( F ` y ) e. _V
55 53 54 breldm 
 |-  ( y ( RR _D G ) ( F ` y ) -> y e. dom ( RR _D G ) )
56 52 55 syl 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> y e. dom ( RR _D G ) )
57 25 56 eqelssd 
 |-  ( ph -> dom ( RR _D G ) = ( A (,) B ) )
58 df-fn 
 |-  ( ( RR _D G ) Fn ( A (,) B ) <-> ( Fun ( RR _D G ) /\ dom ( RR _D G ) = ( A (,) B ) ) )
59 9 57 58 sylanbrc 
 |-  ( ph -> ( RR _D G ) Fn ( A (,) B ) )
60 16 ffnd 
 |-  ( ph -> F Fn ( A (,) B ) )
61 9 adantr 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> Fun ( RR _D G ) )
62 funbrfv 
 |-  ( Fun ( RR _D G ) -> ( y ( RR _D G ) ( F ` y ) -> ( ( RR _D G ) ` y ) = ( F ` y ) ) )
63 61 52 62 sylc 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( ( RR _D G ) ` y ) = ( F ` y ) )
64 59 60 63 eqfnfvd 
 |-  ( ph -> ( RR _D G ) = F )