Metamath Proof Explorer

Theorem 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 ⟶ ℂ ∧ G : A ⟶ ℂ ∧ A ∈ V → F / f G : G supp 0 ⟶ ℂ

Proof

Step Hyp Ref Expression
1 simpl1 ⊢ F : A ⟶ ℂ ∧ G : A ⟶ ℂ ∧ A ∈ V ∧ x ∈ supp 0 ⁡ G → F : A ⟶ ℂ
2 suppssdm ⊢ G supp 0 ⊆ dom ⁡ G
3 fdm ⊢ G : A ⟶ ℂ → dom ⁡ G = A
4 2 3 sseqtrid ⊢ G : A ⟶ ℂ → G supp 0 ⊆ A
5 4 3ad2ant2 ⊢ F : A ⟶ ℂ ∧ G : A ⟶ ℂ ∧ A ∈ V → G supp 0 ⊆ A
6 5 sselda ⊢ F : A ⟶ ℂ ∧ G : A ⟶ ℂ ∧ A ∈ V ∧ x ∈ supp 0 ⁡ G → x ∈ A
7 1 6 ffvelrnd ⊢ F : A ⟶ ℂ ∧ G : A ⟶ ℂ ∧ A ∈ V ∧ x ∈ supp 0 ⁡ G → F ⁡ x ∈ ℂ
8 simpl2 ⊢ F : A ⟶ ℂ ∧ G : A ⟶ ℂ ∧ A ∈ V ∧ x ∈ supp 0 ⁡ G → G : A ⟶ ℂ
9 8 6 ffvelrnd ⊢ F : A ⟶ ℂ ∧ G : A ⟶ ℂ ∧ A ∈ V ∧ x ∈ supp 0 ⁡ G → G ⁡ x ∈ ℂ
10 ffn ⊢ G : A ⟶ ℂ → G Fn A
11 10 3ad2ant2 ⊢ F : A ⟶ ℂ ∧ G : A ⟶ ℂ ∧ A ∈ V → G Fn A
12 simp3 ⊢ F : A ⟶ ℂ ∧ G : A ⟶ ℂ ∧ A ∈ V → A ∈ V
13 0cnd ⊢ F : A ⟶ ℂ ∧ G : A ⟶ ℂ ∧ A ∈ V → 0 ∈ ℂ
14 elsuppfn ⊢ G Fn A ∧ A ∈ V ∧ 0 ∈ ℂ → x ∈ supp 0 ⁡ G ↔ x ∈ A ∧ G ⁡ x ≠ 0
15 11 12 13 14 syl3anc ⊢ F : A ⟶ ℂ ∧ G : A ⟶ ℂ ∧ A ∈ V → x ∈ supp 0 ⁡ G ↔ x ∈ A ∧ G ⁡ x ≠ 0
16 15 simplbda ⊢ F : A ⟶ ℂ ∧ G : A ⟶ ℂ ∧ A ∈ V ∧ x ∈ supp 0 ⁡ G → G ⁡ x ≠ 0
17 7 9 16 divcld ⊢ F : A ⟶ ℂ ∧ G : A ⟶ ℂ ∧ A ∈ V ∧ x ∈ supp 0 ⁡ G → F ⁡ x G ⁡ x ∈ ℂ
18 17 fmpttd ⊢ F : A ⟶ ℂ ∧ G : A ⟶ ℂ ∧ A ∈ V → x ∈ supp 0 ⁡ G ⟼ F ⁡ x G ⁡ x : G supp 0 ⟶ ℂ
19 fdivmpt ⊢ F : A ⟶ ℂ ∧ G : A ⟶ ℂ ∧ A ∈ V → F / f G = x ∈ supp 0 ⁡ G ⟼ F ⁡ x G ⁡ x
20 19 feq1d ⊢ F : A ⟶ ℂ ∧ G : A ⟶ ℂ ∧ A ∈ V → F / f G : G supp 0 ⟶ ℂ ↔ x ∈ supp 0 ⁡ G ⟼ F ⁡ x G ⁡ x : G supp 0 ⟶ ℂ
21 18 20 mpbird ⊢ F : A ⟶ ℂ ∧ G : A ⟶ ℂ ∧ A ∈ V → F / f G : G supp 0 ⟶ ℂ