Metamath Proof Explorer

Theorem ofmul12

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

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

Proof

Step Hyp Ref Expression
1 simpll 
 |-  ( ( ( A e. V /\ F : A --> CC ) /\ ( G : A --> CC /\ H : A --> CC ) ) -> A e. V )
2 simplr 
 |-  ( ( ( A e. V /\ F : A --> CC ) /\ ( G : A --> CC /\ H : A --> CC ) ) -> F : A --> CC )
3 2 ffnd 
 |-  ( ( ( A e. V /\ F : A --> CC ) /\ ( G : A --> CC /\ H : A --> CC ) ) -> F Fn A )
4 simprl 
 |-  ( ( ( A e. V /\ F : A --> CC ) /\ ( G : A --> CC /\ H : A --> CC ) ) -> G : A --> CC )
5 4 ffnd 
 |-  ( ( ( A e. V /\ F : A --> CC ) /\ ( G : A --> CC /\ H : A --> CC ) ) -> G Fn A )
6 simprr 
 |-  ( ( ( A e. V /\ F : A --> CC ) /\ ( G : A --> CC /\ H : A --> CC ) ) -> H : A --> CC )
7 6 ffnd 
 |-  ( ( ( A e. V /\ F : A --> CC ) /\ ( G : A --> CC /\ H : A --> CC ) ) -> 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 /\ H : A --> CC ) ) -> ( G oF x. H ) Fn A )
10 3 7 1 1 8 offn 
 |-  ( ( ( A e. V /\ F : A --> CC ) /\ ( G : A --> CC /\ H : A --> CC ) ) -> ( F oF x. H ) Fn A )
11 5 10 1 1 8 offn 
 |-  ( ( ( A e. V /\ F : A --> CC ) /\ ( G : A --> CC /\ H : A --> CC ) ) -> ( G oF x. ( F oF x. H ) ) Fn A )
12 eqidd 
 |-  ( ( ( ( A e. V /\ F : A --> CC ) /\ ( G : A --> CC /\ H : A --> CC ) ) /\ x e. A ) -> ( F ` x ) = ( F ` x ) )
13 eqidd 
 |-  ( ( ( ( A e. V /\ F : A --> CC ) /\ ( G : A --> CC /\ H : A --> CC ) ) /\ x e. A ) -> ( G ` x ) = ( G ` x ) )
14 eqidd 
 |-  ( ( ( ( A e. V /\ F : A --> CC ) /\ ( G : A --> CC /\ H : A --> CC ) ) /\ x e. A ) -> ( H ` x ) = ( H ` x ) )
15 5 7 1 1 8 13 14 ofval 
 |-  ( ( ( ( A e. V /\ F : A --> CC ) /\ ( G : A --> CC /\ H : A --> CC ) ) /\ x e. A ) -> ( ( G oF x. H ) ` x ) = ( ( G ` x ) x. ( H ` x ) ) )
16 2 ffvelrnda 
 |-  ( ( ( ( A e. V /\ F : A --> CC ) /\ ( G : A --> CC /\ H : A --> CC ) ) /\ x e. A ) -> ( F ` x ) e. CC )
17 4 ffvelrnda 
 |-  ( ( ( ( A e. V /\ F : A --> CC ) /\ ( G : A --> CC /\ H : A --> CC ) ) /\ x e. A ) -> ( G ` x ) e. CC )
18 6 ffvelrnda 
 |-  ( ( ( ( A e. V /\ F : A --> CC ) /\ ( G : A --> CC /\ H : A --> CC ) ) /\ x e. A ) -> ( H ` x ) e. CC )
19 16 17 18 mul12d 
 |-  ( ( ( ( A e. V /\ F : A --> CC ) /\ ( G : A --> CC /\ H : A --> CC ) ) /\ x e. A ) -> ( ( F ` x ) x. ( ( G ` x ) x. ( H ` x ) ) ) = ( ( G ` x ) x. ( ( F ` x ) x. ( H ` x ) ) ) )
20 3 7 1 1 8 12 14 ofval 
 |-  ( ( ( ( A e. V /\ F : A --> CC ) /\ ( G : A --> CC /\ H : A --> CC ) ) /\ x e. A ) -> ( ( F oF x. H ) ` x ) = ( ( F ` x ) x. ( H ` x ) ) )
21 5 10 1 1 8 13 20 ofval 
 |-  ( ( ( ( A e. V /\ F : A --> CC ) /\ ( G : A --> CC /\ H : A --> CC ) ) /\ x e. A ) -> ( ( G oF x. ( F oF x. H ) ) ` x ) = ( ( G ` x ) x. ( ( F ` x ) x. ( H ` x ) ) ) )
22 19 21 eqtr4d 
 |-  ( ( ( ( A e. V /\ F : A --> CC ) /\ ( G : A --> CC /\ H : A --> CC ) ) /\ x e. A ) -> ( ( F ` x ) x. ( ( G ` x ) x. ( H ` x ) ) ) = ( ( G oF x. ( F oF x. H ) ) ` x ) )
23 1 3 9 11 12 15 22 offveq 
 |-  ( ( ( A e. V /\ F : A --> CC ) /\ ( G : A --> CC /\ H : A --> CC ) ) -> ( F oF x. ( G oF x. H ) ) = ( G oF x. ( F oF x. H ) ) )