Step |
Hyp |
Ref |
Expression |
1 |
|
rcaninv.b |
|- B = ( Base ` C ) |
2 |
|
rcaninv.n |
|- N = ( Inv ` C ) |
3 |
|
rcaninv.c |
|- ( ph -> C e. Cat ) |
4 |
|
rcaninv.x |
|- ( ph -> X e. B ) |
5 |
|
rcaninv.y |
|- ( ph -> Y e. B ) |
6 |
|
rcaninv.z |
|- ( ph -> Z e. B ) |
7 |
|
rcaninv.f |
|- ( ph -> F e. ( Y ( Iso ` C ) X ) ) |
8 |
|
rcaninv.g |
|- ( ph -> G e. ( Y ( Hom ` C ) Z ) ) |
9 |
|
rcaninv.h |
|- ( ph -> H e. ( Y ( Hom ` C ) Z ) ) |
10 |
|
rcaninv.1 |
|- R = ( ( Y N X ) ` F ) |
11 |
|
rcaninv.o |
|- .o. = ( <. X , Y >. ( comp ` C ) Z ) |
12 |
|
eqid |
|- ( Hom ` C ) = ( Hom ` C ) |
13 |
|
eqid |
|- ( comp ` C ) = ( comp ` C ) |
14 |
|
eqid |
|- ( Iso ` C ) = ( Iso ` C ) |
15 |
1 12 14 3 5 4
|
isohom |
|- ( ph -> ( Y ( Iso ` C ) X ) C_ ( Y ( Hom ` C ) X ) ) |
16 |
15 7
|
sseldd |
|- ( ph -> F e. ( Y ( Hom ` C ) X ) ) |
17 |
1 12 14 3 4 5
|
isohom |
|- ( ph -> ( X ( Iso ` C ) Y ) C_ ( X ( Hom ` C ) Y ) ) |
18 |
1 2 3 5 4 14
|
invf |
|- ( ph -> ( Y N X ) : ( Y ( Iso ` C ) X ) --> ( X ( Iso ` C ) Y ) ) |
19 |
18 7
|
ffvelrnd |
|- ( ph -> ( ( Y N X ) ` F ) e. ( X ( Iso ` C ) Y ) ) |
20 |
17 19
|
sseldd |
|- ( ph -> ( ( Y N X ) ` F ) e. ( X ( Hom ` C ) Y ) ) |
21 |
1 12 13 3 5 4 5 16 20 6 8
|
catass |
|- ( ph -> ( ( G ( <. X , Y >. ( comp ` C ) Z ) ( ( Y N X ) ` F ) ) ( <. Y , X >. ( comp ` C ) Z ) F ) = ( G ( <. Y , Y >. ( comp ` C ) Z ) ( ( ( Y N X ) ` F ) ( <. Y , X >. ( comp ` C ) Y ) F ) ) ) |
22 |
|
eqid |
|- ( Id ` C ) = ( Id ` C ) |
23 |
|
eqid |
|- ( <. Y , X >. ( comp ` C ) Y ) = ( <. Y , X >. ( comp ` C ) Y ) |
24 |
1 14 2 3 5 4 7 22 23
|
invcoisoid |
|- ( ph -> ( ( ( Y N X ) ` F ) ( <. Y , X >. ( comp ` C ) Y ) F ) = ( ( Id ` C ) ` Y ) ) |
25 |
24
|
eqcomd |
|- ( ph -> ( ( Id ` C ) ` Y ) = ( ( ( Y N X ) ` F ) ( <. Y , X >. ( comp ` C ) Y ) F ) ) |
26 |
25
|
oveq2d |
|- ( ph -> ( G ( <. Y , Y >. ( comp ` C ) Z ) ( ( Id ` C ) ` Y ) ) = ( G ( <. Y , Y >. ( comp ` C ) Z ) ( ( ( Y N X ) ` F ) ( <. Y , X >. ( comp ` C ) Y ) F ) ) ) |
27 |
1 12 22 3 5 13 6 8
|
catrid |
|- ( ph -> ( G ( <. Y , Y >. ( comp ` C ) Z ) ( ( Id ` C ) ` Y ) ) = G ) |
28 |
21 26 27
|
3eqtr2rd |
|- ( ph -> G = ( ( G ( <. X , Y >. ( comp ` C ) Z ) ( ( Y N X ) ` F ) ) ( <. Y , X >. ( comp ` C ) Z ) F ) ) |
29 |
28
|
adantr |
|- ( ( ph /\ ( G .o. R ) = ( H .o. R ) ) -> G = ( ( G ( <. X , Y >. ( comp ` C ) Z ) ( ( Y N X ) ` F ) ) ( <. Y , X >. ( comp ` C ) Z ) F ) ) |
30 |
11
|
eqcomi |
|- ( <. X , Y >. ( comp ` C ) Z ) = .o. |
31 |
30
|
a1i |
|- ( ph -> ( <. X , Y >. ( comp ` C ) Z ) = .o. ) |
32 |
|
eqidd |
|- ( ph -> G = G ) |
33 |
10
|
eqcomi |
|- ( ( Y N X ) ` F ) = R |
34 |
33
|
a1i |
|- ( ph -> ( ( Y N X ) ` F ) = R ) |
35 |
31 32 34
|
oveq123d |
|- ( ph -> ( G ( <. X , Y >. ( comp ` C ) Z ) ( ( Y N X ) ` F ) ) = ( G .o. R ) ) |
36 |
35
|
adantr |
|- ( ( ph /\ ( G .o. R ) = ( H .o. R ) ) -> ( G ( <. X , Y >. ( comp ` C ) Z ) ( ( Y N X ) ` F ) ) = ( G .o. R ) ) |
37 |
|
simpr |
|- ( ( ph /\ ( G .o. R ) = ( H .o. R ) ) -> ( G .o. R ) = ( H .o. R ) ) |
38 |
36 37
|
eqtrd |
|- ( ( ph /\ ( G .o. R ) = ( H .o. R ) ) -> ( G ( <. X , Y >. ( comp ` C ) Z ) ( ( Y N X ) ` F ) ) = ( H .o. R ) ) |
39 |
38
|
oveq1d |
|- ( ( ph /\ ( G .o. R ) = ( H .o. R ) ) -> ( ( G ( <. X , Y >. ( comp ` C ) Z ) ( ( Y N X ) ` F ) ) ( <. Y , X >. ( comp ` C ) Z ) F ) = ( ( H .o. R ) ( <. Y , X >. ( comp ` C ) Z ) F ) ) |
40 |
11
|
oveqi |
|- ( H .o. R ) = ( H ( <. X , Y >. ( comp ` C ) Z ) R ) |
41 |
40
|
oveq1i |
|- ( ( H .o. R ) ( <. Y , X >. ( comp ` C ) Z ) F ) = ( ( H ( <. X , Y >. ( comp ` C ) Z ) R ) ( <. Y , X >. ( comp ` C ) Z ) F ) |
42 |
41
|
a1i |
|- ( ph -> ( ( H .o. R ) ( <. Y , X >. ( comp ` C ) Z ) F ) = ( ( H ( <. X , Y >. ( comp ` C ) Z ) R ) ( <. Y , X >. ( comp ` C ) Z ) F ) ) |
43 |
10 20
|
eqeltrid |
|- ( ph -> R e. ( X ( Hom ` C ) Y ) ) |
44 |
1 12 13 3 5 4 5 16 43 6 9
|
catass |
|- ( ph -> ( ( H ( <. X , Y >. ( comp ` C ) Z ) R ) ( <. Y , X >. ( comp ` C ) Z ) F ) = ( H ( <. Y , Y >. ( comp ` C ) Z ) ( R ( <. Y , X >. ( comp ` C ) Y ) F ) ) ) |
45 |
10
|
oveq1i |
|- ( R ( <. Y , X >. ( comp ` C ) Y ) F ) = ( ( ( Y N X ) ` F ) ( <. Y , X >. ( comp ` C ) Y ) F ) |
46 |
45
|
oveq2i |
|- ( H ( <. Y , Y >. ( comp ` C ) Z ) ( R ( <. Y , X >. ( comp ` C ) Y ) F ) ) = ( H ( <. Y , Y >. ( comp ` C ) Z ) ( ( ( Y N X ) ` F ) ( <. Y , X >. ( comp ` C ) Y ) F ) ) |
47 |
46
|
a1i |
|- ( ph -> ( H ( <. Y , Y >. ( comp ` C ) Z ) ( R ( <. Y , X >. ( comp ` C ) Y ) F ) ) = ( H ( <. Y , Y >. ( comp ` C ) Z ) ( ( ( Y N X ) ` F ) ( <. Y , X >. ( comp ` C ) Y ) F ) ) ) |
48 |
24
|
oveq2d |
|- ( ph -> ( H ( <. Y , Y >. ( comp ` C ) Z ) ( ( ( Y N X ) ` F ) ( <. Y , X >. ( comp ` C ) Y ) F ) ) = ( H ( <. Y , Y >. ( comp ` C ) Z ) ( ( Id ` C ) ` Y ) ) ) |
49 |
44 47 48
|
3eqtrd |
|- ( ph -> ( ( H ( <. X , Y >. ( comp ` C ) Z ) R ) ( <. Y , X >. ( comp ` C ) Z ) F ) = ( H ( <. Y , Y >. ( comp ` C ) Z ) ( ( Id ` C ) ` Y ) ) ) |
50 |
1 12 22 3 5 13 6 9
|
catrid |
|- ( ph -> ( H ( <. Y , Y >. ( comp ` C ) Z ) ( ( Id ` C ) ` Y ) ) = H ) |
51 |
42 49 50
|
3eqtrd |
|- ( ph -> ( ( H .o. R ) ( <. Y , X >. ( comp ` C ) Z ) F ) = H ) |
52 |
51
|
adantr |
|- ( ( ph /\ ( G .o. R ) = ( H .o. R ) ) -> ( ( H .o. R ) ( <. Y , X >. ( comp ` C ) Z ) F ) = H ) |
53 |
29 39 52
|
3eqtrd |
|- ( ( ph /\ ( G .o. R ) = ( H .o. R ) ) -> G = H ) |
54 |
53
|
ex |
|- ( ph -> ( ( G .o. R ) = ( H .o. R ) -> G = H ) ) |