Metamath Proof Explorer

Theorem dvresioo

Description: Restriction of a derivative to an open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion dvresioo 
|- ( ( A C_ RR /\ F : A --> CC ) -> ( RR _D ( F |` ( B (,) C ) ) ) = ( ( RR _D F ) |` ( B (,) C ) ) )

Proof

Step Hyp Ref Expression
1 ax-resscn 
 |-  RR C_ CC
2 1 a1i 
 |-  ( ( A C_ RR /\ F : A --> CC ) -> RR C_ CC )
3 simpr 
 |-  ( ( A C_ RR /\ F : A --> CC ) -> F : A --> CC )
4 simpl 
 |-  ( ( A C_ RR /\ F : A --> CC ) -> A C_ RR )
5 ioossre 
 |-  ( B (,) C ) C_ RR
6 5 a1i 
 |-  ( ( A C_ RR /\ F : A --> CC ) -> ( B (,) C ) C_ RR )
7 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
8 7 tgioo2 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
9 7 8 dvres 
 |-  ( ( ( RR C_ CC /\ F : A --> CC ) /\ ( A C_ RR /\ ( B (,) C ) C_ RR ) ) -> ( RR _D ( F |` ( B (,) C ) ) ) = ( ( RR _D F ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( B (,) C ) ) ) )
10 2 3 4 6 9 syl22anc 
 |-  ( ( A C_ RR /\ F : A --> CC ) -> ( RR _D ( F |` ( B (,) C ) ) ) = ( ( RR _D F ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( B (,) C ) ) ) )
11 ioontr 
 |-  ( ( int ` ( topGen ` ran (,) ) ) ` ( B (,) C ) ) = ( B (,) C )
12 11 reseq2i 
 |-  ( ( RR _D F ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( B (,) C ) ) ) = ( ( RR _D F ) |` ( B (,) C ) )
13 10 12 eqtrdi 
 |-  ( ( A C_ RR /\ F : A --> CC ) -> ( RR _D ( F |` ( B (,) C ) ) ) = ( ( RR _D F ) |` ( B (,) C ) ) )