refdivmptf

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

		Ref	Expression
	Assertion	refdivmptf	$⊢ (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		0red	$⊢ (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	redivcld	$⊢ ((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		id	$⊢ F : A ⟶ ℝ \to F : A ⟶ ℝ$
20		ax-resscn	$⊢ ℝ \subseteq ℂ$
21	20	a1i	$⊢ F : A ⟶ ℝ \to ℝ \subseteq ℂ$
22	19 21	fssd	$⊢ F : A ⟶ ℝ \to F : A ⟶ ℂ$
23		id	$⊢ G : A ⟶ ℝ \to G : A ⟶ ℝ$
24	20	a1i	$⊢ G : A ⟶ ℝ \to ℝ \subseteq ℂ$
25	23 24	fssd	$⊢ G : A ⟶ ℝ \to G : A ⟶ ℂ$
26		id	$⊢ A \in V \to A \in V$
27	22 25 26	3anim123i	$⊢ (F : A ⟶ ℝ \land G : A ⟶ ℝ \land A \in V) \to (F : A ⟶ ℂ \land G : A ⟶ ℂ \land A \in V)$
28		fdivmpt	$⊢ (F : A ⟶ ℂ \land G : A ⟶ ℂ \land A \in V) \to F /_{fG=(x \in {supp}_{0} (G) ⟼ \frac{F (x)}{G (x)})}$
29	27 28	syl	$⊢ (F : A ⟶ ℝ \land G : A ⟶ ℝ \land A \in V) \to F /_{fG=(x \in {supp}_{0} (G) ⟼ \frac{F (x)}{G (x)})}$
30	29	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 ⟶ ℝ}))$
31	18 30	mpbird	$⊢ (F : A ⟶ ℝ \land G : A ⟶ ℝ \land A \in V) \to (F /_{fG:G supp 0⟶ℝ})$

Metamath Proof Explorer

Theorem refdivmptf

Proof