Metamath Proof Explorer

Theorem ofdivdiv2

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

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

Proof

Step Hyp Ref Expression
1 simpll 
 |-  ( ( ( A e. V /\ F : A --> CC ) /\ ( G : A --> ( CC \ { 0 } ) /\ H : A --> ( CC \ { 0 } ) ) ) -> A e. V )
2 simplr 
 |-  ( ( ( A e. V /\ F : A --> CC ) /\ ( G : A --> ( CC \ { 0 } ) /\ H : A --> ( CC \ { 0 } ) ) ) -> F : A --> CC )
3 2 ffnd 
 |-  ( ( ( A e. V /\ F : A --> CC ) /\ ( G : A --> ( CC \ { 0 } ) /\ H : A --> ( CC \ { 0 } ) ) ) -> F Fn A )
4 simprl 
 |-  ( ( ( A e. V /\ F : A --> CC ) /\ ( G : A --> ( CC \ { 0 } ) /\ H : A --> ( CC \ { 0 } ) ) ) -> G : A --> ( CC \ { 0 } ) )
5 4 ffnd 
 |-  ( ( ( A e. V /\ F : A --> CC ) /\ ( G : A --> ( CC \ { 0 } ) /\ H : A --> ( CC \ { 0 } ) ) ) -> G Fn A )
6 simprr 
 |-  ( ( ( A e. V /\ F : A --> CC ) /\ ( G : A --> ( CC \ { 0 } ) /\ H : A --> ( CC \ { 0 } ) ) ) -> H : A --> ( CC \ { 0 } ) )
7 6 ffnd 
 |-  ( ( ( A e. V /\ F : A --> CC ) /\ ( G : A --> ( CC \ { 0 } ) /\ H : A --> ( CC \ { 0 } ) ) ) -> H Fn A )
8 inidm 
 |-  ( A i^i A ) = A
9 5 7 1 1 8 offn 
 |-  ( ( ( A e. V /\ F : A --> CC ) /\ ( G : A --> ( CC \ { 0 } ) /\ H : A --> ( CC \ { 0 } ) ) ) -> ( G oF / H ) Fn A )
10 3 7 1 1 8 offn 
 |-  ( ( ( A e. V /\ F : A --> CC ) /\ ( G : A --> ( CC \ { 0 } ) /\ H : A --> ( CC \ { 0 } ) ) ) -> ( F oF x. H ) Fn A )
11 10 5 1 1 8 offn 
 |-  ( ( ( A e. V /\ F : A --> CC ) /\ ( G : A --> ( CC \ { 0 } ) /\ H : A --> ( CC \ { 0 } ) ) ) -> ( ( F oF x. H ) oF / G ) Fn A )
12 eqidd 
 |-  ( ( ( ( A e. V /\ F : A --> CC ) /\ ( G : A --> ( CC \ { 0 } ) /\ H : A --> ( CC \ { 0 } ) ) ) /\ x e. A ) -> ( F ` x ) = ( F ` x ) )
13 eqidd 
 |-  ( ( ( ( A e. V /\ F : A --> CC ) /\ ( G : A --> ( CC \ { 0 } ) /\ H : A --> ( CC \ { 0 } ) ) ) /\ x e. A ) -> ( ( G oF / H ) ` x ) = ( ( G oF / H ) ` x ) )
14 ffvelrn 
 |-  ( ( F : A --> CC /\ x e. A ) -> ( F ` x ) e. CC )
15 2 14 sylan 
 |-  ( ( ( ( A e. V /\ F : A --> CC ) /\ ( G : A --> ( CC \ { 0 } ) /\ H : A --> ( CC \ { 0 } ) ) ) /\ x e. A ) -> ( F ` x ) e. CC )
16 ffvelrn 
 |-  ( ( G : A --> ( CC \ { 0 } ) /\ x e. A ) -> ( G ` x ) e. ( CC \ { 0 } ) )
17 eldifsn 
 |-  ( ( G ` x ) e. ( CC \ { 0 } ) <-> ( ( G ` x ) e. CC /\ ( G ` x ) =/= 0 ) )
18 16 17 sylib 
 |-  ( ( G : A --> ( CC \ { 0 } ) /\ x e. A ) -> ( ( G ` x ) e. CC /\ ( G ` x ) =/= 0 ) )
19 4 18 sylan 
 |-  ( ( ( ( A e. V /\ F : A --> CC ) /\ ( G : A --> ( CC \ { 0 } ) /\ H : A --> ( CC \ { 0 } ) ) ) /\ x e. A ) -> ( ( G ` x ) e. CC /\ ( G ` x ) =/= 0 ) )
