fdivmpt

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

		Ref	Expression
	Assertion	fdivmpt	$⊢ (F : A ⟶ ℂ \land G : A ⟶ ℂ \land A \in V) \to F /_{fG=(x \in {supp}_{0} (G) ⟼ \frac{F (x)}{G (x)})}$

Proof

Step	Hyp	Ref	Expression
1		fex	$⊢ (F : A ⟶ ℂ \land A \in V) \to F \in V$
2	1	3adant2	$⊢ (F : A ⟶ ℂ \land G : A ⟶ ℂ \land A \in V) \to F \in V$
3		fex	$⊢ (G : A ⟶ ℂ \land A \in V) \to G \in V$
4	3	3adant1	$⊢ (F : A ⟶ ℂ \land G : A ⟶ ℂ \land A \in V) \to G \in V$
5		fdivval	$⊢ (F \in V \land G \in V) \to F /_{fG={(F \div_{f} G) ↾}_{{supp}_{0} (G)}}$
6		offres	$⊢ (F \in V \land G \in V) \to {(F \div_{f} G) ↾}_{{supp}_{0} (G)} = ({F ↾}_{{supp}_{0} (G)}) \div_{f} ({G ↾}_{{supp}_{0} (G)})$
7	5 6	eqtrd	$⊢ (F \in V \land G \in V) \to F /_{fG=({F ↾}_{{supp}_{0} (G)}) \div_{f} ({G ↾}_{{supp}_{0} (G)})}$
8	2 4 7	syl2anc	$⊢ (F : A ⟶ ℂ \land G : A ⟶ ℂ \land A \in V) \to F /_{fG=({F ↾}_{{supp}_{0} (G)}) \div_{f} ({G ↾}_{{supp}_{0} (G)})}$
9		ffn	$⊢ F : A ⟶ ℂ \to F Fn A$
10	9	3ad2ant1	$⊢ (F : A ⟶ ℂ \land G : A ⟶ ℂ \land A \in V) \to F Fn A$
11		suppssdm	$⊢ G supp 0 \subseteq dom G$
12		fdm	$⊢ G : A ⟶ ℂ \to dom G = A$
13	12	eqcomd	$⊢ G : A ⟶ ℂ \to A = dom G$
14	13	3ad2ant2	$⊢ (F : A ⟶ ℂ \land G : A ⟶ ℂ \land A \in V) \to A = dom G$
15	11 14	sseqtrrid	$⊢ (F : A ⟶ ℂ \land G : A ⟶ ℂ \land A \in V) \to G supp 0 \subseteq A$
16		fnssres	$⊢ (F Fn A \land G supp 0 \subseteq A) \to ({F ↾}_{{supp}_{0} (G)}) Fn {supp}_{0} (G)$
17	10 15 16	syl2anc	$⊢ (F : A ⟶ ℂ \land G : A ⟶ ℂ \land A \in V) \to ({F ↾}_{{supp}_{0} (G)}) Fn {supp}_{0} (G)$
18		ffn	$⊢ G : A ⟶ ℂ \to G Fn A$
19	18	3ad2ant2	$⊢ (F : A ⟶ ℂ \land G : A ⟶ ℂ \land A \in V) \to G Fn A$
20		fnssres	$⊢ (G Fn A \land G supp 0 \subseteq A) \to ({G ↾}_{{supp}_{0} (G)}) Fn {supp}_{0} (G)$
21	19 15 20	syl2anc	$⊢ (F : A ⟶ ℂ \land G : A ⟶ ℂ \land A \in V) \to ({G ↾}_{{supp}_{0} (G)}) Fn {supp}_{0} (G)$
22		ovexd	$⊢ (F : A ⟶ ℂ \land G : A ⟶ ℂ \land A \in V) \to G supp 0 \in V$
23		inidm	$⊢ {supp}_{0} (G) \cap {supp}_{0} (G) = G supp 0$
24		fvres	$⊢ x \in {supp}_{0} (G) \to ({F ↾}_{{supp}_{0} (G)}) (x) = F (x)$
25	24	adantl	$⊢ ((F : A ⟶ ℂ \land G : A ⟶ ℂ \land A \in V) \land x \in {supp}_{0} (G)) \to ({F ↾}_{{supp}_{0} (G)}) (x) = F (x)$
26		fvres	$⊢ x \in {supp}_{0} (G) \to ({G ↾}_{{supp}_{0} (G)}) (x) = G (x)$
27	26	adantl	$⊢ ((F : A ⟶ ℂ \land G : A ⟶ ℂ \land A \in V) \land x \in {supp}_{0} (G)) \to ({G ↾}_{{supp}_{0} (G)}) (x) = G (x)$
28	17 21 22 22 23 25 27	offval	$⊢ (F : A ⟶ ℂ \land G : A ⟶ ℂ \land A \in V) \to ({F ↾}_{{supp}_{0} (G)}) \div_{f} ({G ↾}_{{supp}_{0} (G)}) = (x \in {supp}_{0} (G) ⟼ \frac{F (x)}{G (x)})$
29	8 28	eqtrd	$⊢ (F : A ⟶ ℂ \land G : A ⟶ ℂ \land A \in V) \to F /_{fG=(x \in {supp}_{0} (G) ⟼ \frac{F (x)}{G (x)})}$

Metamath Proof Explorer

Theorem fdivmpt

Proof