Theorem fdivpm

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

	Ref	Expression
Assertion	fdivpm	⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐴 ∈ 𝑉 ) → ( 𝐹 /f 𝐺 ) ∈ ( ℂ ↑pm 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		cnex	⊢ ℂ ∈ V
2	1	a1i	⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐴 ∈ 𝑉 ) → ℂ ∈ V )
3		simp3	⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐴 ∈ 𝑉 ) → 𝐴 ∈ 𝑉 )
4		fdivmptf	⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐴 ∈ 𝑉 ) → ( 𝐹 /f 𝐺 ) : ( 𝐺 supp 0 ) ⟶ ℂ )
5		suppssdm	⊢ ( 𝐺 supp 0 ) ⊆ dom 𝐺
6		fdm	⊢ ( 𝐺 : 𝐴 ⟶ ℂ → dom 𝐺 = 𝐴 )
7	6	eqcomd	⊢ ( 𝐺 : 𝐴 ⟶ ℂ → 𝐴 = dom 𝐺 )
8	7	3ad2ant2	⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐴 ∈ 𝑉 ) → 𝐴 = dom 𝐺 )
9	5 8	sseqtrrid	⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐴 ∈ 𝑉 ) → ( 𝐺 supp 0 ) ⊆ 𝐴 )
10		elpm2r	⊢ ( ( ( ℂ ∈ V ∧ 𝐴 ∈ 𝑉 ) ∧ ( ( 𝐹 /f 𝐺 ) : ( 𝐺 supp 0 ) ⟶ ℂ ∧ ( 𝐺 supp 0 ) ⊆ 𝐴 ) ) → ( 𝐹 /f 𝐺 ) ∈ ( ℂ ↑pm 𝐴 ) )
11	2 3 4 9 10	syl22anc	⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐴 ∈ 𝑉 ) → ( 𝐹 /f 𝐺 ) ∈ ( ℂ ↑pm 𝐴 ) )