# Metamath Proof Explorer

## Theorem ulmdvlem2

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

Ref Expression
Hypotheses ulmdv.z ${⊢}{Z}={ℤ}_{\ge {M}}$
ulmdv.s ${⊢}{\phi }\to {S}\in \left\{ℝ,ℂ\right\}$
ulmdv.m ${⊢}{\phi }\to {M}\in ℤ$
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
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}={ℤ}_{\ge {M}}$
2 ulmdv.s ${⊢}{\phi }\to {S}\in \left\{ℝ,ℂ\right\}$
3 ulmdv.m ${⊢}{\phi }\to {M}\in ℤ$
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
8 ovex ${⊢}{S}\mathrm{D}{F}\left({k}\right)\in \mathrm{V}$
9 8 rgenw ${⊢}\forall {k}\in {Z}\phantom{\rule{.4em}{0ex}}{S}\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 {Z}\phantom{\rule{.4em}{0ex}}{S}\mathrm{D}{F}\left({k}\right)\in \mathrm{V}\to \left({k}\in {Z}⟼{S}\mathrm{D}{F}\left({k}\right)\right)Fn{Z}$
12 9 11 mp1i ${⊢}{\phi }\to \left({k}\in {Z}⟼{S}\mathrm{D}{F}\left({k}\right)\right)Fn{Z}$
13 ulmf2
14 12 7 13 syl2anc ${⊢}{\phi }\to \left({k}\in {Z}⟼{S}\mathrm{D}{F}\left({k}\right)\right):{Z}⟶{ℂ}^{{X}}$
15 14 fvmptelrn ${⊢}\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}$