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	$⊢ \underset{˙}{\cdot} = comp (C)$
	upeu2lem.i	$⊢ I = Iso (C)$
	upeu2lem.c	$⊢ φ \to C \in Cat$
	upeu2lem.x	$⊢ φ \to X \in B$
	upeu2lem.y	$⊢ φ \to Y \in B$
	upeu2lem.z	$⊢ φ \to Z \in B$
	upeu2lem.f	$⊢ φ \to F \in (X I Y)$
	upeu2lem.g	$⊢ φ \to G \in (X H Z)$
Assertion	upeu2lem	$⊢ φ \to \exists! k \in (Y H Z) G = k (⟨X, Y⟩ \underset{˙}{\cdot} Z) F$

Proof

Step	Hyp	Ref	Expression
1		upeu2lem.b	$⊢ B = {Base}_{C}$
2		upeu2lem.h	$⊢ H = Hom (C)$
3		upeu2lem.o	$⊢ \underset{˙}{\cdot} = comp (C)$
4		upeu2lem.i	$⊢ I = Iso (C)$
5		upeu2lem.c	$⊢ φ \to C \in Cat$
6		upeu2lem.x	$⊢ φ \to X \in B$
7		upeu2lem.y	$⊢ φ \to Y \in B$
8		upeu2lem.z	$⊢ φ \to Z \in B$
9		upeu2lem.f	$⊢ φ \to F \in (X I Y)$
10		upeu2lem.g	$⊢ φ \to G \in (X H Z)$
11	1 2 4 5 7 6	isohom	$⊢ φ \to Y I X \subseteq Y H X$
12		eqid	$⊢ Inv (C) = Inv (C)$
13	1 12 5 6 7 4	invf	$⊢ φ \to (X Inv (C) Y) : X I Y ⟶ Y I X$
14	13 9	ffvelcdmd	$⊢ φ \to (X Inv (C) Y) (F) \in (Y I X)$
15	11 14	sseldd	$⊢ φ \to (X Inv (C) Y) (F) \in (Y H X)$
16	1 2 3 5 7 6 8 15 10	catcocl	$⊢ φ \to G (⟨Y, X⟩ \underset{˙}{\cdot} Z) (X Inv (C) Y) (F) \in (Y H Z)$
17		oveq1	$⊢ G = k (⟨X, Y⟩ \underset{˙}{\cdot} Z) F \to G (⟨Y, X⟩ \underset{˙}{\cdot} Z) (X Inv (C) Y) (F) = (k (⟨X, Y⟩ \underset{˙}{\cdot} Z) F) (⟨Y, X⟩ \underset{˙}{\cdot} Z) (X Inv (C) Y) (F)$
18	17	adantl	$⊢ ((φ \land k \in (Y H Z)) \land G = k (⟨X, Y⟩ \underset{˙}{\cdot} Z) F) \to G (⟨Y, X⟩ \underset{˙}{\cdot} Z) (X Inv (C) Y) (F) = (k (⟨X, Y⟩ \underset{˙}{\cdot} Z) F) (⟨Y, X⟩ \underset{˙}{\cdot} Z) (X Inv (C) Y) (F)$
19	5	adantr	$⊢ (φ \land k \in (Y H Z)) \to C \in Cat$
20	7	adantr	$⊢ (φ \land k \in (Y H Z)) \to Y \in B$
21	6	adantr	$⊢ (φ \land k \in (Y H Z)) \to X \in B$
22	15	adantr	$⊢ (φ \land k \in (Y H Z)) \to (X Inv (C) Y) (F) \in (Y H X)$
23	1 2 4 5 6 7	isohom	$⊢ φ \to X I Y \subseteq X H Y$
24	23 9	sseldd	$⊢ φ \to F \in (X H Y)$
25	24	adantr	$⊢ (φ \land k \in (Y H Z)) \to F \in (X H Y)$
26	8	adantr	$⊢ (φ \land k \in (Y H Z)) \to Z \in B$
27		simpr	$⊢ (φ \land k \in (Y H Z)) \to k \in (Y H Z)$
28	1 2 3 19 20 21 20 22 25 26 27	catass	$⊢ (φ \land k \in (Y H Z)) \to (k (⟨X, Y⟩ \underset{˙}{\cdot} Z) F) (⟨Y, X⟩ \underset{˙}{\cdot} Z) (X Inv (C) Y) (F) = k (⟨Y, Y⟩ \underset{˙}{\cdot} Z) (F (⟨Y, X⟩ \underset{˙}{\cdot} Y) (X Inv (C) Y) (F))$
29	9	adantr	$⊢ (φ \land k \in (Y H Z)) \to F \in (X I Y)$
30		eqid	$⊢ Id (C) = Id (C)$
31	3	oveqi	$⊢ ⟨Y, X⟩ \underset{˙}{\cdot} Y = ⟨Y, X⟩ comp (C) Y$
32	1 4 12 19 21 20 29 30 31	isocoinvid	$⊢ (φ \land k \in (Y H Z)) \to F (⟨Y, X⟩ \underset{˙}{\cdot} Y) (X Inv (C) Y) (F) = Id (C) (Y)$
33	32	oveq2d	$⊢ (φ \land k \in (Y H Z)) \to k (⟨Y, Y⟩ \underset{˙}{\cdot} Z) (F (⟨Y, X⟩ \underset{˙}{\cdot} Y) (X Inv (C) Y) (F)) = k (⟨Y, Y⟩ \underset{˙}{\cdot} Z) Id (C) (Y)$
34	1 2 30 19 20 3 26 27	catrid	$⊢ (φ \land k \in (Y H Z)) \to k (⟨Y, Y⟩ \underset{˙}{\cdot} Z) Id (C) (Y) = k$
35	28 33 34	3eqtrd	$⊢ (φ \land k \in (Y H Z)) \to (k (⟨X, Y⟩ \underset{˙}{\cdot} Z) F) (⟨Y, X⟩ \underset{˙}{\cdot} Z) (X Inv (C) Y) (F) = k$
36	35	adantr	$⊢ ((φ \land k \in (Y H Z)) \land G = k (⟨X, Y⟩ \underset{˙}{\cdot} Z) F) \to (k (⟨X, Y⟩ \underset{˙}{\cdot} Z) F) (⟨Y, X⟩ \underset{˙}{\cdot} Z) (X Inv (C) Y) (F) = k$
37	18 36	eqtr2d	$⊢ ((φ \land k \in (Y H Z)) \land G = k (⟨X, Y⟩ \underset{˙}{\cdot} Z) F) \to k = G (⟨Y, X⟩ \underset{˙}{\cdot} Z) (X Inv (C) Y) (F)$
38		oveq1	$⊢ k = G (⟨Y, X⟩ \underset{˙}{\cdot} Z) (X Inv (C) Y) (F) \to k (⟨X, Y⟩ \underset{˙}{\cdot} Z) F = (G (⟨Y, X⟩ \underset{˙}{\cdot} Z) (X Inv (C) Y) (F)) (⟨X, Y⟩ \underset{˙}{\cdot} Z) F$
39	38	adantl	$⊢ ((φ \land k \in (Y H Z)) \land k = G (⟨Y, X⟩ \underset{˙}{\cdot} Z) (X Inv (C) Y) (F)) \to k (⟨X, Y⟩ \underset{˙}{\cdot} Z) F = (G (⟨Y, X⟩ \underset{˙}{\cdot} Z) (X Inv (C) Y) (F)) (⟨X, Y⟩ \underset{˙}{\cdot} Z) F$
40	10	adantr	$⊢ (φ \land k \in (Y H Z)) \to G \in (X H Z)$
41	1 2 3 19 21 20 21 25 22 26 40	catass	$⊢ (φ \land k \in (Y H Z)) \to (G (⟨Y, X⟩ \underset{˙}{\cdot} Z) (X Inv (C) Y) (F)) (⟨X, Y⟩ \underset{˙}{\cdot} Z) F = G (⟨X, X⟩ \underset{˙}{\cdot} Z) ((X Inv (C) Y) (F) (⟨X, Y⟩ \underset{˙}{\cdot} X) F)$
42	3	oveqi	$⊢ ⟨X, Y⟩ \underset{˙}{\cdot} X = ⟨X, Y⟩ comp (C) X$
43	1 4 12 19 21 20 29 30 42	invcoisoid	$⊢ (φ \land k \in (Y H Z)) \to (X Inv (C) Y) (F) (⟨X, Y⟩ \underset{˙}{\cdot} X) F = Id (C) (X)$
44	43	oveq2d	$⊢ (φ \land k \in (Y H Z)) \to G (⟨X, X⟩ \underset{˙}{\cdot} Z) ((X Inv (C) Y) (F) (⟨X, Y⟩ \underset{˙}{\cdot} X) F) = G (⟨X, X⟩ \underset{˙}{\cdot} Z) Id (C) (X)$
45	1 2 30 19 21 3 26 40	catrid	$⊢ (φ \land k \in (Y H Z)) \to G (⟨X, X⟩ \underset{˙}{\cdot} Z) Id (C) (X) = G$
46	41 44 45	3eqtrd	$⊢ (φ \land k \in (Y H Z)) \to (G (⟨Y, X⟩ \underset{˙}{\cdot} Z) (X Inv (C) Y) (F)) (⟨X, Y⟩ \underset{˙}{\cdot} Z) F = G$
47	46	adantr	$⊢ ((φ \land k \in (Y H Z)) \land k = G (⟨Y, X⟩ \underset{˙}{\cdot} Z) (X Inv (C) Y) (F)) \to (G (⟨Y, X⟩ \underset{˙}{\cdot} Z) (X Inv (C) Y) (F)) (⟨X, Y⟩ \underset{˙}{\cdot} Z) F = G$
48	39 47	eqtr2d	$⊢ ((φ \land k \in (Y H Z)) \land k = G (⟨Y, X⟩ \underset{˙}{\cdot} Z) (X Inv (C) Y) (F)) \to G = k (⟨X, Y⟩ \underset{˙}{\cdot} Z) F$
49	37 48	impbida	$⊢ (φ \land k \in (Y H Z)) \to (G = k (⟨X, Y⟩ \underset{˙}{\cdot} Z) F \leftrightarrow k = G (⟨Y, X⟩ \underset{˙}{\cdot} Z) (X Inv (C) Y) (F))$
50	49	ralrimiva	$⊢ φ \to \forall k \in (Y H Z) (G = k (⟨X, Y⟩ \underset{˙}{\cdot} Z) F \leftrightarrow k = G (⟨Y, X⟩ \underset{˙}{\cdot} Z) (X Inv (C) Y) (F))$
51		reu6i	$⊢ (G (⟨Y, X⟩ \underset{˙}{\cdot} Z) (X Inv (C) Y) (F) \in (Y H Z) \land \forall k \in (Y H Z) (G = k (⟨X, Y⟩ \underset{˙}{\cdot} Z) F \leftrightarrow k = G (⟨Y, X⟩ \underset{˙}{\cdot} Z) (X Inv (C) Y) (F))) \to \exists! k \in (Y H Z) G = k (⟨X, Y⟩ \underset{˙}{\cdot} Z) F$
52	16 50 51	syl2anc	$⊢ φ \to \exists! k \in (Y H Z) G = k (⟨X, Y⟩ \underset{˙}{\cdot} Z) F$

Metamath Proof Explorer

Theorem upeu2lem

Proof