Metamath Proof Explorer

Theorem ofdivcan4

Description: Function analogue of divcan4 . (Contributed by Steve Rodriguez, 4-Nov-2015)

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

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 simp3 
 |-  ( ( A e. V /\ F : A --> CC /\ G : A --> ( CC \ { 0 } ) ) -> G : A --> ( CC \ { 0 } ) )
5 4 ffnd 
 |-  ( ( A e. V /\ F : A --> CC /\ G : A --> ( CC \ { 0 } ) ) -> G Fn A )
6 inidm 
 |-  ( A i^i A ) = A
7 3 5 1 1 6 offn 
 |-  ( ( A e. V /\ F : A --> CC /\ G : A --> ( CC \ { 0 } ) ) -> ( F oF x. G ) Fn A )
8 eqidd 
 |-  ( ( ( A e. V /\ F : A --> CC /\ G : A --> ( CC \ { 0 } ) ) /\ x e. A ) -> ( F ` x ) = ( F ` x ) )
9 eqidd 
 |-  ( ( ( A e. V /\ F : A --> CC /\ G : A --> ( CC \ { 0 } ) ) /\ x e. A ) -> ( G ` x ) = ( G ` x ) )
10 3 5 1 1 6 8 9 ofval 
 |-  ( ( ( A e. V /\ F : A --> CC /\ G : A --> ( CC \ { 0 } ) ) /\ x e. A ) -> ( ( F oF x. G ) ` x ) = ( ( F ` x ) x. ( G ` x ) ) )
11 ffvelrn 
 |-  ( ( F : A --> CC /\ x e. A ) -> ( F ` x ) e. CC )
12 2 11 sylan 
 |-  ( ( ( A e. V /\ F : A --> CC /\ G : A --> ( CC \ { 0 } ) ) /\ x e. A ) -> ( F ` x ) e. CC )
13 ffvelrn 
 |-  ( ( G : A --> ( CC \ { 0 } ) /\ x e. A ) -> ( G ` x ) e. ( CC \ { 0 } ) )
14 eldifsn 
 |-  ( ( G ` x ) e. ( CC \ { 0 } ) <-> ( ( G ` x ) e. CC /\ ( G ` x ) =/= 0 ) )
15 13 14 sylib 
 |-  ( ( G : A --> ( CC \ { 0 } ) /\ x e. A ) -> ( ( G ` x ) e. CC /\ ( G ` x ) =/= 0 ) )
16 4 15 sylan 
 |-  ( ( ( A e. V /\ F : A --> CC /\ G : A --> ( CC \ { 0 } ) ) /\ x e. A ) -> ( ( G ` x ) e. CC /\ ( G ` x ) =/= 0 ) )
17 divcan4 
 |-  ( ( ( F ` x ) e. CC /\ ( G ` x ) e. CC /\ ( G ` x ) =/= 0 ) -> ( ( ( F ` x ) x. ( G ` x ) ) / ( G ` x ) ) = ( F ` x ) )
18 17 3expb 
 |-  ( ( ( F ` x ) e. CC /\ ( ( G ` x ) e. CC /\ ( G ` x ) =/= 0 ) ) -> ( ( ( F ` x ) x. ( G ` x ) ) / ( G ` x ) ) = ( F ` x ) )
19 12 16 18 syl2anc 
 |-  ( ( ( A e. V /\ F : A --> CC /\ G : A --> ( CC \ { 0 } ) ) /\ x e. A ) -> ( ( ( F ` x ) x. ( G ` x ) ) / ( G ` x ) ) = ( F ` x ) )
20 1 7 5 3 10 9 19 offveq 
 |-  ( ( A e. V /\ F : A --> CC /\ G : A --> ( CC \ { 0 } ) ) -> ( ( F oF x. G ) oF / G ) = F )