fdivmptf

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

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

Proof

Step	Hyp	Ref	Expression
1		simpl1	$⊢ ((F : A ⟶ ℂ \land G : A ⟶ ℂ \land A \in V) \land x \in {supp}_{0} (G)) \to F : A ⟶ ℂ$
2		suppssdm	$⊢ G supp 0 \subseteq dom G$
3		fdm	$⊢ G : A ⟶ ℂ \to dom G = A$
4	2 3	sseqtrid	$⊢ G : A ⟶ ℂ \to G supp 0 \subseteq A$
5	4	3ad2ant2	$⊢ (F : A ⟶ ℂ \land G : A ⟶ ℂ \land A \in V) \to G supp 0 \subseteq A$
6	5	sselda	$⊢ ((F : A ⟶ ℂ \land G : A ⟶ ℂ \land A \in V) \land x \in {supp}_{0} (G)) \to x \in A$
7	1 6	ffvelcdmd	$⊢ ((F : A ⟶ ℂ \land G : A ⟶ ℂ \land A \in V) \land x \in {supp}_{0} (G)) \to F (x) \in ℂ$
8		simpl2	$⊢ ((F : A ⟶ ℂ \land G : A ⟶ ℂ \land A \in V) \land x \in {supp}_{0} (G)) \to G : A ⟶ ℂ$
9	8 6	ffvelcdmd	$⊢ ((F : A ⟶ ℂ \land G : A ⟶ ℂ \land A \in V) \land x \in {supp}_{0} (G)) \to G (x) \in ℂ$
10		ffn	$⊢ G : A ⟶ ℂ \to G Fn A$
11	10	3ad2ant2	$⊢ (F : A ⟶ ℂ \land G : A ⟶ ℂ \land A \in V) \to G Fn A$
12		simp3	$⊢ (F : A ⟶ ℂ \land G : A ⟶ ℂ \land A \in V) \to A \in V$
13		0cnd	$⊢ (F : A ⟶ ℂ \land G : A ⟶ ℂ \land A \in V) \to 0 \in ℂ$
14		elsuppfn	$⊢ (G Fn A \land A \in V \land 0 \in ℂ) \to (x \in {supp}_{0} (G) \leftrightarrow (x \in A \land G (x) \neq 0))$
15	11 12 13 14	syl3anc	$⊢ (F : A ⟶ ℂ \land G : A ⟶ ℂ \land A \in V) \to (x \in {supp}_{0} (G) \leftrightarrow (x \in A \land G (x) \neq 0))$
16	15	simplbda	$⊢ ((F : A ⟶ ℂ \land G : A ⟶ ℂ \land A \in V) \land x \in {supp}_{0} (G)) \to G (x) \neq 0$
17	7 9 16	divcld	$⊢ ((F : A ⟶ ℂ \land G : A ⟶ ℂ \land A \in V) \land x \in {supp}_{0} (G)) \to \frac{F (x)}{G (x)} \in ℂ$
18	17	fmpttd	$⊢ (F : A ⟶ ℂ \land G : A ⟶ ℂ \land A \in V) \to (x \in {supp}_{0} (G) ⟼ \frac{F (x)}{G (x)}) : G supp 0 ⟶ ℂ$
19		fdivmpt	$⊢ (F : A ⟶ ℂ \land G : A ⟶ ℂ \land A \in V) \to F /_{fG=(x \in {supp}_{0} (G) ⟼ \frac{F (x)}{G (x)})}$
20	19	feq1d	$⊢ (F : A ⟶ ℂ \land G : A ⟶ ℂ \land A \in V) \to ((F /_{fG:G supp 0⟶ℂ\leftrightarrow(x \in {supp}_{0} (G) ⟼ \frac{F (x)}{G (x)}) : G supp 0 ⟶ ℂ}))$
21	18 20	mpbird	$⊢ (F : A ⟶ ℂ \land G : A ⟶ ℂ \land A \in V) \to (F /_{fG:G supp 0⟶ℂ})$

Metamath Proof Explorer

Theorem fdivmptf

Proof