Metamath Proof Explorer

Definition df-fdiv

Description: Define the division of two functions into the complex numbers. (Contributed by AV, 15-May-2020)

Ref Expression
Assertion df-fdiv 
|- /_f = ( f e. _V , g e. _V |-> ( ( f oF / g ) |` ( g supp 0 ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfdiv 
 |-  /_f
1 vf 
 |-  f
2 cvv 
 |-  _V
3 vg 
 |-  g
4 1 cv 
 |-  f
5 cdiv 
 |-  /
6 5 cof 
 |-  oF /
7 3 cv 
 |-  g
8 4 7 6 co 
 |-  ( f oF / g )
9 csupp 
 |-  supp
10 cc0 
 |-  0
11 7 10 9 co 
 |-  ( g supp 0 )
12 8 11 cres 
 |-  ( ( f oF / g ) |` ( g supp 0 ) )
13 1 3 2 2 12 cmpo 
 |-  ( f e. _V , g e. _V |-> ( ( f oF / g ) |` ( g supp 0 ) ) )
14 0 13 wceq 
 |-  /_f = ( f e. _V , g e. _V |-> ( ( f oF / g ) |` ( g supp 0 ) ) )