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 = ( 𝑓 ∈ V , 𝑔 ∈ V ↦ ( ( 𝑓 ∘f / 𝑔 ) ↾ ( 𝑔 supp 0 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfdiv	⊢ /f
1		vf	⊢ 𝑓
2		cvv	⊢ V
3		vg	⊢ 𝑔
4	1	cv	⊢ 𝑓
5		cdiv	⊢ /
6	5	cof	⊢ ∘f /
7	3	cv	⊢ 𝑔
8	4 7 6	co	⊢ ( 𝑓 ∘f / 𝑔 )
9		csupp	⊢ supp
10		cc0	⊢ 0
11	7 10 9	co	⊢ ( 𝑔 supp 0 )
12	8 11	cres	⊢ ( ( 𝑓 ∘f / 𝑔 ) ↾ ( 𝑔 supp 0 ) )
13	1 3 2 2 12	cmpo	⊢ ( 𝑓 ∈ V , 𝑔 ∈ V ↦ ( ( 𝑓 ∘f / 𝑔 ) ↾ ( 𝑔 supp 0 ) ) )
14	0 13	wceq	⊢ /f = ( 𝑓 ∈ V , 𝑔 ∈ V ↦ ( ( 𝑓 ∘f / 𝑔 ) ↾ ( 𝑔 supp 0 ) ) )