Metamath Proof Explorer

Theorem fdivval

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

Ref Expression
Assertion fdivval 
|- ( ( F e. V /\ G e. W ) -> ( F /_f G ) = ( ( F oF / G ) |` ( G supp 0 ) ) )

Proof

Step Hyp Ref Expression
1 df-fdiv 
 |-  /_f = ( f e. _V , g e. _V |-> ( ( f oF / g ) |` ( g supp 0 ) ) )
2 1 a1i 
 |-  ( ( F e. V /\ G e. W ) -> /_f = ( f e. _V , g e. _V |-> ( ( f oF / g ) |` ( g supp 0 ) ) ) )
3 oveq12 
 |-  ( ( f = F /\ g = G ) -> ( f oF / g ) = ( F oF / G ) )
4 oveq1 
 |-  ( g = G -> ( g supp 0 ) = ( G supp 0 ) )
5 4 adantl 
 |-  ( ( f = F /\ g = G ) -> ( g supp 0 ) = ( G supp 0 ) )
6 3 5 reseq12d 
 |-  ( ( f = F /\ g = G ) -> ( ( f oF / g ) |` ( g supp 0 ) ) = ( ( F oF / G ) |` ( G supp 0 ) ) )
7 6 adantl 
 |-  ( ( ( F e. V /\ G e. W ) /\ ( f = F /\ g = G ) ) -> ( ( f oF / g ) |` ( g supp 0 ) ) = ( ( F oF / G ) |` ( G supp 0 ) ) )
8 elex 
 |-  ( F e. V -> F e. _V )
9 8 adantr 
 |-  ( ( F e. V /\ G e. W ) -> F e. _V )
10 elex 
 |-  ( G e. W -> G e. _V )
11 10 adantl 
 |-  ( ( F e. V /\ G e. W ) -> G e. _V )
12 funmpt 
 |-  Fun ( x e. ( dom F i^i dom G ) |-> ( ( F ` x ) / ( G ` x ) ) )
13 offval3 
 |-  ( ( F e. V /\ G e. W ) -> ( F oF / G ) = ( x e. ( dom F i^i dom G ) |-> ( ( F ` x ) / ( G ` x ) ) ) )
14 13 funeqd 
 |-  ( ( F e. V /\ G e. W ) -> ( Fun ( F oF / G ) <-> Fun ( x e. ( dom F i^i dom G ) |-> ( ( F ` x ) / ( G ` x ) ) ) ) )
15 12 14 mpbiri 
 |-  ( ( F e. V /\ G e. W ) -> Fun ( F oF / G ) )
16 ovex 
 |-  ( G supp 0 ) e. _V
17 resfunexg 
 |-  ( ( Fun ( F oF / G ) /\ ( G supp 0 ) e. _V ) -> ( ( F oF / G ) |` ( G supp 0 ) ) e. _V )
18 15 16 17 sylancl 
 |-  ( ( F e. V /\ G e. W ) -> ( ( F oF / G ) |` ( G supp 0 ) ) e. _V )
19 2 7 9 11 18 ovmpod 
 |-  ( ( F e. V /\ G e. W ) -> ( F /_f G ) = ( ( F oF / G ) |` ( G supp 0 ) ) )