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	fvmptelrn	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ∈ ( ℂ ↑m 𝑋 ) )
16		elmapi	⊢ ( ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ∈ ( ℂ ↑m 𝑋 ) → ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) : 𝑋 ⟶ ℂ )
17		fdm	⊢ ( ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) : 𝑋 ⟶ ℂ → dom ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) = 𝑋 )
18	15 16 17	3syl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → dom ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) = 𝑋 )