Theorem fdivval

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

	Ref	Expression
Assertion	fdivval	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) → ( 𝐹 /f 𝐺 ) = ( ( 𝐹 ∘f / 𝐺 ) ↾ ( 𝐺 supp 0 ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-fdiv	⊢ /f = ( 𝑓 ∈ V , 𝑔 ∈ V ↦ ( ( 𝑓 ∘f / 𝑔 ) ↾ ( 𝑔 supp 0 ) ) )
2	1	a1i	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) → /f = ( 𝑓 ∈ V , 𝑔 ∈ V ↦ ( ( 𝑓 ∘f / 𝑔 ) ↾ ( 𝑔 supp 0 ) ) ) )
3		oveq12	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( 𝑓 ∘f / 𝑔 ) = ( 𝐹 ∘f / 𝐺 ) )
4		oveq1	⊢ ( 𝑔 = 𝐺 → ( 𝑔 supp 0 ) = ( 𝐺 supp 0 ) )
5	4	adantl	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( 𝑔 supp 0 ) = ( 𝐺 supp 0 ) )
6	3 5	reseq12d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( ( 𝑓 ∘f / 𝑔 ) ↾ ( 𝑔 supp 0 ) ) = ( ( 𝐹 ∘f / 𝐺 ) ↾ ( 𝐺 supp 0 ) ) )
7	6	adantl	⊢ ( ( ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) → ( ( 𝑓 ∘f / 𝑔 ) ↾ ( 𝑔 supp 0 ) ) = ( ( 𝐹 ∘f / 𝐺 ) ↾ ( 𝐺 supp 0 ) ) )
8		elex	⊢ ( 𝐹 ∈ 𝑉 → 𝐹 ∈ V )
9	8	adantr	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) → 𝐹 ∈ V )
10		elex	⊢ ( 𝐺 ∈ 𝑊 → 𝐺 ∈ V )
11	10	adantl	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) → 𝐺 ∈ V )
12		funmpt	⊢ Fun ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑥 ) / ( 𝐺 ‘ 𝑥 ) ) )
13		offval3	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) → ( 𝐹 ∘f / 𝐺 ) = ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑥 ) / ( 𝐺 ‘ 𝑥 ) ) ) )
14	13	funeqd	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) → ( Fun ( 𝐹 ∘f / 𝐺 ) ↔ Fun ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑥 ) / ( 𝐺 ‘ 𝑥 ) ) ) ) )
15	12 14	mpbiri	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) → Fun ( 𝐹 ∘f / 𝐺 ) )
16		ovex	⊢ ( 𝐺 supp 0 ) ∈ V
17		resfunexg	⊢ ( ( Fun ( 𝐹 ∘f / 𝐺 ) ∧ ( 𝐺 supp 0 ) ∈ V ) → ( ( 𝐹 ∘f / 𝐺 ) ↾ ( 𝐺 supp 0 ) ) ∈ V )
18	15 16 17	sylancl	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) → ( ( 𝐹 ∘f / 𝐺 ) ↾ ( 𝐺 supp 0 ) ) ∈ V )
19	2 7 9 11 18	ovmpod	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) → ( 𝐹 /f 𝐺 ) = ( ( 𝐹 ∘f / 𝐺 ) ↾ ( 𝐺 supp 0 ) ) )