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 φ C Cat
rcaninv.x φ X B
rcaninv.y φ Y B
rcaninv.z φ Z B
rcaninv.f φ F Y Iso C X
rcaninv.g φ G Y Hom C Z
rcaninv.h φ H Y Hom C Z
rcaninv.1 R = Y N X F
rcaninv.o No typesetting found for |- .o. = ( <. X , Y >. ( comp ` C ) Z ) with typecode |-
Assertion rcaninv Could not format assertion : No typesetting found for |- ( ph -> ( ( G .o. R ) = ( H .o. R ) -> G = H ) ) with typecode |-

Proof

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