Metamath Proof Explorer

Theorem dvfre

Description: The derivative of a real function is real. (Contributed by Mario Carneiro, 1-Sep-2014)

Ref Expression
Assertion dvfre ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) → ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℝ )

Proof

Step Hyp Ref Expression
1 dvf ⊢ ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℂ
2 ffn ⊢ ( ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℂ → ( ℝ D 𝐹 ) Fn dom ( ℝ D 𝐹 ) )
3 1 2 mp1i ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) → ( ℝ D 𝐹 ) Fn dom ( ℝ D 𝐹 ) )
4 1 ffvelcdmi ⊢ ( 𝑥 ∈ dom ( ℝ D 𝐹 ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ∈ ℂ )
5 4 adantl ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ 𝑥 ∈ dom ( ℝ D 𝐹 ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ∈ ℂ )
6 simpr ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ 𝑥 ∈ dom ( ℝ D 𝐹 ) ) → 𝑥 ∈ dom ( ℝ D 𝐹 ) )
7 fvco3 ⊢ ( ( ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℂ ∧ 𝑥 ∈ dom ( ℝ D 𝐹 ) ) → ( ( ∗ ∘ ( ℝ D 𝐹 ) ) ‘ 𝑥 ) = ( ∗ ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) )
8 1 6 7 sylancr ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ 𝑥 ∈ dom ( ℝ D 𝐹 ) ) → ( ( ∗ ∘ ( ℝ D 𝐹 ) ) ‘ 𝑥 ) = ( ∗ ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) )
9 ax-resscn ⊢ ℝ ⊆ ℂ
10 fss ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ ℝ ⊆ ℂ ) → 𝐹 : 𝐴 ⟶ ℂ )
11 9 10 mpan2 ⊢ ( 𝐹 : 𝐴 ⟶ ℝ → 𝐹 : 𝐴 ⟶ ℂ )
12 dvcj ⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) → ( ℝ D ( ∗ ∘ 𝐹 ) ) = ( ∗ ∘ ( ℝ D 𝐹 ) ) )
13 11 12 sylan ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) → ( ℝ D ( ∗ ∘ 𝐹 ) ) = ( ∗ ∘ ( ℝ D 𝐹 ) ) )
14 ffvelcdm ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝑦 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
15 14 adantlr ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
16 15 cjred ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → ( ∗ ‘ ( 𝐹 ‘ 𝑦 ) ) = ( 𝐹 ‘ 𝑦 ) )
17 16 mpteq2dva ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) → ( 𝑦 ∈ 𝐴 ↦ ( ∗ ‘ ( 𝐹 ‘ 𝑦 ) ) ) = ( 𝑦 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑦 ) ) )
18 15 recnd ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℂ )
19 simpl ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) → 𝐹 : 𝐴 ⟶ ℝ )
20 19 feqmptd ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) → 𝐹 = ( 𝑦 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑦 ) ) )
21 cjf ⊢ ∗ : ℂ ⟶ ℂ
22 21 a1i ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) → ∗ : ℂ ⟶ ℂ )
23 22 feqmptd ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) → ∗ = ( 𝑧 ∈ ℂ ↦ ( ∗ ‘ 𝑧 ) ) )
24 fveq2 ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑦 ) → ( ∗ ‘ 𝑧 ) = ( ∗ ‘ ( 𝐹 ‘ 𝑦 ) ) )
25 18 20 23 24 fmptco ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) → ( ∗ ∘ 𝐹 ) = ( 𝑦 ∈ 𝐴 ↦ ( ∗ ‘ ( 𝐹 ‘ 𝑦 ) ) ) )
26 17 25 20 3eqtr4d ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) → ( ∗ ∘ 𝐹 ) = 𝐹 )
27 26 oveq2d ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) → ( ℝ D ( ∗ ∘ 𝐹 ) ) = ( ℝ D 𝐹 ) )
28 13 27 eqtr3d ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) → ( ∗ ∘ ( ℝ D 𝐹 ) ) = ( ℝ D 𝐹 ) )
29 28 fveq1d ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) → ( ( ∗ ∘ ( ℝ D 𝐹 ) ) ‘ 𝑥 ) = ( ( ℝ D 𝐹 ) ‘ 𝑥 ) )
30 29 adantr ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ 𝑥 ∈ dom ( ℝ D 𝐹 ) ) → ( ( ∗ ∘ ( ℝ D 𝐹 ) ) ‘ 𝑥 ) = ( ( ℝ D 𝐹 ) ‘ 𝑥 ) )
31 8 30 eqtr3d ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ 𝑥 ∈ dom ( ℝ D 𝐹 ) ) → ( ∗ ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) = ( ( ℝ D 𝐹 ) ‘ 𝑥 ) )
32 5 31 cjrebd ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ 𝑥 ∈ dom ( ℝ D 𝐹 ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ∈ ℝ )
33 32 ralrimiva ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) → ∀ 𝑥 ∈ dom ( ℝ D 𝐹 ) ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ∈ ℝ )
34 ffnfv ⊢ ( ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℝ ↔ ( ( ℝ D 𝐹 ) Fn dom ( ℝ D 𝐹 ) ∧ ∀ 𝑥 ∈ dom ( ℝ D 𝐹 ) ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ∈ ℝ ) )
35 3 33 34 sylanbrc ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) → ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℝ )