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