20 ffvelrn 
 |-  ( ( H : A --> ( CC \ { 0 } ) /\ x e. A ) -> ( H ` x ) e. ( CC \ { 0 } ) )
21 eldifsn 
 |-  ( ( H ` x ) e. ( CC \ { 0 } ) <-> ( ( H ` x ) e. CC /\ ( H ` x ) =/= 0 ) )
22 20 21 sylib 
 |-  ( ( H : A --> ( CC \ { 0 } ) /\ x e. A ) -> ( ( H ` x ) e. CC /\ ( H ` x ) =/= 0 ) )
23 6 22 sylan 
 |-  ( ( ( ( A e. V /\ F : A --> CC ) /\ ( G : A --> ( CC \ { 0 } ) /\ H : A --> ( CC \ { 0 } ) ) ) /\ x e. A ) -> ( ( H ` x ) e. CC /\ ( H ` x ) =/= 0 ) )
24 divdiv2 
 |-  ( ( ( F ` x ) e. CC /\ ( ( G ` x ) e. CC /\ ( G ` x ) =/= 0 ) /\ ( ( H ` x ) e. CC /\ ( H ` x ) =/= 0 ) ) -> ( ( F ` x ) / ( ( G ` x ) / ( H ` x ) ) ) = ( ( ( F ` x ) x. ( H ` x ) ) / ( G ` x ) ) )
25 15 19 23 24 syl3anc 
 |-  ( ( ( ( A e. V /\ F : A --> CC ) /\ ( G : A --> ( CC \ { 0 } ) /\ H : A --> ( CC \ { 0 } ) ) ) /\ x e. A ) -> ( ( F ` x ) / ( ( G ` x ) / ( H ` x ) ) ) = ( ( ( F ` x ) x. ( H ` x ) ) / ( G ` x ) ) )
26 eqidd 
 |-  ( ( ( ( A e. V /\ F : A --> CC ) /\ ( G : A --> ( CC \ { 0 } ) /\ H : A --> ( CC \ { 0 } ) ) ) /\ x e. A ) -> ( G ` x ) = ( G ` x ) )
27 eqidd 
 |-  ( ( ( ( A e. V /\ F : A --> CC ) /\ ( G : A --> ( CC \ { 0 } ) /\ H : A --> ( CC \ { 0 } ) ) ) /\ x e. A ) -> ( H ` x ) = ( H ` x ) )
28 5 7 1 1 8 26 27 ofval 
 |-  ( ( ( ( A e. V /\ F : A --> CC ) /\ ( G : A --> ( CC \ { 0 } ) /\ H : A --> ( CC \ { 0 } ) ) ) /\ x e. A ) -> ( ( G oF / H ) ` x ) = ( ( G ` x ) / ( H ` x ) ) )
29 28 oveq2d 
 |-  ( ( ( ( A e. V /\ F : A --> CC ) /\ ( G : A --> ( CC \ { 0 } ) /\ H : A --> ( CC \ { 0 } ) ) ) /\ x e. A ) -> ( ( F ` x ) / ( ( G oF / H ) ` x ) ) = ( ( F ` x ) / ( ( G ` x ) / ( H ` x ) ) ) )
30 3 7 1 1 8 12 27 ofval 
 |-  ( ( ( ( A e. V /\ F : A --> CC ) /\ ( G : A --> ( CC \ { 0 } ) /\ H : A --> ( CC \ { 0 } ) ) ) /\ x e. A ) -> ( ( F oF x. H ) ` x ) = ( ( F ` x ) x. ( H ` x ) ) )
31 10 5 1 1 8 30 26 ofval 
 |-  ( ( ( ( A e. V /\ F : A --> CC ) /\ ( G : A --> ( CC \ { 0 } ) /\ H : A --> ( CC \ { 0 } ) ) ) /\ x e. A ) -> ( ( ( F oF x. H ) oF / G ) ` x ) = ( ( ( F ` x ) x. ( H ` x ) ) / ( G ` x ) ) )
32 25 29 31 3eqtr4d 
 |-  ( ( ( ( A e. V /\ F : A --> CC ) /\ ( G : A --> ( CC \ { 0 } ) /\ H : A --> ( CC \ { 0 } ) ) ) /\ x e. A ) -> ( ( F ` x ) / ( ( G oF / H ) ` x ) ) = ( ( ( F oF x. H ) oF / G ) ` x ) )
33 1 3 9 11 12 13 32 offveq 
 |-  ( ( ( A e. V /\ F : A --> CC ) /\ ( G : A --> ( CC \ { 0 } ) /\ H : A --> ( CC \ { 0 } ) ) ) -> ( F oF / ( G oF / H ) ) = ( ( F oF x. H ) oF / G ) )