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

Metamath Proof Explorer

Theorem dvmptrecl

Description: Real closure of a derivative. (Contributed by Mario Carneiro, 18-May-2016)

Ref Expression
Hypotheses dvmptrecl.s ⊢ ( 𝜑 → 𝑆 ⊆ ℝ )
dvmptrecl.a ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐴 ∈ ℝ )
dvmptrecl.v ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐵 ∈ 𝑉 )
dvmptrecl.b ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) )
Assertion dvmptrecl ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐵 ∈ ℝ )

Proof

Step Hyp Ref Expression
1 dvmptrecl.s ⊢ ( 𝜑 → 𝑆 ⊆ ℝ )
2 dvmptrecl.a ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐴 ∈ ℝ )
3 dvmptrecl.v ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐵 ∈ 𝑉 )
4 dvmptrecl.b ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) )
5 2 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) : 𝑆 ⟶ ℝ )
6 dvfre ⊢ ( ( ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) : 𝑆 ⟶ ℝ ∧ 𝑆 ⊆ ℝ ) → ( ℝ D ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) : dom ( ℝ D ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) ⟶ ℝ )
7 5 1 6 syl2anc ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) : dom ( ℝ D ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) ⟶ ℝ )
8 4 dmeqd ⊢ ( 𝜑 → dom ( ℝ D ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) = dom ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) )
9 3 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑆 𝐵 ∈ 𝑉 )
10 dmmptg ⊢ ( ∀ 𝑥 ∈ 𝑆 𝐵 ∈ 𝑉 → dom ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) = 𝑆 )
11 9 10 syl ⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) = 𝑆 )
12 8 11 eqtrd ⊢ ( 𝜑 → dom ( ℝ D ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) = 𝑆 )
13 4 12 feq12d ⊢ ( 𝜑 → ( ( ℝ D ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) : dom ( ℝ D ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) ⟶ ℝ ↔ ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) : 𝑆 ⟶ ℝ ) )
14 7 13 mpbid ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) : 𝑆 ⟶ ℝ )
15 14 fvmptelcdm ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐵 ∈ ℝ )