Metamath Proof Explorer

Theorem dvmptrecl

Description: Real closure of a derivative. (Contributed by Mario Carneiro, 18-May-2016)

Ref Expression
Hypotheses dvmptrecl.s 
|- ( ph -> S C_ RR )
dvmptrecl.a 
|- ( ( ph /\ x e. S ) -> A e. RR )
dvmptrecl.v 
|- ( ( ph /\ x e. S ) -> B e. V )
dvmptrecl.b 
|- ( ph -> ( RR _D ( x e. S |-> A ) ) = ( x e. S |-> B ) )
Assertion dvmptrecl 
|- ( ( ph /\ x e. S ) -> B e. RR )

Proof

Step Hyp Ref Expression
1 dvmptrecl.s 
 |-  ( ph -> S C_ RR )
2 dvmptrecl.a 
 |-  ( ( ph /\ x e. S ) -> A e. RR )
3 dvmptrecl.v 
 |-  ( ( ph /\ x e. S ) -> B e. V )
4 dvmptrecl.b 
 |-  ( ph -> ( RR _D ( x e. S |-> A ) ) = ( x e. S |-> B ) )
5 2 fmpttd 
 |-  ( ph -> ( x e. S |-> A ) : S --> RR )
6 dvfre 
 |-  ( ( ( x e. S |-> A ) : S --> RR /\ S C_ RR ) -> ( RR _D ( x e. S |-> A ) ) : dom ( RR _D ( x e. S |-> A ) ) --> RR )
7 5 1 6 syl2anc 
 |-  ( ph -> ( RR _D ( x e. S |-> A ) ) : dom ( RR _D ( x e. S |-> A ) ) --> RR )
8 4 dmeqd 
 |-  ( ph -> dom ( RR _D ( x e. S |-> A ) ) = dom ( x e. S |-> B ) )
9 3 ralrimiva 
 |-  ( ph -> A. x e. S B e. V )
10 dmmptg 
 |-  ( A. x e. S B e. V -> dom ( x e. S |-> B ) = S )
11 9 10 syl 
 |-  ( ph -> dom ( x e. S |-> B ) = S )
12 8 11 eqtrd 
 |-  ( ph -> dom ( RR _D ( x e. S |-> A ) ) = S )
13 4 12 feq12d 
 |-  ( ph -> ( ( RR _D ( x e. S |-> A ) ) : dom ( RR _D ( x e. S |-> A ) ) --> RR <-> ( x e. S |-> B ) : S --> RR ) )
14 7 13 mpbid 
 |-  ( ph -> ( x e. S |-> B ) : S --> RR )
15 14 fvmptelrn 
 |-  ( ( ph /\ x e. S ) -> B e. RR )