upciclem3

	Ref	Expression
Hypotheses	upcic.b	$⊢ B = {Base}_{D}$
	upcic.c	$⊢ C = {Base}_{E}$
	upcic.h	$⊢ H = Hom (D)$
	upcic.j	$⊢ J = Hom (E)$
	upcic.o	$⊢ O = comp (E)$
	upcic.f	$⊢ φ \to F (D Func E) G$
	upcic.x	$⊢ φ \to X \in B$
	upcic.y	$⊢ φ \to Y \in B$
	upcic.z	$⊢ φ \to Z \in C$
	upcic.m	$⊢ φ \to M \in (Z J F (X))$
	upcic.1	$⊢ φ \to \forall w \in B \forall f \in (Z J F (w)) \exists! k \in (X H w) f = (X G w) (k) (⟨Z, F (X)⟩ O F (w)) M$
	upciclem3.od	$⊢ \underset{˙}{\cdot} = comp (D)$
	upciclem3.k	$⊢ φ \to K \in (X H Y)$
	upciclem3.l	$⊢ φ \to L \in (Y H X)$
	upciclem3.mn	$⊢ φ \to M = (Y G X) (L) (⟨Z, F (Y)⟩ O F (X)) N$
	upciclem3.nm	$⊢ φ \to N = (X G Y) (K) (⟨Z, F (X)⟩ O F (Y)) M$
Assertion	upciclem3	$⊢ φ \to L (⟨X, Y⟩ \underset{˙}{\cdot} X) K = Id (D) (X)$

Proof

Step	Hyp	Ref	Expression
1		upcic.b	$⊢ B = {Base}_{D}$
2		upcic.c	$⊢ C = {Base}_{E}$
3		upcic.h	$⊢ H = Hom (D)$
4		upcic.j	$⊢ J = Hom (E)$
5		upcic.o	$⊢ O = comp (E)$
6		upcic.f	$⊢ φ \to F (D Func E) G$
7		upcic.x	$⊢ φ \to X \in B$
8		upcic.y	$⊢ φ \to Y \in B$
9		upcic.z	$⊢ φ \to Z \in C$
10		upcic.m	$⊢ φ \to M \in (Z J F (X))$
11		upcic.1	$⊢ φ \to \forall w \in B \forall f \in (Z J F (w)) \exists! k \in (X H w) f = (X G w) (k) (⟨Z, F (X)⟩ O F (w)) M$
12		upciclem3.od	$⊢ \underset{˙}{\cdot} = comp (D)$
13		upciclem3.k	$⊢ φ \to K \in (X H Y)$
14		upciclem3.l	$⊢ φ \to L \in (Y H X)$
15		upciclem3.mn	$⊢ φ \to M = (Y G X) (L) (⟨Z, F (Y)⟩ O F (X)) N$
16		upciclem3.nm	$⊢ φ \to N = (X G Y) (K) (⟨Z, F (X)⟩ O F (Y)) M$
17		fveq2	$⊢ p = L (⟨X, Y⟩ \underset{˙}{\cdot} X) K \to (X G X) (p) = (X G X) (L (⟨X, Y⟩ \underset{˙}{\cdot} X) K)$
18	17	oveq1d	$⊢ p = L (⟨X, Y⟩ \underset{˙}{\cdot} X) K \to (X G X) (p) (⟨Z, F (X)⟩ O F (X)) M = (X G X) (L (⟨X, Y⟩ \underset{˙}{\cdot} X) K) (⟨Z, F (X)⟩ O F (X)) M$
19	18	eqeq2d	$⊢ p = L (⟨X, Y⟩ \underset{˙}{\cdot} X) K \to (M = (X G X) (p) (⟨Z, F (X)⟩ O F (X)) M \leftrightarrow M = (X G X) (L (⟨X, Y⟩ \underset{˙}{\cdot} X) K) (⟨Z, F (X)⟩ O F (X)) M)$
20		fveq2	$⊢ p = Id (D) (X) \to (X G X) (p) = (X G X) (Id (D) (X))$
21	20	oveq1d	$⊢ p = Id (D) (X) \to (X G X) (p) (⟨Z, F (X)⟩ O F (X)) M = (X G X) (Id (D) (X)) (⟨Z, F (X)⟩ O F (X)) M$
22	21	eqeq2d	$⊢ p = Id (D) (X) \to (M = (X G X) (p) (⟨Z, F (X)⟩ O F (X)) M \leftrightarrow M = (X G X) (Id (D) (X)) (⟨Z, F (X)⟩ O F (X)) M)$
23	11 7 10	upciclem1	$⊢ φ \to \exists! p \in (X H X) M = (X G X) (p) (⟨Z, F (X)⟩ O F (X)) M$
24	6	funcrcl2	$⊢ φ \to D \in Cat$
25	1 3 12 24 7 8 7 13 14	catcocl	$⊢ φ \to L (⟨X, Y⟩ \underset{˙}{\cdot} X) K \in (X H X)$
26		eqid	$⊢ Id (D) = Id (D)$
27	1 3 26 24 7	catidcl	$⊢ φ \to Id (D) (X) \in (X H X)$
28	1 2 3 4 5 6 7 8 7 9 10 12 13 14 16	upciclem2	$⊢ φ \to (X G X) (L (⟨X, Y⟩ \underset{˙}{\cdot} X) K) (⟨Z, F (X)⟩ O F (X)) M = (Y G X) (L) (⟨Z, F (Y)⟩ O F (X)) N$
29	15 28	eqtr4d	$⊢ φ \to M = (X G X) (L (⟨X, Y⟩ \underset{˙}{\cdot} X) K) (⟨Z, F (X)⟩ O F (X)) M$
30		eqid	$⊢ Id (E) = Id (E)$
31	1 26 30 6 7	funcid	$⊢ φ \to (X G X) (Id (D) (X)) = Id (E) (F (X))$
32	31	oveq1d	$⊢ φ \to (X G X) (Id (D) (X)) (⟨Z, F (X)⟩ O F (X)) M = Id (E) (F (X)) (⟨Z, F (X)⟩ O F (X)) M$
33	6	funcrcl3	$⊢ φ \to E \in Cat$
34	1 2 6	funcf1	$⊢ φ \to F : B ⟶ C$
35	34 7	ffvelcdmd	$⊢ φ \to F (X) \in C$
36	2 4 30 33 9 5 35 10	catlid	$⊢ φ \to Id (E) (F (X)) (⟨Z, F (X)⟩ O F (X)) M = M$
37	32 36	eqtr2d	$⊢ φ \to M = (X G X) (Id (D) (X)) (⟨Z, F (X)⟩ O F (X)) M$
38	19 22 23 25 27 29 37	reu2eqd	$⊢ φ \to L (⟨X, Y⟩ \underset{˙}{\cdot} X) K = Id (D) (X)$

Metamath Proof Explorer

Theorem upciclem3

Proof