Metamath Proof Explorer


Theorem isocoinvid

Description: The inverse of an isomorphism composed with the isomorphism is the identity. (Contributed by AV, 10-Apr-2020)

Ref Expression
Hypotheses invisoinv.b B = Base C
invisoinv.i I = Iso C
invisoinv.n N = Inv C
invisoinv.c φ C Cat
invisoinv.x φ X B
invisoinv.y φ Y B
invisoinv.f φ F X I Y
invcoisoid.1 1 ˙ = Id C
isocoinvid.o No typesetting found for |- .o. = ( <. Y , X >. ( comp ` C ) Y ) with typecode |-
Assertion isocoinvid Could not format assertion : No typesetting found for |- ( ph -> ( F .o. ( ( X N Y ) ` F ) ) = ( .1. ` Y ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 invisoinv.b B = Base C
2 invisoinv.i I = Iso C
3 invisoinv.n N = Inv C
4 invisoinv.c φ C Cat
5 invisoinv.x φ X B
6 invisoinv.y φ Y B
7 invisoinv.f φ F X I Y
8 invcoisoid.1 1 ˙ = Id C
9 isocoinvid.o Could not format .o. = ( <. Y , X >. ( comp ` C ) Y ) : No typesetting found for |- .o. = ( <. Y , X >. ( comp ` C ) Y ) with typecode |-
10 1 2 3 4 5 6 7 invisoinvl φ X N Y F Y N X F
11 eqid Sect C = Sect C
12 1 3 4 6 5 11 isinv φ X N Y F Y N X F X N Y F Y Sect C X F F X Sect C Y X N Y F
13 simpl X N Y F Y Sect C X F F X Sect C Y X N Y F X N Y F Y Sect C X F
14 12 13 syl6bi φ X N Y F Y N X F X N Y F Y Sect C X F
15 10 14 mpd φ X N Y F Y Sect C X F
16 eqid Hom C = Hom C
17 eqid comp C = comp C
18 1 16 2 4 6 5 isohom φ Y I X Y Hom C X
19 1 3 4 5 6 2 invf φ X N Y : X I Y Y I X
20 19 7 ffvelrnd φ X N Y F Y I X
21 18 20 sseldd φ X N Y F Y Hom C X
22 1 16 2 4 5 6 isohom φ X I Y X Hom C Y
23 22 7 sseldd φ F X Hom C Y
24 1 16 17 8 11 4 6 5 21 23 issect2 φ X N Y F Y Sect C X F F Y X comp C Y X N Y F = 1 ˙ Y
25 9 a1i Could not format ( ph -> .o. = ( <. Y , X >. ( comp ` C ) Y ) ) : No typesetting found for |- ( ph -> .o. = ( <. Y , X >. ( comp ` C ) Y ) ) with typecode |-
26 25 eqcomd Could not format ( ph -> ( <. Y , X >. ( comp ` C ) Y ) = .o. ) : No typesetting found for |- ( ph -> ( <. Y , X >. ( comp ` C ) Y ) = .o. ) with typecode |-
27 26 oveqd Could not format ( ph -> ( F ( <. Y , X >. ( comp ` C ) Y ) ( ( X N Y ) ` F ) ) = ( F .o. ( ( X N Y ) ` F ) ) ) : No typesetting found for |- ( ph -> ( F ( <. Y , X >. ( comp ` C ) Y ) ( ( X N Y ) ` F ) ) = ( F .o. ( ( X N Y ) ` F ) ) ) with typecode |-
28 27 eqeq1d Could not format ( ph -> ( ( F ( <. Y , X >. ( comp ` C ) Y ) ( ( X N Y ) ` F ) ) = ( .1. ` Y ) <-> ( F .o. ( ( X N Y ) ` F ) ) = ( .1. ` Y ) ) ) : No typesetting found for |- ( ph -> ( ( F ( <. Y , X >. ( comp ` C ) Y ) ( ( X N Y ) ` F ) ) = ( .1. ` Y ) <-> ( F .o. ( ( X N Y ) ` F ) ) = ( .1. ` Y ) ) ) with typecode |-
29 24 28 bitrd Could not format ( ph -> ( ( ( X N Y ) ` F ) ( Y ( Sect ` C ) X ) F <-> ( F .o. ( ( X N Y ) ` F ) ) = ( .1. ` Y ) ) ) : No typesetting found for |- ( ph -> ( ( ( X N Y ) ` F ) ( Y ( Sect ` C ) X ) F <-> ( F .o. ( ( X N Y ) ` F ) ) = ( .1. ` Y ) ) ) with typecode |-
30 15 29 mpbid Could not format ( ph -> ( F .o. ( ( X N Y ) ` F ) ) = ( .1. ` Y ) ) : No typesetting found for |- ( ph -> ( F .o. ( ( X N Y ) ` F ) ) = ( .1. ` Y ) ) with typecode |-