| Step |
Hyp |
Ref |
Expression |
| 1 |
|
comfeqval.b |
|- B = ( Base ` C ) |
| 2 |
|
comfeqval.h |
|- H = ( Hom ` C ) |
| 3 |
|
comfeqval.1 |
|- .x. = ( comp ` C ) |
| 4 |
|
comfeqval.2 |
|- .xb = ( comp ` D ) |
| 5 |
|
comfeqval.3 |
|- ( ph -> ( Homf ` C ) = ( Homf ` D ) ) |
| 6 |
|
comfeqval.4 |
|- ( ph -> ( comf ` C ) = ( comf ` D ) ) |
| 7 |
|
comfeqval.x |
|- ( ph -> X e. B ) |
| 8 |
|
comfeqval.y |
|- ( ph -> Y e. B ) |
| 9 |
|
comfeqval.z |
|- ( ph -> Z e. B ) |
| 10 |
|
comfeqval.f |
|- ( ph -> F e. ( X H Y ) ) |
| 11 |
|
comfeqval.g |
|- ( ph -> G e. ( Y H Z ) ) |
| 12 |
6
|
oveqd |
|- ( ph -> ( <. X , Y >. ( comf ` C ) Z ) = ( <. X , Y >. ( comf ` D ) Z ) ) |
| 13 |
12
|
oveqd |
|- ( ph -> ( G ( <. X , Y >. ( comf ` C ) Z ) F ) = ( G ( <. X , Y >. ( comf ` D ) Z ) F ) ) |
| 14 |
|
eqid |
|- ( comf ` C ) = ( comf ` C ) |
| 15 |
14 1 2 3 7 8 9 10 11
|
comfval |
|- ( ph -> ( G ( <. X , Y >. ( comf ` C ) Z ) F ) = ( G ( <. X , Y >. .x. Z ) F ) ) |
| 16 |
|
eqid |
|- ( comf ` D ) = ( comf ` D ) |
| 17 |
|
eqid |
|- ( Base ` D ) = ( Base ` D ) |
| 18 |
|
eqid |
|- ( Hom ` D ) = ( Hom ` D ) |
| 19 |
5
|
homfeqbas |
|- ( ph -> ( Base ` C ) = ( Base ` D ) ) |
| 20 |
1 19
|
eqtrid |
|- ( ph -> B = ( Base ` D ) ) |
| 21 |
7 20
|
eleqtrd |
|- ( ph -> X e. ( Base ` D ) ) |
| 22 |
8 20
|
eleqtrd |
|- ( ph -> Y e. ( Base ` D ) ) |
| 23 |
9 20
|
eleqtrd |
|- ( ph -> Z e. ( Base ` D ) ) |
| 24 |
1 2 18 5 7 8
|
homfeqval |
|- ( ph -> ( X H Y ) = ( X ( Hom ` D ) Y ) ) |
| 25 |
10 24
|
eleqtrd |
|- ( ph -> F e. ( X ( Hom ` D ) Y ) ) |
| 26 |
1 2 18 5 8 9
|
homfeqval |
|- ( ph -> ( Y H Z ) = ( Y ( Hom ` D ) Z ) ) |
| 27 |
11 26
|
eleqtrd |
|- ( ph -> G e. ( Y ( Hom ` D ) Z ) ) |
| 28 |
16 17 18 4 21 22 23 25 27
|
comfval |
|- ( ph -> ( G ( <. X , Y >. ( comf ` D ) Z ) F ) = ( G ( <. X , Y >. .xb Z ) F ) ) |
| 29 |
13 15 28
|
3eqtr3d |
|- ( ph -> ( G ( <. X , Y >. .x. Z ) F ) = ( G ( <. X , Y >. .xb Z ) F ) ) |