Metamath Proof Explorer

Theorem ofdivrec

Description: Function analogue of divrec , a division analogue of ofnegsub . (Contributed by Steve Rodriguez, 3-Nov-2015)

Ref Expression
Assertion ofdivrec 
|- ( ( A e. V /\ F : A --> CC /\ G : A --> ( CC \ { 0 } ) ) -> ( F oF x. ( ( A X. { 1 } ) oF / G ) ) = ( F oF / G ) )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( A e. V /\ F : A --> CC /\ G : A --> ( CC \ { 0 } ) ) -> A e. V )
2 simp2 
 |-  ( ( A e. V /\ F : A --> CC /\ G : A --> ( CC \ { 0 } ) ) -> F : A --> CC )
3 2 ffnd 
 |-  ( ( A e. V /\ F : A --> CC /\ G : A --> ( CC \ { 0 } ) ) -> F Fn A )
4 ax-1cn 
 |-  1 e. CC
5 fnconstg 
 |-  ( 1 e. CC -> ( A X. { 1 } ) Fn A )
6 4 5 mp1i 
 |-  ( ( A e. V /\ F : A --> CC /\ G : A --> ( CC \ { 0 } ) ) -> ( A X. { 1 } ) Fn A )
7 simp3 
 |-  ( ( A e. V /\ F : A --> CC /\ G : A --> ( CC \ { 0 } ) ) -> G : A --> ( CC \ { 0 } ) )
8 7 ffnd 
 |-  ( ( A e. V /\ F : A --> CC /\ G : A --> ( CC \ { 0 } ) ) -> G Fn A )
9 inidm 
 |-  ( A i^i A ) = A
10 6 8 1 1 9 offn 
 |-  ( ( A e. V /\ F : A --> CC /\ G : A --> ( CC \ { 0 } ) ) -> ( ( A X. { 1 } ) oF / G ) Fn A )
11 3 8 1 1 9 offn 
 |-  ( ( A e. V /\ F : A --> CC /\ G : A --> ( CC \ { 0 } ) ) -> ( F oF / G ) Fn A )
12 eqidd 
 |-  ( ( ( A e. V /\ F : A --> CC /\ G : A --> ( CC \ { 0 } ) ) /\ x e. A ) -> ( F ` x ) = ( F ` x ) )
13 1cnd 
 |-  ( ( A e. V /\ F : A --> CC /\ G : A --> ( CC \ { 0 } ) ) -> 1 e. CC )
14 eqidd 
 |-  ( ( ( A e. V /\ F : A --> CC /\ G : A --> ( CC \ { 0 } ) ) /\ x e. A ) -> ( G ` x ) = ( G ` x ) )
15 1 13 8 14 ofc1 
 |-  ( ( ( A e. V /\ F : A --> CC /\ G : A --> ( CC \ { 0 } ) ) /\ x e. A ) -> ( ( ( A X. { 1 } ) oF / G ) ` x ) = ( 1 / ( G ` x ) ) )
16 ffvelrn 
 |-  ( ( F : A --> CC /\ x e. A ) -> ( F ` x ) e. CC )
17 2 16 sylan 
 |-  ( ( ( A e. V /\ F : A --> CC /\ G : A --> ( CC \ { 0 } ) ) /\ x e. A ) -> ( F ` x ) e. CC )
18 ffvelrn 
 |-  ( ( G : A --> ( CC \ { 0 } ) /\ x e. A ) -> ( G ` x ) e. ( CC \ { 0 } ) )
19 eldifsn 
 |-  ( ( G ` x ) e. ( CC \ { 0 } ) <-> ( ( G ` x ) e. CC /\ ( G ` x ) =/= 0 ) )
20 18 19 sylib 
 |-  ( ( G : A --> ( CC \ { 0 } ) /\ x e. A ) -> ( ( G ` x ) e. CC /\ ( G ` x ) =/= 0 ) )
21 7 20 sylan 
 |-  ( ( ( A e. V /\ F : A --> CC /\ G : A --> ( CC \ { 0 } ) ) /\ x e. A ) -> ( ( G ` x ) e. CC /\ ( G ` x ) =/= 0 ) )
22 divrec 
 |-  ( ( ( F ` x ) e. CC /\ ( G ` x ) e. CC /\ ( G ` x ) =/= 0 ) -> ( ( F ` x ) / ( G ` x ) ) = ( ( F ` x ) x. ( 1 / ( G ` x ) ) ) )
23 22 eqcomd 
 |-  ( ( ( F ` x ) e. CC /\ ( G ` x ) e. CC /\ ( G ` x ) =/= 0 ) -> ( ( F ` x ) x. ( 1 / ( G ` x ) ) ) = ( ( F ` x ) / ( G ` x ) ) )
24 23 3expb 
 |-  ( ( ( F ` x ) e. CC /\ ( ( G ` x ) e. CC /\ ( G ` x ) =/= 0 ) ) -> ( ( F ` x ) x. ( 1 / ( G ` x ) ) ) = ( ( F ` x ) / ( G ` x ) ) )
25 17 21 24 syl2anc 
 |-  ( ( ( A e. V /\ F : A --> CC /\ G : A --> ( CC \ { 0 } ) ) /\ x e. A ) -> ( ( F ` x ) x. ( 1 / ( G ` x ) ) ) = ( ( F ` x ) / ( G ` x ) ) )
26 3 8 1 1 9 12 14 ofval 
 |-  ( ( ( A e. V /\ F : A --> CC /\ G : A --> ( CC \ { 0 } ) ) /\ x e. A ) -> ( ( F oF / G ) ` x ) = ( ( F ` x ) / ( G ` x ) ) )
27 25 26 eqtr4d 
 |-  ( ( ( A e. V /\ F : A --> CC /\ G : A --> ( CC \ { 0 } ) ) /\ x e. A ) -> ( ( F ` x ) x. ( 1 / ( G ` x ) ) ) = ( ( F oF / G ) ` x ) )
28 1 3 10 11 12 15 27 offveq 
 |-  ( ( A e. V /\ F : A --> CC /\ G : A --> ( CC \ { 0 } ) ) -> ( F oF x. ( ( A X. { 1 } ) oF / G ) ) = ( F oF / G ) )