Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-fdiv Structured version   Visualization version   GIF version

Definition df-fdiv 44939
 Description: Define the division of two functions into the complex numbers. (Contributed by AV, 15-May-2020.)
Assertion
Ref Expression
df-fdiv /f = (𝑓 ∈ V, 𝑔 ∈ V ↦ ((𝑓f / 𝑔) ↾ (𝑔 supp 0)))
Distinct variable group:   𝑓,𝑔

Detailed syntax breakdown of Definition df-fdiv
StepHypRef Expression
1 cfdiv 44938 . 2 class /f
2 vf . . 3 setvar 𝑓
3 vg . . 3 setvar 𝑔
4 cvv 3444 . . 3 class V
52cv 1537 . . . . 5 class 𝑓
63cv 1537 . . . . 5 class 𝑔
7 cdiv 11290 . . . . . 6 class /
87cof 7391 . . . . 5 class f /
95, 6, 8co 7139 . . . 4 class (𝑓f / 𝑔)
10 cc0 10530 . . . . 5 class 0
11 csupp 7817 . . . . 5 class supp
126, 10, 11co 7139 . . . 4 class (𝑔 supp 0)
139, 12cres 5525 . . 3 class ((𝑓f / 𝑔) ↾ (𝑔 supp 0))
142, 3, 4, 4, 13cmpo 7141 . 2 class (𝑓 ∈ V, 𝑔 ∈ V ↦ ((𝑓f / 𝑔) ↾ (𝑔 supp 0)))
151, 14wceq 1538 1 wff /f = (𝑓 ∈ V, 𝑔 ∈ V ↦ ((𝑓f / 𝑔) ↾ (𝑔 supp 0)))
 Colors of variables: wff setvar class This definition is referenced by:  fdivval  44940
 Copyright terms: Public domain W3C validator