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 ⊢ φ → S ∈ ℝ ℂ
dvmptadd.a ⊢ φ ∧ x ∈ X → A ∈ ℂ
dvmptadd.b ⊢ φ ∧ x ∈ X → B ∈ V
dvmptadd.da ⊢ φ → dx ∈ X A dS x = x ∈ X ⟼ B
Assertion dvmptcl ⊢ φ ∧ x ∈ X → B ∈ ℂ

Proof

Step Hyp Ref Expression
1 dvmptadd.s ⊢ φ → S ∈ ℝ ℂ
2 dvmptadd.a ⊢ φ ∧ x ∈ X → A ∈ ℂ
3 dvmptadd.b ⊢ φ ∧ x ∈ X → B ∈ V
4 dvmptadd.da ⊢ φ → dx ∈ X A dS x = x ∈ X ⟼ B
5 dvfg ⊢ S ∈ ℝ ℂ → dx ∈ X A dS x : dom ⁡ dx ∈ X A dS x ⟶ ℂ
6 1 5 syl ⊢ φ → dx ∈ X A dS x : dom ⁡ dx ∈ X A dS x ⟶ ℂ
7 4 dmeqd ⊢ φ → dom ⁡ dx ∈ X A dS x = dom ⁡ x ∈ X ⟼ B
8 3 ralrimiva ⊢ φ → ∀ x ∈ X B ∈ V
9 dmmptg ⊢ ∀ x ∈ X B ∈ V → dom ⁡ x ∈ X ⟼ B = X
10 8 9 syl ⊢ φ → dom ⁡ x ∈ X ⟼ B = X
11 7 10 eqtrd ⊢ φ → dom ⁡ dx ∈ X A dS x = X
12 11 feq2d ⊢ φ → dx ∈ X A dS x : dom ⁡ dx ∈ X A dS x ⟶ ℂ ↔ dx ∈ X A dS x : X ⟶ ℂ
13 6 12 mpbid ⊢ φ → dx ∈ X A dS x : X ⟶ ℂ
14 4 feq1d ⊢ φ → dx ∈ X A dS x : X ⟶ ℂ ↔ x ∈ X ⟼ B : X ⟶ ℂ
15 13 14 mpbid ⊢ φ → x ∈ X ⟼ B : X ⟶ ℂ
16 15 fvmptelrn ⊢ φ ∧ x ∈ X → B ∈ ℂ