Metamath Proof Explorer

Theorem fdivmpt

Description: The quotient of two functions into the complex numbers as mapping. (Contributed by AV, 16-May-2020)

Ref Expression
Assertion fdivmpt ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐴 ∈ 𝑉 ) → ( 𝐹 /f 𝐺 ) = ( 𝑥 ∈ ( 𝐺 supp 0 ) ↦ ( ( 𝐹 ‘ 𝑥 ) / ( 𝐺 ‘ 𝑥 ) ) ) )

Proof

Step Hyp Ref Expression
1 fex ⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ∈ 𝑉 ) → 𝐹 ∈ V )
2 1 3adant2 ⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐴 ∈ 𝑉 ) → 𝐹 ∈ V )
3 fex ⊢ ( ( 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐴 ∈ 𝑉 ) → 𝐺 ∈ V )
4 3 3adant1 ⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐴 ∈ 𝑉 ) → 𝐺 ∈ V )
5 fdivval ⊢ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) → ( 𝐹 /f 𝐺 ) = ( ( 𝐹 ∘f / 𝐺 ) ↾ ( 𝐺 supp 0 ) ) )
6 offres ⊢ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) → ( ( 𝐹 ∘f / 𝐺 ) ↾ ( 𝐺 supp 0 ) ) = ( ( 𝐹 ↾ ( 𝐺 supp 0 ) ) ∘f / ( 𝐺 ↾ ( 𝐺 supp 0 ) ) ) )
7 5 6 eqtrd ⊢ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) → ( 𝐹 /f 𝐺 ) = ( ( 𝐹 ↾ ( 𝐺 supp 0 ) ) ∘f / ( 𝐺 ↾ ( 𝐺 supp 0 ) ) ) )
8 2 4 7 syl2anc ⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐴 ∈ 𝑉 ) → ( 𝐹 /f 𝐺 ) = ( ( 𝐹 ↾ ( 𝐺 supp 0 ) ) ∘f / ( 𝐺 ↾ ( 𝐺 supp 0 ) ) ) )
9 ffn ⊢ ( 𝐹 : 𝐴 ⟶ ℂ → 𝐹 Fn 𝐴 )
10 9 3ad2ant1 ⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐴 ∈ 𝑉 ) → 𝐹 Fn 𝐴 )
11 suppssdm ⊢ ( 𝐺 supp 0 ) ⊆ dom 𝐺
12 fdm ⊢ ( 𝐺 : 𝐴 ⟶ ℂ → dom 𝐺 = 𝐴 )
13 12 eqcomd ⊢ ( 𝐺 : 𝐴 ⟶ ℂ → 𝐴 = dom 𝐺 )
14 13 3ad2ant2 ⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐴 ∈ 𝑉 ) → 𝐴 = dom 𝐺 )
15 11 14 sseqtrrid ⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐴 ∈ 𝑉 ) → ( 𝐺 supp 0 ) ⊆ 𝐴 )
16 fnssres ⊢ ( ( 𝐹 Fn 𝐴 ∧ ( 𝐺 supp 0 ) ⊆ 𝐴 ) → ( 𝐹 ↾ ( 𝐺 supp 0 ) ) Fn ( 𝐺 supp 0 ) )
17 10 15 16 syl2anc ⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐴 ∈ 𝑉 ) → ( 𝐹 ↾ ( 𝐺 supp 0 ) ) Fn ( 𝐺 supp 0 ) )
18 ffn ⊢ ( 𝐺 : 𝐴 ⟶ ℂ → 𝐺 Fn 𝐴 )
19 18 3ad2ant2 ⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐴 ∈ 𝑉 ) → 𝐺 Fn 𝐴 )
20 fnssres ⊢ ( ( 𝐺 Fn 𝐴 ∧ ( 𝐺 supp 0 ) ⊆ 𝐴 ) → ( 𝐺 ↾ ( 𝐺 supp 0 ) ) Fn ( 𝐺 supp 0 ) )
21 19 15 20 syl2anc ⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐴 ∈ 𝑉 ) → ( 𝐺 ↾ ( 𝐺 supp 0 ) ) Fn ( 𝐺 supp 0 ) )
22 ovexd ⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐴 ∈ 𝑉 ) → ( 𝐺 supp 0 ) ∈ V )
23 inidm ⊢ ( ( 𝐺 supp 0 ) ∩ ( 𝐺 supp 0 ) ) = ( 𝐺 supp 0 )
24 fvres ⊢ ( 𝑥 ∈ ( 𝐺 supp 0 ) → ( ( 𝐹 ↾ ( 𝐺 supp 0 ) ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
25 24 adantl ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐺 supp 0 ) ) → ( ( 𝐹 ↾ ( 𝐺 supp 0 ) ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
26 fvres ⊢ ( 𝑥 ∈ ( 𝐺 supp 0 ) → ( ( 𝐺 ↾ ( 𝐺 supp 0 ) ) ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
27 26 adantl ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐺 supp 0 ) ) → ( ( 𝐺 ↾ ( 𝐺 supp 0 ) ) ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
28 17 21 22 22 23 25 27 offval ⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐴 ∈ 𝑉 ) → ( ( 𝐹 ↾ ( 𝐺 supp 0 ) ) ∘f / ( 𝐺 ↾ ( 𝐺 supp 0 ) ) ) = ( 𝑥 ∈ ( 𝐺 supp 0 ) ↦ ( ( 𝐹 ‘ 𝑥 ) / ( 𝐺 ‘ 𝑥 ) ) ) )
29 8 28 eqtrd ⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐴 ∈ 𝑉 ) → ( 𝐹 /f 𝐺 ) = ( 𝑥 ∈ ( 𝐺 supp 0 ) ↦ ( ( 𝐹 ‘ 𝑥 ) / ( 𝐺 ‘ 𝑥 ) ) ) )