This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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