Users' Mathboxes 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 41650
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 ↦ ((𝑓𝑓 / 𝑔) ↾ (𝑔 supp 0)))
Distinct variable group:   𝑓,𝑔

Detailed syntax breakdown of Definition df-fdiv
StepHypRef Expression
1 cfdiv 41649 . 2 class /f
2 vf . . 3 setvar 𝑓
3 vg . . 3 setvar 𝑔
4 cvv 3189 . . 3 class V
52cv 1479 . . . . 5 class 𝑓
63cv 1479 . . . . 5 class 𝑔
7 cdiv 10636 . . . . . 6 class /
87cof 6855 . . . . 5 class 𝑓 /
95, 6, 8co 6610 . . . 4 class (𝑓𝑓 / 𝑔)
10 cc0 9888 . . . . 5 class 0
11 csupp 7247 . . . . 5 class supp
126, 10, 11co 6610 . . . 4 class (𝑔 supp 0)
139, 12cres 5081 . . 3 class ((𝑓𝑓 / 𝑔) ↾ (𝑔 supp 0))
142, 3, 4, 4, 13cmpt2 6612 . 2 class (𝑓 ∈ V, 𝑔 ∈ V ↦ ((𝑓𝑓 / 𝑔) ↾ (𝑔 supp 0)))
151, 14wceq 1480 1 wff /f = (𝑓 ∈ V, 𝑔 ∈ V ↦ ((𝑓𝑓 / 𝑔) ↾ (𝑔 supp 0)))
Colors of variables: wff setvar class
This definition is referenced by:  fdivval  41651
  Copyright terms: Public domain W3C validator