Metamath Proof Explorer

Theorem dvdivf

Description: The quotient rule for everywhere-differentiable functions. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses dvdivf.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
dvdivf.f ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℂ )
dvdivf.g ⊢ ( 𝜑 → 𝐺 : 𝑋 ⟶ ( ℂ ∖ { 0 } ) )
dvdivf.fdv ⊢ ( 𝜑 → dom ( 𝑆 D 𝐹 ) = 𝑋 )
dvdivf.gdv ⊢ ( 𝜑 → dom ( 𝑆 D 𝐺 ) = 𝑋 )
Assertion dvdivf ( 𝜑 → ( 𝑆 D ( 𝐹 ∘f / 𝐺 ) ) = ( ( ( ( 𝑆 D 𝐹 ) ∘f · 𝐺 ) ∘f − ( ( 𝑆 D 𝐺 ) ∘f · 𝐹 ) ) ∘f / ( 𝐺 ∘f · 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 dvdivf.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
2 dvdivf.f ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℂ )
3 dvdivf.g ⊢ ( 𝜑 → 𝐺 : 𝑋 ⟶ ( ℂ ∖ { 0 } ) )
4 dvdivf.fdv ⊢ ( 𝜑 → dom ( 𝑆 D 𝐹 ) = 𝑋 )
5 dvdivf.gdv ⊢ ( 𝜑 → dom ( 𝑆 D 𝐺 ) = 𝑋 )
6 2 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
7 dvfg ⊢ ( 𝑆 ∈ { ℝ , ℂ } → ( 𝑆 D 𝐹 ) : dom ( 𝑆 D 𝐹 ) ⟶ ℂ )
8 1 7 syl ⊢ ( 𝜑 → ( 𝑆 D 𝐹 ) : dom ( 𝑆 D 𝐹 ) ⟶ ℂ )
9 4 feq2d ⊢ ( 𝜑 → ( ( 𝑆 D 𝐹 ) : dom ( 𝑆 D 𝐹 ) ⟶ ℂ ↔ ( 𝑆 D 𝐹 ) : 𝑋 ⟶ ℂ ) )
10 8 9 mpbid ⊢ ( 𝜑 → ( 𝑆 D 𝐹 ) : 𝑋 ⟶ ℂ )
11 10 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) ∈ ℂ )
12 2 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝑋 ↦ ( 𝐹 ‘ 𝑥 ) ) )
13 12 oveq2d ⊢ ( 𝜑 → ( 𝑆 D 𝐹 ) = ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( 𝐹 ‘ 𝑥 ) ) ) )
14 10 feqmptd ⊢ ( 𝜑 → ( 𝑆 D 𝐹 ) = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) ) )
15 13 14 eqtr3d ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) ) )
16 3 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐺 ‘ 𝑥 ) ∈ ( ℂ ∖ { 0 } ) )
17 dvfg ⊢ ( 𝑆 ∈ { ℝ , ℂ } → ( 𝑆 D 𝐺 ) : dom ( 𝑆 D 𝐺 ) ⟶ ℂ )
18 1 17 syl ⊢ ( 𝜑 → ( 𝑆 D 𝐺 ) : dom ( 𝑆 D 𝐺 ) ⟶ ℂ )
19 5 feq2d ⊢ ( 𝜑 → ( ( 𝑆 D 𝐺 ) : dom ( 𝑆 D 𝐺 ) ⟶ ℂ ↔ ( 𝑆 D 𝐺 ) : 𝑋 ⟶ ℂ ) )
20 18 19 mpbid ⊢ ( 𝜑 → ( 𝑆 D 𝐺 ) : 𝑋 ⟶ ℂ )
21 20 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑆 D 𝐺 ) ‘ 𝑥 ) ∈ ℂ )
22 3 feqmptd ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝑋 ↦ ( 𝐺 ‘ 𝑥 ) ) )
23 22 oveq2d ⊢ ( 𝜑 → ( 𝑆 D 𝐺 ) = ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( 𝐺 ‘ 𝑥 ) ) ) )
24 20 feqmptd ⊢ ( 𝜑 → ( 𝑆 D 𝐺 ) = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑆 D 𝐺 ) ‘ 𝑥 ) ) )
25 23 24 eqtr3d ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( 𝐺 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑆 D 𝐺 ) ‘ 𝑥 ) ) )
26 1 6 11 15 16 21 25 dvmptdiv ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( ( 𝐹 ‘ 𝑥 ) / ( 𝐺 ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ( ( ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) − ( ( ( 𝑆 D 𝐺 ) ‘ 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) ) / ( ( 𝐺 ‘ 𝑥 ) ↑ 2 ) ) ) )
27 ovex ⊢ ( 𝑆 D 𝐹 ) ∈ V
28 27 dmex ⊢ dom ( 𝑆 D 𝐹 ) ∈ V
29 4 28 eqeltrrdi ⊢ ( 𝜑 → 𝑋 ∈ V )
30 29 6 16 12 22 offval2 ⊢ ( 𝜑 → ( 𝐹 ∘f / 𝐺 ) = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝐹 ‘ 𝑥 ) / ( 𝐺 ‘ 𝑥 ) ) ) )
31 30 oveq2d ⊢ ( 𝜑 → ( 𝑆 D ( 𝐹 ∘f / 𝐺 ) ) = ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( ( 𝐹 ‘ 𝑥 ) / ( 𝐺 ‘ 𝑥 ) ) ) ) )
32 ovexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) − ( ( ( 𝑆 D 𝐺 ) ‘ 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) ) ∈ V )
33 16 eldifad ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐺 ‘ 𝑥 ) ∈ ℂ )
34 33 sqcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐺 ‘ 𝑥 ) ↑ 2 ) ∈ ℂ )
35 11 33 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ∈ ℂ )
36 21 6 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( ( 𝑆 D 𝐺 ) ‘ 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) ∈ ℂ )
37 29 11 33 14 22 offval2 ⊢ ( 𝜑 → ( ( 𝑆 D 𝐹 ) ∘f · 𝐺 ) = ( 𝑥 ∈ 𝑋 ↦ ( ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) )
38 29 21 6 24 12 offval2 ⊢ ( 𝜑 → ( ( 𝑆 D 𝐺 ) ∘f · 𝐹 ) = ( 𝑥 ∈ 𝑋 ↦ ( ( ( 𝑆 D 𝐺 ) ‘ 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) ) )
39 29 35 36 37 38 offval2 ⊢ ( 𝜑 → ( ( ( 𝑆 D 𝐹 ) ∘f · 𝐺 ) ∘f − ( ( 𝑆 D 𝐺 ) ∘f · 𝐹 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ( ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) − ( ( ( 𝑆 D 𝐺 ) ‘ 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) ) ) )
40 29 16 16 22 22 offval2 ⊢ ( 𝜑 → ( 𝐺 ∘f · 𝐺 ) = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝐺 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) )
41 33 sqvald ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐺 ‘ 𝑥 ) ↑ 2 ) = ( ( 𝐺 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) )
42 41 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 2 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝐺 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) )
43 40 42 eqtr4d ⊢ ( 𝜑 → ( 𝐺 ∘f · 𝐺 ) = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 2 ) ) )
44 29 32 34 39 43 offval2 ⊢ ( 𝜑 → ( ( ( ( 𝑆 D 𝐹 ) ∘f · 𝐺 ) ∘f − ( ( 𝑆 D 𝐺 ) ∘f · 𝐹 ) ) ∘f / ( 𝐺 ∘f · 𝐺 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ( ( ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) − ( ( ( 𝑆 D 𝐺 ) ‘ 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) ) / ( ( 𝐺 ‘ 𝑥 ) ↑ 2 ) ) ) )
45 26 31 44 3eqtr4d ⊢ ( 𝜑 → ( 𝑆 D ( 𝐹 ∘f / 𝐺 ) ) = ( ( ( ( 𝑆 D 𝐹 ) ∘f · 𝐺 ) ∘f − ( ( 𝑆 D 𝐺 ) ∘f · 𝐹 ) ) ∘f / ( 𝐺 ∘f · 𝐺 ) ) )