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

Metamath Proof Explorer

Theorem upeu2lem

Description: Lemma for upeu2 . There exists a unique morphism from Y to Z that commutes if F : X --> Y is an isomorphism. (Contributed by Zhi Wang, 20-Sep-2025)

Ref Expression
Hypotheses upeu2lem.b 
|- B = ( Base ` C )
upeu2lem.h 
|- H = ( Hom ` C )
upeu2lem.o 
|- .x. = ( comp ` C )
upeu2lem.i 
|- I = ( Iso ` C )
upeu2lem.c 
|- ( ph -> C e. Cat )
upeu2lem.x 
|- ( ph -> X e. B )
upeu2lem.y 
|- ( ph -> Y e. B )
upeu2lem.z 
|- ( ph -> Z e. B )
upeu2lem.f 
|- ( ph -> F e. ( X I Y ) )
upeu2lem.g 
|- ( ph -> G e. ( X H Z ) )
Assertion upeu2lem 
|- ( ph -> E! k e. ( Y H Z ) G = ( k ( <. X , Y >. .x. Z ) F ) )

Proof

Step Hyp Ref Expression
1 upeu2lem.b 
 |-  B = ( Base ` C )
2 upeu2lem.h 
 |-  H = ( Hom ` C )
3 upeu2lem.o 
 |-  .x. = ( comp ` C )
4 upeu2lem.i 
 |-  I = ( Iso ` C )
5 upeu2lem.c 
 |-  ( ph -> C e. Cat )
6 upeu2lem.x 
 |-  ( ph -> X e. B )
7 upeu2lem.y 
 |-  ( ph -> Y e. B )
8 upeu2lem.z 
 |-  ( ph -> Z e. B )
9 upeu2lem.f 
 |-  ( ph -> F e. ( X I Y ) )
10 upeu2lem.g 
 |-  ( ph -> G e. ( X H Z ) )
11 1 2 4 5 7 6 isohom 
 |-  ( ph -> ( Y I X ) C_ ( Y H X ) )
12 eqid 
 |-  ( Inv ` C ) = ( Inv ` C )
13 1 12 5 6 7 4 invf 
 |-  ( ph -> ( X ( Inv ` C ) Y ) : ( X I Y ) --> ( Y I X ) )
14 13 9 ffvelcdmd 
 |-  ( ph -> ( ( X ( Inv ` C ) Y ) ` F ) e. ( Y I X ) )
15 11 14 sseldd 
 |-  ( ph -> ( ( X ( Inv ` C ) Y ) ` F ) e. ( Y H X ) )
16 1 2 3 5 7 6 8 15 10 catcocl 
 |-  ( ph -> ( G ( <. Y , X >. .x. Z ) ( ( X ( Inv ` C ) Y ) ` F ) ) e. ( Y H Z ) )
17 oveq1 
 |-  ( G = ( k ( <. X , Y >. .x. Z ) F ) -> ( G ( <. Y , X >. .x. Z ) ( ( X ( Inv ` C ) Y ) ` F ) ) = ( ( k ( <. X , Y >. .x. Z ) F ) ( <. Y , X >. .x. Z ) ( ( X ( Inv ` C ) Y ) ` F ) ) )
18 17 adantl 
 |-  ( ( ( ph /\ k e. ( Y H Z ) ) /\ G = ( k ( <. X , Y >. .x. Z ) F ) ) -> ( G ( <. Y , X >. .x. Z ) ( ( X ( Inv ` C ) Y ) ` F ) ) = ( ( k ( <. X , Y >. .x. Z ) F ) ( <. Y , X >. .x. Z ) ( ( X ( Inv ` C ) Y ) ` F ) ) )
19 5 adantr 
 |-  ( ( ph /\ k e. ( Y H Z ) ) -> C e. Cat )
20 7 adantr 
 |-  ( ( ph /\ k e. ( Y H Z ) ) -> Y e. B )
21 6 adantr 
 |-  ( ( ph /\ k e. ( Y H Z ) ) -> X e. B )
22 15 adantr 
 |-  ( ( ph /\ k e. ( Y H Z ) ) -> ( ( X ( Inv ` C ) Y ) ` F ) e. ( Y H X ) )
23 1 2 4 5 6 7 isohom 
 |-  ( ph -> ( X I Y ) C_ ( X H Y ) )
24 23 9 sseldd 
 |-  ( ph -> F e. ( X H Y ) )
25 24 adantr 
 |-  ( ( ph /\ k e. ( Y H Z ) ) -> F e. ( X H Y ) )
26 8 adantr 
 |-  ( ( ph /\ k e. ( Y H Z ) ) -> Z e. B )
27 simpr 
 |-  ( ( ph /\ k e. ( Y H Z ) ) -> k e. ( Y H Z ) )
28 1 2 3 19 20 21 20 22 25 26 27 catass 
 |-  ( ( ph /\ k e. ( Y H Z ) ) -> ( ( k ( <. X , Y >. .x. Z ) F ) ( <. Y , X >. .x. Z ) ( ( X ( Inv ` C ) Y ) ` F ) ) = ( k ( <. Y , Y >. .x. Z ) ( F ( <. Y , X >. .x. Y ) ( ( X ( Inv ` C ) Y ) ` F ) ) ) )
29 9 adantr 
 |-  ( ( ph /\ k e. ( Y H Z ) ) -> F e. ( X I Y ) )
30 eqid 
 |-  ( Id ` C ) = ( Id ` C )
31 3 oveqi 
 |-  ( <. Y , X >. .x. Y ) = ( <. Y , X >. ( comp ` C ) Y )
