Step |
Hyp |
Ref |
Expression |
1 |
|
elinel2 |
|- ( x e. ( ( dom F i^i dom G ) i^i D ) -> x e. D ) |
2 |
|
fvres |
|- ( x e. D -> ( ( F |` D ) ` x ) = ( F ` x ) ) |
3 |
|
fvres |
|- ( x e. D -> ( ( G |` D ) ` x ) = ( G ` x ) ) |
4 |
2 3
|
oveq12d |
|- ( x e. D -> ( ( ( F |` D ) ` x ) R ( ( G |` D ) ` x ) ) = ( ( F ` x ) R ( G ` x ) ) ) |
5 |
1 4
|
syl |
|- ( x e. ( ( dom F i^i dom G ) i^i D ) -> ( ( ( F |` D ) ` x ) R ( ( G |` D ) ` x ) ) = ( ( F ` x ) R ( G ` x ) ) ) |
6 |
5
|
mpteq2ia |
|- ( x e. ( ( dom F i^i dom G ) i^i D ) |-> ( ( ( F |` D ) ` x ) R ( ( G |` D ) ` x ) ) ) = ( x e. ( ( dom F i^i dom G ) i^i D ) |-> ( ( F ` x ) R ( G ` x ) ) ) |
7 |
|
inindi |
|- ( D i^i ( dom F i^i dom G ) ) = ( ( D i^i dom F ) i^i ( D i^i dom G ) ) |
8 |
|
incom |
|- ( ( dom F i^i dom G ) i^i D ) = ( D i^i ( dom F i^i dom G ) ) |
9 |
|
dmres |
|- dom ( F |` D ) = ( D i^i dom F ) |
10 |
|
dmres |
|- dom ( G |` D ) = ( D i^i dom G ) |
11 |
9 10
|
ineq12i |
|- ( dom ( F |` D ) i^i dom ( G |` D ) ) = ( ( D i^i dom F ) i^i ( D i^i dom G ) ) |
12 |
7 8 11
|
3eqtr4ri |
|- ( dom ( F |` D ) i^i dom ( G |` D ) ) = ( ( dom F i^i dom G ) i^i D ) |
13 |
12
|
mpteq1i |
|- ( x e. ( dom ( F |` D ) i^i dom ( G |` D ) ) |-> ( ( ( F |` D ) ` x ) R ( ( G |` D ) ` x ) ) ) = ( x e. ( ( dom F i^i dom G ) i^i D ) |-> ( ( ( F |` D ) ` x ) R ( ( G |` D ) ` x ) ) ) |
14 |
|
resmpt3 |
|- ( ( x e. ( dom F i^i dom G ) |-> ( ( F ` x ) R ( G ` x ) ) ) |` D ) = ( x e. ( ( dom F i^i dom G ) i^i D ) |-> ( ( F ` x ) R ( G ` x ) ) ) |
15 |
6 13 14
|
3eqtr4ri |
|- ( ( x e. ( dom F i^i dom G ) |-> ( ( F ` x ) R ( G ` x ) ) ) |` D ) = ( x e. ( dom ( F |` D ) i^i dom ( G |` D ) ) |-> ( ( ( F |` D ) ` x ) R ( ( G |` D ) ` x ) ) ) |
16 |
|
offval3 |
|- ( ( F e. V /\ G e. W ) -> ( F oF R G ) = ( x e. ( dom F i^i dom G ) |-> ( ( F ` x ) R ( G ` x ) ) ) ) |
17 |
16
|
reseq1d |
|- ( ( F e. V /\ G e. W ) -> ( ( F oF R G ) |` D ) = ( ( x e. ( dom F i^i dom G ) |-> ( ( F ` x ) R ( G ` x ) ) ) |` D ) ) |
18 |
|
resexg |
|- ( F e. V -> ( F |` D ) e. _V ) |
19 |
|
resexg |
|- ( G e. W -> ( G |` D ) e. _V ) |
20 |
|
offval3 |
|- ( ( ( F |` D ) e. _V /\ ( G |` D ) e. _V ) -> ( ( F |` D ) oF R ( G |` D ) ) = ( x e. ( dom ( F |` D ) i^i dom ( G |` D ) ) |-> ( ( ( F |` D ) ` x ) R ( ( G |` D ) ` x ) ) ) ) |
21 |
18 19 20
|
syl2an |
|- ( ( F e. V /\ G e. W ) -> ( ( F |` D ) oF R ( G |` D ) ) = ( x e. ( dom ( F |` D ) i^i dom ( G |` D ) ) |-> ( ( ( F |` D ) ` x ) R ( ( G |` D ) ` x ) ) ) ) |
22 |
15 17 21
|
3eqtr4a |
|- ( ( F e. V /\ G e. W ) -> ( ( F oF R G ) |` D ) = ( ( F |` D ) oF R ( G |` D ) ) ) |