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	fvmptelrn	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐵 ∈ ℝ )