This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dvmptcl

Description: Closure lemma for dvmptcmul and other related theorems. (Contributed by Mario Carneiro, 1-Sep-2014) (Revised by Mario Carneiro, 11-Feb-2015)

Ref Expression
Hypotheses dvmptadd.s 
|- ( ph -> S e. { RR , CC } )
dvmptadd.a 
|- ( ( ph /\ x e. X ) -> A e. CC )
dvmptadd.b 
|- ( ( ph /\ x e. X ) -> B e. V )
dvmptadd.da 
|- ( ph -> ( S _D ( x e. X |-> A ) ) = ( x e. X |-> B ) )
Assertion dvmptcl 
|- ( ( ph /\ x e. X ) -> B e. CC )

Proof

Step Hyp Ref Expression
1 dvmptadd.s 
 |-  ( ph -> S e. { RR , CC } )
2 dvmptadd.a 
 |-  ( ( ph /\ x e. X ) -> A e. CC )
3 dvmptadd.b 
 |-  ( ( ph /\ x e. X ) -> B e. V )
4 dvmptadd.da 
 |-  ( ph -> ( S _D ( x e. X |-> A ) ) = ( x e. X |-> B ) )
5 dvfg 
 |-  ( S e. { RR , CC } -> ( S _D ( x e. X |-> A ) ) : dom ( S _D ( x e. X |-> A ) ) --> CC )
6 1 5 syl 
 |-  ( ph -> ( S _D ( x e. X |-> A ) ) : dom ( S _D ( x e. X |-> A ) ) --> CC )
7 4 dmeqd 
 |-  ( ph -> dom ( S _D ( x e. X |-> A ) ) = dom ( x e. X |-> B ) )
8 3 ralrimiva 
 |-  ( ph -> A. x e. X B e. V )
9 dmmptg 
 |-  ( A. x e. X B e. V -> dom ( x e. X |-> B ) = X )
10 8 9 syl 
 |-  ( ph -> dom ( x e. X |-> B ) = X )
11 7 10 eqtrd 
 |-  ( ph -> dom ( S _D ( x e. X |-> A ) ) = X )
12 11 feq2d 
 |-  ( ph -> ( ( S _D ( x e. X |-> A ) ) : dom ( S _D ( x e. X |-> A ) ) --> CC <-> ( S _D ( x e. X |-> A ) ) : X --> CC ) )
13 6 12 mpbid 
 |-  ( ph -> ( S _D ( x e. X |-> A ) ) : X --> CC )
14 4 feq1d 
 |-  ( ph -> ( ( S _D ( x e. X |-> A ) ) : X --> CC <-> ( x e. X |-> B ) : X --> CC ) )
15 13 14 mpbid 
 |-  ( ph -> ( x e. X |-> B ) : X --> CC )
16 15 fvmptelcdm 
 |-  ( ( ph /\ x e. X ) -> B e. CC )