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	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
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	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) ∈ ℂ )
12	2	feqmptd	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝑋 ↦ ( 𝐹 ‘ 𝑥 ) ) )
13	12	oveq2d	⊢ ( 𝜑 → ( 𝑆 D 𝐹 ) = ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( 𝐹 ‘ 𝑥 ) ) ) )
14	10	feqmptd	⊢ ( 𝜑 → ( 𝑆 D 𝐹 ) = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) ) )
15	13 14	eqtr3d	⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) ) )
16	3	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐺 ‘ 𝑥 ) ∈ ( ℂ ∖ { 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	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑆 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 · 𝐺 ) ) )