fdivval

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

		Ref	Expression
	Assertion	fdivval	$⊢ (F \in V \land G \in W) \to F /_{fG={(F \div_{f} G) ↾}_{{supp}_{0} (G)}}$

Step	Hyp	Ref	Expression
1		df-fdiv	$⊢ /_{f=(f \in V, g \in V ⟼ {(f \div_{f} g) ↾}_{{supp}_{0} (g)})}$
2	1	a1i	$⊢ (F \in V \land G \in W) \to /_{f=(f \in V, g \in V ⟼ {(f \div_{f} g) ↾}_{{supp}_{0} (g)})}$
3		oveq12	$⊢ (f = F \land g = G) \to f \div_{f} g = F \div_{f} G$
4		oveq1	$⊢ g = G \to g supp 0 = G supp 0$
5	4	adantl	$⊢ (f = F \land g = G) \to g supp 0 = G supp 0$
6	3 5	reseq12d	$⊢ (f = F \land g = G) \to {(f \div_{f} g) ↾}_{{supp}_{0} (g)} = {(F \div_{f} G) ↾}_{{supp}_{0} (G)}$
7	6	adantl	$⊢ ((F \in V \land G \in W) \land (f = F \land g = G)) \to {(f \div_{f} g) ↾}_{{supp}_{0} (g)} = {(F \div_{f} G) ↾}_{{supp}_{0} (G)}$
8		elex	$⊢ F \in V \to F \in V$
9	8	adantr	$⊢ (F \in V \land G \in W) \to F \in V$
10		elex	$⊢ G \in W \to G \in V$
11	10	adantl	$⊢ (F \in V \land G \in W) \to G \in V$
12		funmpt	$⊢ Fun (x \in (dom F \cap dom G) ⟼ \frac{F (x)}{G (x)})$
13		offval3	$⊢ (F \in V \land G \in W) \to F \div_{f} G = (x \in (dom F \cap dom G) ⟼ \frac{F (x)}{G (x)})$
14	13	funeqd	$⊢ (F \in V \land G \in W) \to (Fun (F \div_{f} G) \leftrightarrow Fun (x \in (dom F \cap dom G) ⟼ \frac{F (x)}{G (x)}))$
15	12 14	mpbiri	$⊢ (F \in V \land G \in W) \to Fun (F \div_{f} G)$
16		ovex	$⊢ G supp 0 \in V$
17		resfunexg	$⊢ (Fun (F \div_{f} G) \land G supp 0 \in V) \to {(F \div_{f} G) ↾}_{{supp}_{0} (G)} \in V$
18	15 16 17	sylancl	$⊢ (F \in V \land G \in W) \to {(F \div_{f} G) ↾}_{{supp}_{0} (G)} \in V$
19	2 7 9 11 18	ovmpod	$⊢ (F \in V \land G \in W) \to F /_{fG={(F \div_{f} G) ↾}_{{supp}_{0} (G)}}$

Metamath Proof Explorer