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	$$⊢\phi \to S\in \left\{ℝ,ℂ\right\}$$
	dvmptadd.a	$$⊢\left(\phi \wedge x\in X\right)\to A\in ℂ$$
	dvmptadd.b	$$⊢\left(\phi \wedge x\in X\right)\to B\in V$$
	dvmptadd.da	$$⊢\phi \to \frac{d\left(x\in X⟼A\right)}{d_{S}x}=\left(x\in X⟼B\right)$$
Assertion	dvmptcl	$$⊢\left(\phi \wedge x\in X\right)\to B\in ℂ$$

Proof

Step	Hyp	Ref	Expression
1		dvmptadd.s	$$⊢\phi \to S\in \left\{ℝ,ℂ\right\}$$
2		dvmptadd.a	$$⊢\left(\phi \wedge x\in X\right)\to A\in ℂ$$
3		dvmptadd.b	$$⊢\left(\phi \wedge x\in X\right)\to B\in V$$
4		dvmptadd.da	$$⊢\phi \to \frac{d\left(x\in X⟼A\right)}{d_{S}x}=\left(x\in X⟼B\right)$$
5		dvfg	$$⊢S\in \left\{ℝ,ℂ\right\}\to \frac{d\left(x\in X⟼A\right)}{d_{S}x}:\mathrm{dom}\frac{d\left(x\in X⟼A\right)}{d_{S}x}⟶ℂ$$
6	1 5	syl	$$⊢\phi \to \frac{d\left(x\in X⟼A\right)}{d_{S}x}:\mathrm{dom}\frac{d\left(x\in X⟼A\right)}{d_{S}x}⟶ℂ$$
7	4	dmeqd	$$⊢\phi \to \mathrm{dom}\frac{d\left(x\in X⟼A\right)}{d_{S}x}=\mathrm{dom}\left(x\in X⟼B\right)$$
8	3	ralrimiva	$$⊢\phi \to \forall x\in XB\in V$$
9		dmmptg	$$⊢\forall x\in XB\in V\to \mathrm{dom}\left(x\in X⟼B\right)=X$$
10	8 9	syl	$$⊢\phi \to \mathrm{dom}\left(x\in X⟼B\right)=X$$
11	7 10	eqtrd	$$⊢\phi \to \mathrm{dom}\frac{d\left(x\in X⟼A\right)}{d_{S}x}=X$$
12	11	feq2d	$$⊢\phi \to \left(\frac{d\left(x\in X⟼A\right)}{d_{S}x}:\mathrm{dom}\frac{d\left(x\in X⟼A\right)}{d_{S}x}⟶ℂ\leftrightarrow \frac{d\left(x\in X⟼A\right)}{d_{S}x}:X⟶ℂ\right)$$
13	6 12	mpbid	$$⊢\phi \to \frac{d\left(x\in X⟼A\right)}{d_{S}x}:X⟶ℂ$$
14	4	feq1d	$$⊢\phi \to \left(\frac{d\left(x\in X⟼A\right)}{d_{S}x}:X⟶ℂ\leftrightarrow \left(x\in X⟼B\right):X⟶ℂ\right)$$
15	13 14	mpbid	$$⊢\phi \to \left(x\in X⟼B\right):X⟶ℂ$$
16	15	fvmptelcdm	$$⊢\left(\phi \wedge x\in X\right)\to B\in ℂ$$