Metamath Proof Explorer


Theorem inveq

Description: If there are two inverses of a morphism, these inverses are equal. Corollary 3.11 of Adamek p. 28. (Contributed by AV, 10-Apr-2020) (Revised by AV, 3-Jul-2022)

Ref Expression
Hypotheses inveq.b
|- B = ( Base ` C )
inveq.n
|- N = ( Inv ` C )
inveq.c
|- ( ph -> C e. Cat )
inveq.x
|- ( ph -> X e. B )
inveq.y
|- ( ph -> Y e. B )
Assertion inveq
|- ( ph -> ( ( F ( X N Y ) G /\ F ( X N Y ) K ) -> G = K ) )

Proof

Step Hyp Ref Expression
1 inveq.b
 |-  B = ( Base ` C )
2 inveq.n
 |-  N = ( Inv ` C )
3 inveq.c
 |-  ( ph -> C e. Cat )
4 inveq.x
 |-  ( ph -> X e. B )
5 inveq.y
 |-  ( ph -> Y e. B )
6 eqid
 |-  ( Sect ` C ) = ( Sect ` C )
7 3 adantr
 |-  ( ( ph /\ ( F ( X N Y ) G /\ F ( X N Y ) K ) ) -> C e. Cat )
8 5 adantr
 |-  ( ( ph /\ ( F ( X N Y ) G /\ F ( X N Y ) K ) ) -> Y e. B )
9 4 adantr
 |-  ( ( ph /\ ( F ( X N Y ) G /\ F ( X N Y ) K ) ) -> X e. B )
10 1 2 3 4 5 6 isinv
 |-  ( ph -> ( F ( X N Y ) G <-> ( F ( X ( Sect ` C ) Y ) G /\ G ( Y ( Sect ` C ) X ) F ) ) )
11 simpr
 |-  ( ( F ( X ( Sect ` C ) Y ) G /\ G ( Y ( Sect ` C ) X ) F ) -> G ( Y ( Sect ` C ) X ) F )
12 10 11 syl6bi
 |-  ( ph -> ( F ( X N Y ) G -> G ( Y ( Sect ` C ) X ) F ) )
13 12 com12
 |-  ( F ( X N Y ) G -> ( ph -> G ( Y ( Sect ` C ) X ) F ) )
14 13 adantr
 |-  ( ( F ( X N Y ) G /\ F ( X N Y ) K ) -> ( ph -> G ( Y ( Sect ` C ) X ) F ) )
15 14 impcom
 |-  ( ( ph /\ ( F ( X N Y ) G /\ F ( X N Y ) K ) ) -> G ( Y ( Sect ` C ) X ) F )
16 1 2 3 4 5 6 isinv
 |-  ( ph -> ( F ( X N Y ) K <-> ( F ( X ( Sect ` C ) Y ) K /\ K ( Y ( Sect ` C ) X ) F ) ) )
17 simpl
 |-  ( ( F ( X ( Sect ` C ) Y ) K /\ K ( Y ( Sect ` C ) X ) F ) -> F ( X ( Sect ` C ) Y ) K )
18 16 17 syl6bi
 |-  ( ph -> ( F ( X N Y ) K -> F ( X ( Sect ` C ) Y ) K ) )
19 18 adantld
 |-  ( ph -> ( ( F ( X N Y ) G /\ F ( X N Y ) K ) -> F ( X ( Sect ` C ) Y ) K ) )
20 19 imp
 |-  ( ( ph /\ ( F ( X N Y ) G /\ F ( X N Y ) K ) ) -> F ( X ( Sect ` C ) Y ) K )
21 1 6 7 8 9 15 20 sectcan
 |-  ( ( ph /\ ( F ( X N Y ) G /\ F ( X N Y ) K ) ) -> G = K )
22 21 ex
 |-  ( ph -> ( ( F ( X N Y ) G /\ F ( X N Y ) K ) -> G = K ) )