Metamath Proof Explorer

Theorem rcaninv

Description: Right cancellation of an inverse of an isomorphism. (Contributed by AV, 5-Apr-2020)

Ref Expression
Hypotheses rcaninv.b 
|- B = ( Base ` C )
rcaninv.n 
|- N = ( Inv ` C )
rcaninv.c 
|- ( ph -> C e. Cat )
rcaninv.x 
|- ( ph -> X e. B )
rcaninv.y 
|- ( ph -> Y e. B )
rcaninv.z 
|- ( ph -> Z e. B )
rcaninv.f 
|- ( ph -> F e. ( Y ( Iso ` C ) X ) )
rcaninv.g 
|- ( ph -> G e. ( Y ( Hom ` C ) Z ) )
rcaninv.h 
|- ( ph -> H e. ( Y ( Hom ` C ) Z ) )
rcaninv.1 
|- R = ( ( Y N X ) ` F )
rcaninv.o 
|- .o. = ( <. X , Y >. ( comp ` C ) Z )
Assertion rcaninv 
|- ( ph -> ( ( G .o. R ) = ( H .o. R ) -> G = H ) )

Proof

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 ) )