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 \in V, g \in V ⟼ {(f \div_{f} g) ↾}_{{supp}_{0} (g)})}$

Step	Hyp	Ref	Expression
0		cfdiv	$class /_{f}$
1		vf	$setvar f$
2		cvv	$class V$
3		vg	$setvar g$
4	1	cv	$setvar f$
5		cdiv	$class \div$
6	5	cof	$class \circ_{f} \div$
7	3	cv	$setvar g$
8	4 7 6	co	$class (f \div_{f} g)$
9		csupp	$class supp$
10		cc0	$class 0$
11	7 10 9	co	$class {supp}_{0} (g)$
12	8 11	cres	$class ({(f \div_{f} g) ↾}_{{supp}_{0} (g)})$
13	1 3 2 2 12	cmpo	$class (f \in V, g \in V ⟼ {(f \div_{f} g) ↾}_{{supp}_{0} (g)})$
14	0 13	wceq	$wff /_{f=(f \in V, g \in V ⟼ {(f \div_{f} g) ↾}_{{supp}_{0} (g)})}$

Metamath Proof Explorer