Metamath Proof Explorer

Theorem dvfre

Description: The derivative of a real function is real. (Contributed by Mario Carneiro, 1-Sep-2014)

Ref Expression
Assertion dvfre 
|- ( ( F : A --> RR /\ A C_ RR ) -> ( RR _D F ) : dom ( RR _D F ) --> RR )

Proof

Step Hyp Ref Expression
1 dvf 
 |-  ( RR _D F ) : dom ( RR _D F ) --> CC
2 ffn 
 |-  ( ( RR _D F ) : dom ( RR _D F ) --> CC -> ( RR _D F ) Fn dom ( RR _D F ) )
3 1 2 mp1i 
 |-  ( ( F : A --> RR /\ A C_ RR ) -> ( RR _D F ) Fn dom ( RR _D F ) )
4 1 ffvelrni 
 |-  ( x e. dom ( RR _D F ) -> ( ( RR _D F ) ` x ) e. CC )
5 4 adantl 
 |-  ( ( ( F : A --> RR /\ A C_ RR ) /\ x e. dom ( RR _D F ) ) -> ( ( RR _D F ) ` x ) e. CC )
6 simpr 
 |-  ( ( ( F : A --> RR /\ A C_ RR ) /\ x e. dom ( RR _D F ) ) -> x e. dom ( RR _D F ) )
7 fvco3 
 |-  ( ( ( RR _D F ) : dom ( RR _D F ) --> CC /\ x e. dom ( RR _D F ) ) -> ( ( * o. ( RR _D F ) ) ` x ) = ( * ` ( ( RR _D F ) ` x ) ) )
8 1 6 7 sylancr 
 |-  ( ( ( F : A --> RR /\ A C_ RR ) /\ x e. dom ( RR _D F ) ) -> ( ( * o. ( RR _D F ) ) ` x ) = ( * ` ( ( RR _D F ) ` x ) ) )
9 ax-resscn 
 |-  RR C_ CC
10 fss 
 |-  ( ( F : A --> RR /\ RR C_ CC ) -> F : A --> CC )
11 9 10 mpan2 
 |-  ( F : A --> RR -> F : A --> CC )
12 dvcj 
 |-  ( ( F : A --> CC /\ A C_ RR ) -> ( RR _D ( * o. F ) ) = ( * o. ( RR _D F ) ) )
13 11 12 sylan 
 |-  ( ( F : A --> RR /\ A C_ RR ) -> ( RR _D ( * o. F ) ) = ( * o. ( RR _D F ) ) )
14 ffvelrn 
 |-  ( ( F : A --> RR /\ y e. A ) -> ( F ` y ) e. RR )
15 14 adantlr 
 |-  ( ( ( F : A --> RR /\ A C_ RR ) /\ y e. A ) -> ( F ` y ) e. RR )
16 15 cjred 
 |-  ( ( ( F : A --> RR /\ A C_ RR ) /\ y e. A ) -> ( * ` ( F ` y ) ) = ( F ` y ) )
17 16 mpteq2dva 
 |-  ( ( F : A --> RR /\ A C_ RR ) -> ( y e. A |-> ( * ` ( F ` y ) ) ) = ( y e. A |-> ( F ` y ) ) )
18 15 recnd 
 |-  ( ( ( F : A --> RR /\ A C_ RR ) /\ y e. A ) -> ( F ` y ) e. CC )
19 simpl 
 |-  ( ( F : A --> RR /\ A C_ RR ) -> F : A --> RR )
20 19 feqmptd 
 |-  ( ( F : A --> RR /\ A C_ RR ) -> F = ( y e. A |-> ( F ` y ) ) )
21 cjf 
 |-  * : CC --> CC
22 21 a1i 
 |-  ( ( F : A --> RR /\ A C_ RR ) -> * : CC --> CC )
23 22 feqmptd 
 |-  ( ( F : A --> RR /\ A C_ RR ) -> * = ( z e. CC |-> ( * ` z ) ) )
24 fveq2 
 |-  ( z = ( F ` y ) -> ( * ` z ) = ( * ` ( F ` y ) ) )
25 18 20 23 24 fmptco 
 |-  ( ( F : A --> RR /\ A C_ RR ) -> ( * o. F ) = ( y e. A |-> ( * ` ( F ` y ) ) ) )
26 17 25 20 3eqtr4d 
 |-  ( ( F : A --> RR /\ A C_ RR ) -> ( * o. F ) = F )
27 26 oveq2d 
 |-  ( ( F : A --> RR /\ A C_ RR ) -> ( RR _D ( * o. F ) ) = ( RR _D F ) )
28 13 27 eqtr3d 
 |-  ( ( F : A --> RR /\ A C_ RR ) -> ( * o. ( RR _D F ) ) = ( RR _D F ) )
29 28 fveq1d 
 |-  ( ( F : A --> RR /\ A C_ RR ) -> ( ( * o. ( RR _D F ) ) ` x ) = ( ( RR _D F ) ` x ) )
30 29 adantr 
 |-  ( ( ( F : A --> RR /\ A C_ RR ) /\ x e. dom ( RR _D F ) ) -> ( ( * o. ( RR _D F ) ) ` x ) = ( ( RR _D F ) ` x ) )
31 8 30 eqtr3d 
 |-  ( ( ( F : A --> RR /\ A C_ RR ) /\ x e. dom ( RR _D F ) ) -> ( * ` ( ( RR _D F ) ` x ) ) = ( ( RR _D F ) ` x ) )
32 5 31 cjrebd 
 |-  ( ( ( F : A --> RR /\ A C_ RR ) /\ x e. dom ( RR _D F ) ) -> ( ( RR _D F ) ` x ) e. RR )
33 32 ralrimiva 
 |-  ( ( F : A --> RR /\ A C_ RR ) -> A. x e. dom ( RR _D F ) ( ( RR _D F ) ` x ) e. RR )
34 ffnfv 
 |-  ( ( RR _D F ) : dom ( RR _D F ) --> RR <-> ( ( RR _D F ) Fn dom ( RR _D F ) /\ A. x e. dom ( RR _D F ) ( ( RR _D F ) ` x ) e. RR ) )
35 3 33 34 sylanbrc 
 |-  ( ( F : A --> RR /\ A C_ RR ) -> ( RR _D F ) : dom ( RR _D F ) --> RR )