Theorem ulmdvlem2

Description: Lemma for ulmdv . (Contributed by Mario Carneiro, 8-May-2015)

	Ref	Expression
Hypotheses	ulmdv.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	ulmdv.s	$$⊢\phi \to S\in \left\{ℝ,ℂ\right\}$$
	ulmdv.m	$$⊢\phi \to M\in \mathbb{Z}$$
	ulmdv.f	$$⊢\phi \to F:Z⟶{ℂ}^X$$
	ulmdv.g	$$⊢\phi \to G:X⟶ℂ$$
	ulmdv.l	$$⊢\left(\phi \wedge z\in X\right)\to \left(k\in Z⟼F\left(k\right)\left(z\right)\right)⇝G\left(z\right)$$
	ulmdv.u	$$⊢\phi \to \left(k\in Z⟼S\mathrm{D}F\left(k\right)\right)\underset{u}{⇝}\left(X\right)H$$
Assertion	ulmdvlem2	$$⊢\left(\phi \wedge k\in Z\right)\to \mathrm{dom}{F\left(k\right)}_S^{\prime }=X$$

Proof

Step	Hyp	Ref	Expression
1		ulmdv.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		ulmdv.s	$$⊢\phi \to S\in \left\{ℝ,ℂ\right\}$$
3		ulmdv.m	$$⊢\phi \to M\in \mathbb{Z}$$
4		ulmdv.f	$$⊢\phi \to F:Z⟶{ℂ}^X$$
5		ulmdv.g	$$⊢\phi \to G:X⟶ℂ$$
6		ulmdv.l	$$⊢\left(\phi \wedge z\in X\right)\to \left(k\in Z⟼F\left(k\right)\left(z\right)\right)⇝G\left(z\right)$$
7		ulmdv.u	$$⊢\phi \to \left(k\in Z⟼S\mathrm{D}F\left(k\right)\right)\underset{u}{⇝}\left(X\right)H$$
8		ovex	$$⊢S\mathrm{D}F\left(k\right)\in \mathrm{V}$$
9	8	rgenw	$$⊢\forall k\in ZS\mathrm{D}F\left(k\right)\in \mathrm{V}$$
10		eqid	$$⊢\left(k\in Z⟼S\mathrm{D}F\left(k\right)\right)=\left(k\in Z⟼S\mathrm{D}F\left(k\right)\right)$$
11	10	fnmpt	$$⊢\forall k\in ZS\mathrm{D}F\left(k\right)\in \mathrm{V}\to \left(k\in Z⟼S\mathrm{D}F\left(k\right)\right)FnZ$$
12	9 11	mp1i	$$⊢\phi \to \left(k\in Z⟼S\mathrm{D}F\left(k\right)\right)FnZ$$
13		ulmf2	$$⊢\left(\left(k\in Z⟼S\mathrm{D}F\left(k\right)\right)FnZ\wedge \left(k\in Z⟼S\mathrm{D}F\left(k\right)\right)\underset{u}{⇝}\left(X\right)H\right)\to \left(k\in Z⟼S\mathrm{D}F\left(k\right)\right):Z⟶{ℂ}^X$$
14	12 7 13	syl2anc	$$⊢\phi \to \left(k\in Z⟼S\mathrm{D}F\left(k\right)\right):Z⟶{ℂ}^X$$
15	14	fvmptelcdm	$$⊢\left(\phi \wedge k\in Z\right)\to S\mathrm{D}F\left(k\right)\in \left({ℂ}^X\right)$$
16		elmapi	$$⊢S\mathrm{D}F\left(k\right)\in \left({ℂ}^X\right)\to {F\left(k\right)}_S^{\prime }:X⟶ℂ$$
17		fdm	$$⊢{F\left(k\right)}_S^{\prime }:X⟶ℂ\to \mathrm{dom}{F\left(k\right)}_S^{\prime }=X$$
18	15 16 17	3syl	$$⊢\left(\phi \wedge k\in Z\right)\to \mathrm{dom}{F\left(k\right)}_S^{\prime }=X$$