Step |
Hyp |
Ref |
Expression |
1 |
|
cofuass.g |
|- ( ph -> G e. ( C Func D ) ) |
2 |
|
cofuass.h |
|- ( ph -> H e. ( D Func E ) ) |
3 |
|
cofuass.k |
|- ( ph -> K e. ( E Func F ) ) |
4 |
|
coass |
|- ( ( ( 1st ` K ) o. ( 1st ` H ) ) o. ( 1st ` G ) ) = ( ( 1st ` K ) o. ( ( 1st ` H ) o. ( 1st ` G ) ) ) |
5 |
|
eqid |
|- ( Base ` D ) = ( Base ` D ) |
6 |
5 2 3
|
cofu1st |
|- ( ph -> ( 1st ` ( K o.func H ) ) = ( ( 1st ` K ) o. ( 1st ` H ) ) ) |
7 |
6
|
coeq1d |
|- ( ph -> ( ( 1st ` ( K o.func H ) ) o. ( 1st ` G ) ) = ( ( ( 1st ` K ) o. ( 1st ` H ) ) o. ( 1st ` G ) ) ) |
8 |
|
eqid |
|- ( Base ` C ) = ( Base ` C ) |
9 |
8 1 2
|
cofu1st |
|- ( ph -> ( 1st ` ( H o.func G ) ) = ( ( 1st ` H ) o. ( 1st ` G ) ) ) |
10 |
9
|
coeq2d |
|- ( ph -> ( ( 1st ` K ) o. ( 1st ` ( H o.func G ) ) ) = ( ( 1st ` K ) o. ( ( 1st ` H ) o. ( 1st ` G ) ) ) ) |
11 |
4 7 10
|
3eqtr4a |
|- ( ph -> ( ( 1st ` ( K o.func H ) ) o. ( 1st ` G ) ) = ( ( 1st ` K ) o. ( 1st ` ( H o.func G ) ) ) ) |
12 |
|
coass |
|- ( ( ( ( ( 1st ` H ) ` ( ( 1st ` G ) ` x ) ) ( 2nd ` K ) ( ( 1st ` H ) ` ( ( 1st ` G ) ` y ) ) ) o. ( ( ( 1st ` G ) ` x ) ( 2nd ` H ) ( ( 1st ` G ) ` y ) ) ) o. ( x ( 2nd ` G ) y ) ) = ( ( ( ( 1st ` H ) ` ( ( 1st ` G ) ` x ) ) ( 2nd ` K ) ( ( 1st ` H ) ` ( ( 1st ` G ) ` y ) ) ) o. ( ( ( ( 1st ` G ) ` x ) ( 2nd ` H ) ( ( 1st ` G ) ` y ) ) o. ( x ( 2nd ` G ) y ) ) ) |
13 |
2
|
3ad2ant1 |
|- ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> H e. ( D Func E ) ) |
14 |
3
|
3ad2ant1 |
|- ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> K e. ( E Func F ) ) |
15 |
|
relfunc |
|- Rel ( C Func D ) |
16 |
|
1st2ndbr |
|- ( ( Rel ( C Func D ) /\ G e. ( C Func D ) ) -> ( 1st ` G ) ( C Func D ) ( 2nd ` G ) ) |
17 |
15 1 16
|
sylancr |
|- ( ph -> ( 1st ` G ) ( C Func D ) ( 2nd ` G ) ) |
18 |
17
|
3ad2ant1 |
|- ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> ( 1st ` G ) ( C Func D ) ( 2nd ` G ) ) |
19 |
8 5 18
|
funcf1 |
|- ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> ( 1st ` G ) : ( Base ` C ) --> ( Base ` D ) ) |
20 |
|
simp2 |
|- ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> x e. ( Base ` C ) ) |
21 |
19 20
|
ffvelrnd |
|- ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> ( ( 1st ` G ) ` x ) e. ( Base ` D ) ) |
22 |
|
simp3 |
|- ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> y e. ( Base ` C ) ) |
23 |
19 22
|
ffvelrnd |
|- ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> ( ( 1st ` G ) ` y ) e. ( Base ` D ) ) |
24 |
5 13 14 21 23
|
cofu2nd |
|- ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> ( ( ( 1st ` G ) ` x ) ( 2nd ` ( K o.func H ) ) ( ( 1st ` G ) ` y ) ) = ( ( ( ( 1st ` H ) ` ( ( 1st ` G ) ` x ) ) ( 2nd ` K ) ( ( 1st ` H ) ` ( ( 1st ` G ) ` y ) ) ) o. ( ( ( 1st ` G ) ` x ) ( 2nd ` H ) ( ( 1st ` G ) ` y ) ) ) ) |
25 |
24
|
coeq1d |
|- ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> ( ( ( ( 1st ` G ) ` x ) ( 2nd ` ( K o.func H ) ) ( ( 1st ` G ) ` y ) ) o. ( x ( 2nd ` G ) y ) ) = ( ( ( ( ( 1st ` H ) ` ( ( 1st ` G ) ` x ) ) ( 2nd ` K ) ( ( 1st ` H ) ` ( ( 1st ` G ) ` y ) ) ) o. ( ( ( 1st ` G ) ` x ) ( 2nd ` H ) ( ( 1st ` G ) ` y ) ) ) o. ( x ( 2nd ` G ) y ) ) ) |
26 |
1
|
3ad2ant1 |
|- ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> G e. ( C Func D ) ) |
27 |
8 26 13 20
|
cofu1 |
|- ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> ( ( 1st ` ( H o.func G ) ) ` x ) = ( ( 1st ` H ) ` ( ( 1st ` G ) ` x ) ) ) |
28 |
8 26 13 22
|
cofu1 |
|- ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> ( ( 1st ` ( H o.func G ) ) ` y ) = ( ( 1st ` H ) ` ( ( 1st ` G ) ` y ) ) ) |
29 |
27 28
|
oveq12d |
|- ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> ( ( ( 1st ` ( H o.func G ) ) ` x ) ( 2nd ` K ) ( ( 1st ` ( H o.func G ) ) ` y ) ) = ( ( ( 1st ` H ) ` ( ( 1st ` G ) ` x ) ) ( 2nd ` K ) ( ( 1st ` H ) ` ( ( 1st ` G ) ` y ) ) ) ) |
30 |
8 26 13 20 22
|
cofu2nd |
|- ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> ( x ( 2nd ` ( H o.func G ) ) y ) = ( ( ( ( 1st ` G ) ` x ) ( 2nd ` H ) ( ( 1st ` G ) ` y ) ) o. ( x ( 2nd ` G ) y ) ) ) |
31 |
29 30
|
coeq12d |
|- ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> ( ( ( ( 1st ` ( H o.func G ) ) ` x ) ( 2nd ` K ) ( ( 1st ` ( H o.func G ) ) ` y ) ) o. ( x ( 2nd ` ( H o.func G ) ) y ) ) = ( ( ( ( 1st ` H ) ` ( ( 1st ` G ) ` x ) ) ( 2nd ` K ) ( ( 1st ` H ) ` ( ( 1st ` G ) ` y ) ) ) o. ( ( ( ( 1st ` G ) ` x ) ( 2nd ` H ) ( ( 1st ` G ) ` y ) ) o. ( x ( 2nd ` G ) y ) ) ) ) |
32 |
12 25 31
|
3eqtr4a |
|- ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> ( ( ( ( 1st ` G ) ` x ) ( 2nd ` ( K o.func H ) ) ( ( 1st ` G ) ` y ) ) o. ( x ( 2nd ` G ) y ) ) = ( ( ( ( 1st ` ( H o.func G ) ) ` x ) ( 2nd ` K ) ( ( 1st ` ( H o.func G ) ) ` y ) ) o. ( x ( 2nd ` ( H o.func G ) ) y ) ) ) |
33 |
32
|
mpoeq3dva |
|- ( ph -> ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( ( ( 1st ` G ) ` x ) ( 2nd ` ( K o.func H ) ) ( ( 1st ` G ) ` y ) ) o. ( x ( 2nd ` G ) y ) ) ) = ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( ( ( 1st ` ( H o.func G ) ) ` x ) ( 2nd ` K ) ( ( 1st ` ( H o.func G ) ) ` y ) ) o. ( x ( 2nd ` ( H o.func G ) ) y ) ) ) ) |
34 |
11 33
|
opeq12d |
|- ( ph -> <. ( ( 1st ` ( K o.func H ) ) o. ( 1st ` G ) ) , ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( ( ( 1st ` G ) ` x ) ( 2nd ` ( K o.func H ) ) ( ( 1st ` G ) ` y ) ) o. ( x ( 2nd ` G ) y ) ) ) >. = <. ( ( 1st ` K ) o. ( 1st ` ( H o.func G ) ) ) , ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( ( ( 1st ` ( H o.func G ) ) ` x ) ( 2nd ` K ) ( ( 1st ` ( H o.func G ) ) ` y ) ) o. ( x ( 2nd ` ( H o.func G ) ) y ) ) ) >. ) |
35 |
2 3
|
cofucl |
|- ( ph -> ( K o.func H ) e. ( D Func F ) ) |
36 |
8 1 35
|
cofuval |
|- ( ph -> ( ( K o.func H ) o.func G ) = <. ( ( 1st ` ( K o.func H ) ) o. ( 1st ` G ) ) , ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( ( ( 1st ` G ) ` x ) ( 2nd ` ( K o.func H ) ) ( ( 1st ` G ) ` y ) ) o. ( x ( 2nd ` G ) y ) ) ) >. ) |
37 |
1 2
|
cofucl |
|- ( ph -> ( H o.func G ) e. ( C Func E ) ) |
38 |
8 37 3
|
cofuval |
|- ( ph -> ( K o.func ( H o.func G ) ) = <. ( ( 1st ` K ) o. ( 1st ` ( H o.func G ) ) ) , ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( ( ( 1st ` ( H o.func G ) ) ` x ) ( 2nd ` K ) ( ( 1st ` ( H o.func G ) ) ` y ) ) o. ( x ( 2nd ` ( H o.func G ) ) y ) ) ) >. ) |
39 |
34 36 38
|
3eqtr4d |
|- ( ph -> ( ( K o.func H ) o.func G ) = ( K o.func ( H o.func G ) ) ) |