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

Metamath Proof Explorer

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 ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
dvmptadd.a ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ )
dvmptadd.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ 𝑉 )
dvmptadd.da ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) )
Assertion dvmptcl ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ ℂ )

Proof

Step Hyp Ref Expression
1 dvmptadd.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
2 dvmptadd.a ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ )
3 dvmptadd.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ 𝑉 )
4 dvmptadd.da ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) )
5 dvfg ⊢ ( 𝑆 ∈ { ℝ , ℂ } → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) : dom ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ⟶ ℂ )
6 1 5 syl ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) : dom ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ⟶ ℂ )
7 4 dmeqd ⊢ ( 𝜑 → dom ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = dom ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) )
8 3 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 𝐵 ∈ 𝑉 )
9 dmmptg ⊢ ( ∀ 𝑥 ∈ 𝑋 𝐵 ∈ 𝑉 → dom ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) = 𝑋 )
10 8 9 syl ⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) = 𝑋 )
11 7 10 eqtrd ⊢ ( 𝜑 → dom ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = 𝑋 )
12 11 feq2d ⊢ ( 𝜑 → ( ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) : dom ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ⟶ ℂ ↔ ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) : 𝑋 ⟶ ℂ ) )
13 6 12 mpbid ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) : 𝑋 ⟶ ℂ )
14 4 feq1d ⊢ ( 𝜑 → ( ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) : 𝑋 ⟶ ℂ ↔ ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) : 𝑋 ⟶ ℂ ) )
15 13 14 mpbid ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) : 𝑋 ⟶ ℂ )
16 15 fvmptelcdm ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ ℂ )