32 1 4 12 19 21 20 29 30 31 isocoinvid 
 |-  ( ( ph /\ k e. ( Y H Z ) ) -> ( F ( <. Y , X >. .x. Y ) ( ( X ( Inv ` C ) Y ) ` F ) ) = ( ( Id ` C ) ` Y ) )
33 32 oveq2d 
 |-  ( ( ph /\ k e. ( Y H Z ) ) -> ( k ( <. Y , Y >. .x. Z ) ( F ( <. Y , X >. .x. Y ) ( ( X ( Inv ` C ) Y ) ` F ) ) ) = ( k ( <. Y , Y >. .x. Z ) ( ( Id ` C ) ` Y ) ) )
34 1 2 30 19 20 3 26 27 catrid 
 |-  ( ( ph /\ k e. ( Y H Z ) ) -> ( k ( <. Y , Y >. .x. Z ) ( ( Id ` C ) ` Y ) ) = k )
35 28 33 34 3eqtrd 
 |-  ( ( ph /\ k e. ( Y H Z ) ) -> ( ( k ( <. X , Y >. .x. Z ) F ) ( <. Y , X >. .x. Z ) ( ( X ( Inv ` C ) Y ) ` F ) ) = k )
36 35 adantr 
 |-  ( ( ( ph /\ k e. ( Y H Z ) ) /\ G = ( k ( <. X , Y >. .x. Z ) F ) ) -> ( ( k ( <. X , Y >. .x. Z ) F ) ( <. Y , X >. .x. Z ) ( ( X ( Inv ` C ) Y ) ` F ) ) = k )
37 18 36 eqtr2d 
 |-  ( ( ( ph /\ k e. ( Y H Z ) ) /\ G = ( k ( <. X , Y >. .x. Z ) F ) ) -> k = ( G ( <. Y , X >. .x. Z ) ( ( X ( Inv ` C ) Y ) ` F ) ) )
38 oveq1 
 |-  ( k = ( G ( <. Y , X >. .x. Z ) ( ( X ( Inv ` C ) Y ) ` F ) ) -> ( k ( <. X , Y >. .x. Z ) F ) = ( ( G ( <. Y , X >. .x. Z ) ( ( X ( Inv ` C ) Y ) ` F ) ) ( <. X , Y >. .x. Z ) F ) )
39 38 adantl 
 |-  ( ( ( ph /\ k e. ( Y H Z ) ) /\ k = ( G ( <. Y , X >. .x. Z ) ( ( X ( Inv ` C ) Y ) ` F ) ) ) -> ( k ( <. X , Y >. .x. Z ) F ) = ( ( G ( <. Y , X >. .x. Z ) ( ( X ( Inv ` C ) Y ) ` F ) ) ( <. X , Y >. .x. Z ) F ) )
40 10 adantr 
 |-  ( ( ph /\ k e. ( Y H Z ) ) -> G e. ( X H Z ) )
41 1 2 3 19 21 20 21 25 22 26 40 catass 
 |-  ( ( ph /\ k e. ( Y H Z ) ) -> ( ( G ( <. Y , X >. .x. Z ) ( ( X ( Inv ` C ) Y ) ` F ) ) ( <. X , Y >. .x. Z ) F ) = ( G ( <. X , X >. .x. Z ) ( ( ( X ( Inv ` C ) Y ) ` F ) ( <. X , Y >. .x. X ) F ) ) )
42 3 oveqi 
 |-  ( <. X , Y >. .x. X ) = ( <. X , Y >. ( comp ` C ) X )
43 1 4 12 19 21 20 29 30 42 invcoisoid 
 |-  ( ( ph /\ k e. ( Y H Z ) ) -> ( ( ( X ( Inv ` C ) Y ) ` F ) ( <. X , Y >. .x. X ) F ) = ( ( Id ` C ) ` X ) )
44 43 oveq2d 
 |-  ( ( ph /\ k e. ( Y H Z ) ) -> ( G ( <. X , X >. .x. Z ) ( ( ( X ( Inv ` C ) Y ) ` F ) ( <. X , Y >. .x. X ) F ) ) = ( G ( <. X , X >. .x. Z ) ( ( Id ` C ) ` X ) ) )
45 1 2 30 19 21 3 26 40 catrid 
 |-  ( ( ph /\ k e. ( Y H Z ) ) -> ( G ( <. X , X >. .x. Z ) ( ( Id ` C ) ` X ) ) = G )
46 41 44 45 3eqtrd 
 |-  ( ( ph /\ k e. ( Y H Z ) ) -> ( ( G ( <. Y , X >. .x. Z ) ( ( X ( Inv ` C ) Y ) ` F ) ) ( <. X , Y >. .x. Z ) F ) = G )
47 46 adantr 
 |-  ( ( ( ph /\ k e. ( Y H Z ) ) /\ k = ( G ( <. Y , X >. .x. Z ) ( ( X ( Inv ` C ) Y ) ` F ) ) ) -> ( ( G ( <. Y , X >. .x. Z ) ( ( X ( Inv ` C ) Y ) ` F ) ) ( <. X , Y >. .x. Z ) F ) = G )
48 39 47 eqtr2d 
 |-  ( ( ( ph /\ k e. ( Y H Z ) ) /\ k = ( G ( <. Y , X >. .x. Z ) ( ( X ( Inv ` C ) Y ) ` F ) ) ) -> G = ( k ( <. X , Y >. .x. Z ) F ) )
49 37 48 impbida 
 |-  ( ( ph /\ k e. ( Y H Z ) ) -> ( G = ( k ( <. X , Y >. .x. Z ) F ) <-> k = ( G ( <. Y , X >. .x. Z ) ( ( X ( Inv ` C ) Y ) ` F ) ) ) )
50 49 ralrimiva 
 |-  ( ph -> A. k e. ( Y H Z ) ( G = ( k ( <. X , Y >. .x. Z ) F ) <-> k = ( G ( <. Y , X >. .x. Z ) ( ( X ( Inv ` C ) Y ) ` F ) ) ) )
51 reu6i 
 |-  ( ( ( G ( <. Y , X >. .x. Z ) ( ( X ( Inv ` C ) Y ) ` F ) ) e. ( Y H Z ) /\ A. k e. ( Y H Z ) ( G = ( k ( <. X , Y >. .x. Z ) F ) <-> k = ( G ( <. Y , X >. .x. Z ) ( ( X ( Inv ` C ) Y ) ` F ) ) ) ) -> E! k e. ( Y H Z ) G = ( k ( <. X , Y >. .x. Z ) F ) )
52 16 50 51 syl2anc 
 |-  ( ph -> E! k e. ( Y H Z ) G = ( k ( <. X , Y >. .x. Z ) F ) )