Metamath Proof Explorer

Theorem 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 𝐺 ) : ( 𝐺 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 ffvelcdmd ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐺 supp 0 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
8 simpl2 ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐺 supp 0 ) ) → 𝐺 : 𝐴 ⟶ ℝ )
9 8 6 ffvelcdmd ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐺 supp 0 ) ) → ( 𝐺 ‘ 𝑥 ) ∈ ℝ )
10 ffn ⊢ ( 𝐺 : 𝐴 ⟶ ℝ → 𝐺 Fn 𝐴 )
11 10 3ad2ant2 ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ 𝑉 ) → 𝐺 Fn 𝐴 )
12 simp3 ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ 𝑉 ) → 𝐴 ∈ 𝑉 )
13 0red ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ 𝑉 ) → 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 redivcld ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐺 supp 0 ) ) → ( ( 𝐹 ‘ 𝑥 ) / ( 𝐺 ‘ 𝑥 ) ) ∈ ℝ )
18 17 fmpttd ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ 𝑉 ) → ( 𝑥 ∈ ( 𝐺 supp 0 ) ↦ ( ( 𝐹 ‘ 𝑥 ) / ( 𝐺 ‘ 𝑥 ) ) ) : ( 𝐺 supp 0 ) ⟶ ℝ )
19 id ⊢ ( 𝐹 : 𝐴 ⟶ ℝ → 𝐹 : 𝐴 ⟶ ℝ )
20 ax-resscn ⊢ ℝ ⊆ ℂ
21 20 a1i ⊢ ( 𝐹 : 𝐴 ⟶ ℝ → ℝ ⊆ ℂ )
22 19 21 fssd ⊢ ( 𝐹 : 𝐴 ⟶ ℝ → 𝐹 : 𝐴 ⟶ ℂ )
23 id ⊢ ( 𝐺 : 𝐴 ⟶ ℝ → 𝐺 : 𝐴 ⟶ ℝ )
24 20 a1i ⊢ ( 𝐺 : 𝐴 ⟶ ℝ → ℝ ⊆ ℂ )
25 23 24 fssd ⊢ ( 𝐺 : 𝐴 ⟶ ℝ → 𝐺 : 𝐴 ⟶ ℂ )
26 id ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ 𝑉 )
27 22 25 26 3anim123i ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ 𝑉 ) → ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐴 ∈ 𝑉 ) )
28 fdivmpt ⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐴 ∈ 𝑉 ) → ( 𝐹 /f 𝐺 ) = ( 𝑥 ∈ ( 𝐺 supp 0 ) ↦ ( ( 𝐹 ‘ 𝑥 ) / ( 𝐺 ‘ 𝑥 ) ) ) )
29 27 28 syl ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ 𝑉 ) → ( 𝐹 /f 𝐺 ) = ( 𝑥 ∈ ( 𝐺 supp 0 ) ↦ ( ( 𝐹 ‘ 𝑥 ) / ( 𝐺 ‘ 𝑥 ) ) ) )
30 29 feq1d ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ 𝑉 ) → ( ( 𝐹 /f 𝐺 ) : ( 𝐺 supp 0 ) ⟶ ℝ ↔ ( 𝑥 ∈ ( 𝐺 supp 0 ) ↦ ( ( 𝐹 ‘ 𝑥 ) / ( 𝐺 ‘ 𝑥 ) ) ) : ( 𝐺 supp 0 ) ⟶ ℝ ) )
31 18 30 mpbird ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ 𝑉 ) → ( 𝐹 /f 𝐺 ) : ( 𝐺 supp 0 ) ⟶ ℝ )