concom

Description: A cone to a diagram commutes with the diagram. (Contributed by Zhi Wang, 13-Nov-2025)

	Ref	Expression
Hypotheses	islmd.l	$⊢ L = C Δ_{func} D$
	islmd.a	$⊢ A = {Base}_{C}$
	islmd.n	$⊢ N = D Nat C$
	islmd.b	$⊢ B = {Base}_{D}$
	concl.k	$⊢ K = 1^{st} (L) (X)$
	concl.x	$⊢ φ \to X \in A$
	concl.y	$⊢ φ \to Y \in B$
	concom.z	$⊢ φ \to Z \in B$
	concom.m	$⊢ φ \to M \in (Y J Z)$
	concom.j	$⊢ J = Hom (D)$
	concom.o	$⊢ \underset{˙}{\cdot} = comp (C)$
	concom.r	$⊢ φ \to R \in (K N F)$
Assertion	concom	$⊢ φ \to R (Z) = (Y 2^{nd} (F) Z) (M) (⟨X, 1^{st} (F) (Y)⟩ \underset{˙}{\cdot} 1^{st} (F) (Z)) R (Y)$

Proof

Step	Hyp	Ref	Expression
1		islmd.l	$⊢ L = C Δ_{func} D$
2		islmd.a	$⊢ A = {Base}_{C}$
3		islmd.n	$⊢ N = D Nat C$
4		islmd.b	$⊢ B = {Base}_{D}$
5		concl.k	$⊢ K = 1^{st} (L) (X)$
6		concl.x	$⊢ φ \to X \in A$
7		concl.y	$⊢ φ \to Y \in B$
8		concom.z	$⊢ φ \to Z \in B$
9		concom.m	$⊢ φ \to M \in (Y J Z)$
10		concom.j	$⊢ J = Hom (D)$
11		concom.o	$⊢ \underset{˙}{\cdot} = comp (C)$
12		concom.r	$⊢ φ \to R \in (K N F)$
13	3 12	nat1st2nd	$⊢ φ \to R \in (⟨1^{st} (K), 2^{nd} (K)⟩ N ⟨1^{st} (F), 2^{nd} (F)⟩)$
14	3 13 4 10 11 7 8 9	nati	$⊢ φ \to R (Z) (⟨1^{st} (K) (Y), 1^{st} (K) (Z)⟩ \underset{˙}{\cdot} 1^{st} (F) (Z)) (Y 2^{nd} (K) Z) (M) = (Y 2^{nd} (F) Z) (M) (⟨1^{st} (K) (Y), 1^{st} (F) (Y)⟩ \underset{˙}{\cdot} 1^{st} (F) (Z)) R (Y)$
15	3 13	natrcl3	$⊢ φ \to 1^{st} (F) (D Func C) 2^{nd} (F)$
16	15	funcrcl3	$⊢ φ \to C \in Cat$
17	15	funcrcl2	$⊢ φ \to D \in Cat$
18	1 16 17 2 6 5 4 7	diag11	$⊢ φ \to 1^{st} (K) (Y) = X$
19	1 16 17 2 6 5 4 8	diag11	$⊢ φ \to 1^{st} (K) (Z) = X$
20	18 19	opeq12d	$⊢ φ \to ⟨1^{st} (K) (Y), 1^{st} (K) (Z)⟩ = ⟨X, X⟩$
21	20	oveq1d	$⊢ φ \to ⟨1^{st} (K) (Y), 1^{st} (K) (Z)⟩ \underset{˙}{\cdot} 1^{st} (F) (Z) = ⟨X, X⟩ \underset{˙}{\cdot} 1^{st} (F) (Z)$
22		eqidd	$⊢ φ \to R (Z) = R (Z)$
23		eqid	$⊢ Id (C) = Id (C)$
24	1 16 17 2 6 5 4 7 10 23 8 9	diag12	$⊢ φ \to (Y 2^{nd} (K) Z) (M) = Id (C) (X)$
25	21 22 24	oveq123d	$⊢ φ \to R (Z) (⟨1^{st} (K) (Y), 1^{st} (K) (Z)⟩ \underset{˙}{\cdot} 1^{st} (F) (Z)) (Y 2^{nd} (K) Z) (M) = R (Z) (⟨X, X⟩ \underset{˙}{\cdot} 1^{st} (F) (Z)) Id (C) (X)$
26		eqid	$⊢ Hom (C) = Hom (C)$
27	4 2 15	funcf1	$⊢ φ \to 1^{st} (F) : B ⟶ A$
28	27 8	ffvelcdmd	$⊢ φ \to 1^{st} (F) (Z) \in A$
29	1 2 3 4 5 6 8 26 12	concl	$⊢ φ \to R (Z) \in (X Hom (C) 1^{st} (F) (Z))$
30	2 26 23 16 6 11 28 29	catrid	$⊢ φ \to R (Z) (⟨X, X⟩ \underset{˙}{\cdot} 1^{st} (F) (Z)) Id (C) (X) = R (Z)$
31	25 30	eqtrd	$⊢ φ \to R (Z) (⟨1^{st} (K) (Y), 1^{st} (K) (Z)⟩ \underset{˙}{\cdot} 1^{st} (F) (Z)) (Y 2^{nd} (K) Z) (M) = R (Z)$
32	18	opeq1d	$⊢ φ \to ⟨1^{st} (K) (Y), 1^{st} (F) (Y)⟩ = ⟨X, 1^{st} (F) (Y)⟩$
33	32	oveq1d	$⊢ φ \to ⟨1^{st} (K) (Y), 1^{st} (F) (Y)⟩ \underset{˙}{\cdot} 1^{st} (F) (Z) = ⟨X, 1^{st} (F) (Y)⟩ \underset{˙}{\cdot} 1^{st} (F) (Z)$
34	33	oveqd	$⊢ φ \to (Y 2^{nd} (F) Z) (M) (⟨1^{st} (K) (Y), 1^{st} (F) (Y)⟩ \underset{˙}{\cdot} 1^{st} (F) (Z)) R (Y) = (Y 2^{nd} (F) Z) (M) (⟨X, 1^{st} (F) (Y)⟩ \underset{˙}{\cdot} 1^{st} (F) (Z)) R (Y)$
35	14 31 34	3eqtr3d	$⊢ φ \to R (Z) = (Y 2^{nd} (F) Z) (M) (⟨X, 1^{st} (F) (Y)⟩ \underset{˙}{\cdot} 1^{st} (F) (Z)) R (Y)$

Metamath Proof Explorer

Theorem concom

Proof