Metamath Proof Explorer

Theorem ofoprabco

Description: Function operation as a composition with an operation. (Contributed by Thierry Arnoux, 4-Jun-2017)

Ref Expression
Hypotheses ofoprabco.1 
|- F/_ a M
ofoprabco.2 
|- ( ph -> F : A --> B )
ofoprabco.3 
|- ( ph -> G : A --> C )
ofoprabco.4 
|- ( ph -> A e. V )
ofoprabco.5 
|- ( ph -> M = ( a e. A |-> <. ( F ` a ) , ( G ` a ) >. ) )
ofoprabco.6 
|- ( ph -> N = ( x e. B , y e. C |-> ( x R y ) ) )
Assertion ofoprabco 
|- ( ph -> ( F oF R G ) = ( N o. M ) )

Proof

Step Hyp Ref Expression
1 ofoprabco.1 
 |-  F/_ a M
2 ofoprabco.2 
 |-  ( ph -> F : A --> B )
3 ofoprabco.3 
 |-  ( ph -> G : A --> C )
4 ofoprabco.4 
 |-  ( ph -> A e. V )
5 ofoprabco.5 
 |-  ( ph -> M = ( a e. A |-> <. ( F ` a ) , ( G ` a ) >. ) )
6 ofoprabco.6 
 |-  ( ph -> N = ( x e. B , y e. C |-> ( x R y ) ) )
7 2 ffvelrnda 
 |-  ( ( ph /\ a e. A ) -> ( F ` a ) e. B )
8 3 ffvelrnda 
 |-  ( ( ph /\ a e. A ) -> ( G ` a ) e. C )
9 opelxpi 
 |-  ( ( ( F ` a ) e. B /\ ( G ` a ) e. C ) -> <. ( F ` a ) , ( G ` a ) >. e. ( B X. C ) )
10 7 8 9 syl2anc 
 |-  ( ( ph /\ a e. A ) -> <. ( F ` a ) , ( G ` a ) >. e. ( B X. C ) )
11 5 10 fvmpt2d 
 |-  ( ( ph /\ a e. A ) -> ( M ` a ) = <. ( F ` a ) , ( G ` a ) >. )
12 11 fveq2d 
 |-  ( ( ph /\ a e. A ) -> ( N ` ( M ` a ) ) = ( N ` <. ( F ` a ) , ( G ` a ) >. ) )
13 df-ov 
 |-  ( ( F ` a ) N ( G ` a ) ) = ( N ` <. ( F ` a ) , ( G ` a ) >. )
14 13 a1i 
 |-  ( ( ph /\ a e. A ) -> ( ( F ` a ) N ( G ` a ) ) = ( N ` <. ( F ` a ) , ( G ` a ) >. ) )
15 6 adantr 
 |-  ( ( ph /\ a e. A ) -> N = ( x e. B , y e. C |-> ( x R y ) ) )
16 simprl 
 |-  ( ( ( ph /\ a e. A ) /\ ( x = ( F ` a ) /\ y = ( G ` a ) ) ) -> x = ( F ` a ) )
17 simprr 
 |-  ( ( ( ph /\ a e. A ) /\ ( x = ( F ` a ) /\ y = ( G ` a ) ) ) -> y = ( G ` a ) )
18 16 17 oveq12d 
 |-  ( ( ( ph /\ a e. A ) /\ ( x = ( F ` a ) /\ y = ( G ` a ) ) ) -> ( x R y ) = ( ( F ` a ) R ( G ` a ) ) )
19 ovexd 
 |-  ( ( ph /\ a e. A ) -> ( ( F ` a ) R ( G ` a ) ) e. _V )
20 15 18 7 8 19 ovmpod 
 |-  ( ( ph /\ a e. A ) -> ( ( F ` a ) N ( G ` a ) ) = ( ( F ` a ) R ( G ` a ) ) )
21 12 14 20 3eqtr2d 
 |-  ( ( ph /\ a e. A ) -> ( N ` ( M ` a ) ) = ( ( F ` a ) R ( G ` a ) ) )
22 21 mpteq2dva 
 |-  ( ph -> ( a e. A |-> ( N ` ( M ` a ) ) ) = ( a e. A |-> ( ( F ` a ) R ( G ` a ) ) ) )
23 ovex 
 |-  ( x R y ) e. _V
24 23 rgen2w 
 |-  A. x e. B A. y e. C ( x R y ) e. _V
25 eqid 
 |-  ( x e. B , y e. C |-> ( x R y ) ) = ( x e. B , y e. C |-> ( x R y ) )
26 25 fmpo 
 |-  ( A. x e. B A. y e. C ( x R y ) e. _V <-> ( x e. B , y e. C |-> ( x R y ) ) : ( B X. C ) --> _V )
27 24 26 mpbi 
 |-  ( x e. B , y e. C |-> ( x R y ) ) : ( B X. C ) --> _V
28 6 feq1d 
 |-  ( ph -> ( N : ( B X. C ) --> _V <-> ( x e. B , y e. C |-> ( x R y ) ) : ( B X. C ) --> _V ) )
29 27 28 mpbiri 
 |-  ( ph -> N : ( B X. C ) --> _V )
30 5 10 fmpt3d 
 |-  ( ph -> M : A --> ( B X. C ) )
31 1 fcomptf 
 |-  ( ( N : ( B X. C ) --> _V /\ M : A --> ( B X. C ) ) -> ( N o. M ) = ( a e. A |-> ( N ` ( M ` a ) ) ) )
32 29 30 31 syl2anc 
 |-  ( ph -> ( N o. M ) = ( a e. A |-> ( N ` ( M ` a ) ) ) )
33 2 feqmptd 
 |-  ( ph -> F = ( a e. A |-> ( F ` a ) ) )
34 3 feqmptd 
 |-  ( ph -> G = ( a e. A |-> ( G ` a ) ) )
35 4 7 8 33 34 offval2 
 |-  ( ph -> ( F oF R G ) = ( a e. A |-> ( ( F ` a ) R ( G ` a ) ) ) )
36 22 32 35 3eqtr4rd 
 |-  ( ph -> ( F oF R G ) = ( N o. M ) )