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	fvmptelrn	|- ( ( ph /\ x e. X ) -> B e. CC )