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 𝐺 ) : ( 𝐺 supp 0 ) ⟶ ℂ )

Proof

Step	Hyp	Ref	Expression
1		simpl1	⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐺 supp 0 ) ) → 𝐹 : 𝐴 ⟶ ℂ )
2		suppssdm	⊢ ( 𝐺 supp 0 ) ⊆ dom 𝐺
3		fdm	⊢ ( 𝐺 : 𝐴 ⟶ ℂ → dom 𝐺 = 𝐴 )
4	2 3	sseqtrid	⊢ ( 𝐺 : 𝐴 ⟶ ℂ → ( 𝐺 supp 0 ) ⊆ 𝐴 )
5	4	3ad2ant2	⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐴 ∈ 𝑉 ) → ( 𝐺 supp 0 ) ⊆ 𝐴 )
6	5	sselda	⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐺 supp 0 ) ) → 𝑥 ∈ 𝐴 )
7	1 6	ffvelrnd	⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐺 supp 0 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
8		simpl2	⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐺 supp 0 ) ) → 𝐺 : 𝐴 ⟶ ℂ )
9	8 6	ffvelrnd	⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐺 supp 0 ) ) → ( 𝐺 ‘ 𝑥 ) ∈ ℂ )
10		ffn	⊢ ( 𝐺 : 𝐴 ⟶ ℂ → 𝐺 Fn 𝐴 )
11	10	3ad2ant2	⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐴 ∈ 𝑉 ) → 𝐺 Fn 𝐴 )
12		simp3	⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐴 ∈ 𝑉 ) → 𝐴 ∈ 𝑉 )
13		0cnd	⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐴 ∈ 𝑉 ) → 0 ∈ ℂ )
14		elsuppfn	⊢ ( ( 𝐺 Fn 𝐴 ∧ 𝐴 ∈ 𝑉 ∧ 0 ∈ ℂ ) → ( 𝑥 ∈ ( 𝐺 supp 0 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝐺 ‘ 𝑥 ) ≠ 0 ) ) )
15	11 12 13 14	syl3anc	⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐴 ∈ 𝑉 ) → ( 𝑥 ∈ ( 𝐺 supp 0 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝐺 ‘ 𝑥 ) ≠ 0 ) ) )
16	15	simplbda	⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐺 supp 0 ) ) → ( 𝐺 ‘ 𝑥 ) ≠ 0 )
17	7 9 16	divcld	⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐺 supp 0 ) ) → ( ( 𝐹 ‘ 𝑥 ) / ( 𝐺 ‘ 𝑥 ) ) ∈ ℂ )
18	17	fmpttd	⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐴 ∈ 𝑉 ) → ( 𝑥 ∈ ( 𝐺 supp 0 ) ↦ ( ( 𝐹 ‘ 𝑥 ) / ( 𝐺 ‘ 𝑥 ) ) ) : ( 𝐺 supp 0 ) ⟶ ℂ )
19		fdivmpt	⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐴 ∈ 𝑉 ) → ( 𝐹 /f 𝐺 ) = ( 𝑥 ∈ ( 𝐺 supp 0 ) ↦ ( ( 𝐹 ‘ 𝑥 ) / ( 𝐺 ‘ 𝑥 ) ) ) )
20	19	feq1d	⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐴 ∈ 𝑉 ) → ( ( 𝐹 /f 𝐺 ) : ( 𝐺 supp 0 ) ⟶ ℂ ↔ ( 𝑥 ∈ ( 𝐺 supp 0 ) ↦ ( ( 𝐹 ‘ 𝑥 ) / ( 𝐺 ‘ 𝑥 ) ) ) : ( 𝐺 supp 0 ) ⟶ ℂ ) )
21	18 20	mpbird	⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐴 ∈ 𝑉 ) → ( 𝐹 /f 𝐺 ) : ( 𝐺 supp 0 ) ⟶ ℂ )