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

Metamath Proof Explorer

Theorem ulmdvlem2

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

Ref Expression
Hypotheses ulmdv.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
ulmdv.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
ulmdv.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
ulmdv.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑋 ) )
ulmdv.g ⊢ ( 𝜑 → 𝐺 : 𝑋 ⟶ ℂ )
ulmdv.l ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ⇝ ( 𝐺 ‘ 𝑧 ) )
ulmdv.u ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) ( ⇝𝑢 ‘ 𝑋 ) 𝐻 )
Assertion ulmdvlem2 ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → dom ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) = 𝑋 )

Proof

Step Hyp Ref Expression
1 ulmdv.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 ulmdv.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
3 ulmdv.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
4 ulmdv.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑋 ) )
5 ulmdv.g ⊢ ( 𝜑 → 𝐺 : 𝑋 ⟶ ℂ )
6 ulmdv.l ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ⇝ ( 𝐺 ‘ 𝑧 ) )
7 ulmdv.u ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) ( ⇝𝑢 ‘ 𝑋 ) 𝐻 )
8 ovex ⊢ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ∈ V
9 8 rgenw ⊢ ∀ 𝑘 ∈ 𝑍 ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ∈ V
10 eqid ⊢ ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) )
11 10 fnmpt ⊢ ( ∀ 𝑘 ∈ 𝑍 ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ∈ V → ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) Fn 𝑍 )
12 9 11 mp1i ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) Fn 𝑍 )
13 ulmf2 ⊢ ( ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) Fn 𝑍 ∧ ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) ( ⇝𝑢 ‘ 𝑋 ) 𝐻 ) → ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) : 𝑍 ⟶ ( ℂ ↑m 𝑋 ) )
14 12 7 13 syl2anc ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) : 𝑍 ⟶ ( ℂ ↑m 𝑋 ) )
15 14 fvmptelcdm ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ∈ ( ℂ ↑m 𝑋 ) )
16 elmapi ⊢ ( ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ∈ ( ℂ ↑m 𝑋 ) → ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) : 𝑋 ⟶ ℂ )
17 fdm ⊢ ( ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) : 𝑋 ⟶ ℂ → dom ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) = 𝑋 )
18 15 16 17 3syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → dom ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) = 𝑋 )