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 ⊢ 𝐵 = ( Base ‘ 𝐶 )
upeu2lem.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
upeu2lem.o ⊢ · = ( comp ‘ 𝐶 )
upeu2lem.i ⊢ 𝐼 = ( Iso ‘ 𝐶 )
upeu2lem.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
upeu2lem.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
upeu2lem.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
upeu2lem.z ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
upeu2lem.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) )
upeu2lem.g ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑋 𝐻 𝑍 ) )
Assertion upeu2lem ( 𝜑 → ∃! 𝑘 ∈ ( 𝑌 𝐻 𝑍 ) 𝐺 = ( 𝑘 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) )

Proof

Step Hyp Ref Expression
1 upeu2lem.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
2 upeu2lem.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
3 upeu2lem.o ⊢ · = ( comp ‘ 𝐶 )
4 upeu2lem.i ⊢ 𝐼 = ( Iso ‘ 𝐶 )
5 upeu2lem.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
6 upeu2lem.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
7 upeu2lem.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
8 upeu2lem.z ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
9 upeu2lem.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) )
10 upeu2lem.g ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑋 𝐻 𝑍 ) )
11 1 2 4 5 7 6 isohom ⊢ ( 𝜑 → ( 𝑌 𝐼 𝑋 ) ⊆ ( 𝑌 𝐻 𝑋 ) )
12 eqid ⊢ ( Inv ‘ 𝐶 ) = ( Inv ‘ 𝐶 )
13 1 12 5 6 7 4 invf ⊢ ( 𝜑 → ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) : ( 𝑋 𝐼 𝑌 ) ⟶ ( 𝑌 𝐼 𝑋 ) )
14 13 9 ffvelcdmd ⊢ ( 𝜑 → ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ∈ ( 𝑌 𝐼 𝑋 ) )
15 11 14 sseldd ⊢ ( 𝜑 → ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ∈ ( 𝑌 𝐻 𝑋 ) )
16 1 2 3 5 7 6 8 15 10 catcocl ⊢ ( 𝜑 → ( 𝐺 ( ⟨ 𝑌 , 𝑋 ⟩ · 𝑍 ) ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) ∈ ( 𝑌 𝐻 𝑍 ) )
17 oveq1 ⊢ ( 𝐺 = ( 𝑘 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) → ( 𝐺 ( ⟨ 𝑌 , 𝑋 ⟩ · 𝑍 ) ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) = ( ( 𝑘 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ( ⟨ 𝑌 , 𝑋 ⟩ · 𝑍 ) ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) )
18 17 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑌 𝐻 𝑍 ) ) ∧ 𝐺 = ( 𝑘 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ) → ( 𝐺 ( ⟨ 𝑌 , 𝑋 ⟩ · 𝑍 ) ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) = ( ( 𝑘 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ( ⟨ 𝑌 , 𝑋 ⟩ · 𝑍 ) ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) )
19 5 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑌 𝐻 𝑍 ) ) → 𝐶 ∈ Cat )
20 7 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑌 𝐻 𝑍 ) ) → 𝑌 ∈ 𝐵 )
21 6 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑌 𝐻 𝑍 ) ) → 𝑋 ∈ 𝐵 )
22 15 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑌 𝐻 𝑍 ) ) → ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ∈ ( 𝑌 𝐻 𝑋 ) )
23 1 2 4 5 6 7 isohom ⊢ ( 𝜑 → ( 𝑋 𝐼 𝑌 ) ⊆ ( 𝑋 𝐻 𝑌 ) )
24 23 9 sseldd ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
25 24 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑌 𝐻 𝑍 ) ) → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
26 8 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑌 𝐻 𝑍 ) ) → 𝑍 ∈ 𝐵 )
27 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑌 𝐻 𝑍 ) ) → 𝑘 ∈ ( 𝑌 𝐻 𝑍 ) )
28 1 2 3 19 20 21 20 22 25 26 27 catass ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑌 𝐻 𝑍 ) ) → ( ( 𝑘 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ( ⟨ 𝑌 , 𝑋 ⟩ · 𝑍 ) ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) = ( 𝑘 ( ⟨ 𝑌 , 𝑌 ⟩ · 𝑍 ) ( 𝐹 ( ⟨ 𝑌 , 𝑋 ⟩ · 𝑌 ) ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) ) )
29 9 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑌 𝐻 𝑍 ) ) → 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) )
30 eqid ⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
31 3 oveqi ⊢ ( ⟨ 𝑌 , 𝑋 ⟩ · 𝑌 ) = ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 )
32 1 4 12 19 21 20 29 30 31 isocoinvid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑌 𝐻 𝑍 ) ) → ( 𝐹 ( ⟨ 𝑌 , 𝑋 ⟩ · 𝑌 ) ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) = ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) )
33 32 oveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑌 𝐻 𝑍 ) ) → ( 𝑘 ( ⟨ 𝑌 , 𝑌 ⟩ · 𝑍 ) ( 𝐹 ( ⟨ 𝑌 , 𝑋 ⟩ · 𝑌 ) ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) ) = ( 𝑘 ( ⟨ 𝑌 , 𝑌 ⟩ · 𝑍 ) ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ) )
34 1 2 30 19 20 3 26 27 catrid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑌 𝐻 𝑍 ) ) → ( 𝑘 ( ⟨ 𝑌 , 𝑌 ⟩ · 𝑍 ) ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ) = 𝑘 )
35 28 33 34 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑌 𝐻 𝑍 ) ) → ( ( 𝑘 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ( ⟨ 𝑌 , 𝑋 ⟩ · 𝑍 ) ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) = 𝑘 )
36 35 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑌 𝐻 𝑍 ) ) ∧ 𝐺 = ( 𝑘 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ) → ( ( 𝑘 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ( ⟨ 𝑌 , 𝑋 ⟩ · 𝑍 ) ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) = 𝑘 )
37 18 36 eqtr2d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑌 𝐻 𝑍 ) ) ∧ 𝐺 = ( 𝑘 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ) → 𝑘 = ( 𝐺 ( ⟨ 𝑌 , 𝑋 ⟩ · 𝑍 ) ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) )
38 oveq1 ⊢ ( 𝑘 = ( 𝐺 ( ⟨ 𝑌 , 𝑋 ⟩ · 𝑍 ) ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) → ( 𝑘 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) = ( ( 𝐺 ( ⟨ 𝑌 , 𝑋 ⟩ · 𝑍 ) ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) )
39 38 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑌 𝐻 𝑍 ) ) ∧ 𝑘 = ( 𝐺 ( ⟨ 𝑌 , 𝑋 ⟩ · 𝑍 ) ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) ) → ( 𝑘 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) = ( ( 𝐺 ( ⟨ 𝑌 , 𝑋 ⟩ · 𝑍 ) ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) )
40 10 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑌 𝐻 𝑍 ) ) → 𝐺 ∈ ( 𝑋 𝐻 𝑍 ) )
41 1 2 3 19 21 20 21 25 22 26 40 catass ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑌 𝐻 𝑍 ) ) → ( ( 𝐺 ( ⟨ 𝑌 , 𝑋 ⟩ · 𝑍 ) ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) = ( 𝐺 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑍 ) ( ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑋 ) 𝐹 ) ) )
42 3 oveqi ⊢ ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑋 ) = ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 )
43 1 4 12 19 21 20 29 30 42 invcoisoid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑌 𝐻 𝑍 ) ) → ( ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) )
44 43 oveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑌 𝐻 𝑍 ) ) → ( 𝐺 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑍 ) ( ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑋 ) 𝐹 ) ) = ( 𝐺 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑍 ) ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) )
45 1 2 30 19 21 3 26 40 catrid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑌 𝐻 𝑍 ) ) → ( 𝐺 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑍 ) ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) = 𝐺 )
46 41 44 45 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑌 𝐻 𝑍 ) ) → ( ( 𝐺 ( ⟨ 𝑌 , 𝑋 ⟩ · 𝑍 ) ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) = 𝐺 )
47 46 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑌 𝐻 𝑍 ) ) ∧ 𝑘 = ( 𝐺 ( ⟨ 𝑌 , 𝑋 ⟩ · 𝑍 ) ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) ) → ( ( 𝐺 ( ⟨ 𝑌 , 𝑋 ⟩ · 𝑍 ) ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) = 𝐺 )
48 39 47 eqtr2d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑌 𝐻 𝑍 ) ) ∧ 𝑘 = ( 𝐺 ( ⟨ 𝑌 , 𝑋 ⟩ · 𝑍 ) ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) ) → 𝐺 = ( 𝑘 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) )
49 37 48 impbida ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑌 𝐻 𝑍 ) ) → ( 𝐺 = ( 𝑘 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ↔ 𝑘 = ( 𝐺 ( ⟨ 𝑌 , 𝑋 ⟩ · 𝑍 ) ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) ) )
50 49 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 𝑌 𝐻 𝑍 ) ( 𝐺 = ( 𝑘 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ↔ 𝑘 = ( 𝐺 ( ⟨ 𝑌 , 𝑋 ⟩ · 𝑍 ) ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) ) )
51 reu6i ⊢ ( ( ( 𝐺 ( ⟨ 𝑌 , 𝑋 ⟩ · 𝑍 ) ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) ∈ ( 𝑌 𝐻 𝑍 ) ∧ ∀ 𝑘 ∈ ( 𝑌 𝐻 𝑍 ) ( 𝐺 = ( 𝑘 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ↔ 𝑘 = ( 𝐺 ( ⟨ 𝑌 , 𝑋 ⟩ · 𝑍 ) ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) ) ) → ∃! 𝑘 ∈ ( 𝑌 𝐻 𝑍 ) 𝐺 = ( 𝑘 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) )
52 16 50 51 syl2anc ⊢ ( 𝜑 → ∃! 𝑘 ∈ ( 𝑌 𝐻 𝑍 ) 𝐺 = ( 𝑘 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) )