concom

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

	Ref	Expression
Hypotheses	islmd.l	⊢ 𝐿 = ( 𝐶 Δ_func 𝐷 )
	islmd.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
	islmd.n	⊢ 𝑁 = ( 𝐷 Nat 𝐶 )
	islmd.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
	concl.k	⊢ 𝐾 = ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 )
	concl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
	concl.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	concom.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
	concom.m	⊢ ( 𝜑 → 𝑀 ∈ ( 𝑌 𝐽 𝑍 ) )
	concom.j	⊢ 𝐽 = ( Hom ‘ 𝐷 )
	concom.o	⊢ · = ( comp ‘ 𝐶 )
	concom.r	⊢ ( 𝜑 → 𝑅 ∈ ( 𝐾 𝑁 𝐹 ) )
Assertion	concom	⊢ ( 𝜑 → ( 𝑅 ‘ 𝑍 ) = ( ( ( 𝑌 ( 2^nd ‘ 𝐹 ) 𝑍 ) ‘ 𝑀 ) ( ⟨ 𝑋 , ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ⟩ · ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ) ( 𝑅 ‘ 𝑌 ) ) )

Proof

Step	Hyp	Ref	Expression
1		islmd.l	⊢ 𝐿 = ( 𝐶 Δ_func 𝐷 )
2		islmd.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
3		islmd.n	⊢ 𝑁 = ( 𝐷 Nat 𝐶 )
4		islmd.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
5		concl.k	⊢ 𝐾 = ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 )
6		concl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
7		concl.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
8		concom.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
9		concom.m	⊢ ( 𝜑 → 𝑀 ∈ ( 𝑌 𝐽 𝑍 ) )
10		concom.j	⊢ 𝐽 = ( Hom ‘ 𝐷 )
11		concom.o	⊢ · = ( comp ‘ 𝐶 )
12		concom.r	⊢ ( 𝜑 → 𝑅 ∈ ( 𝐾 𝑁 𝐹 ) )
13	3 12	nat1st2nd	⊢ ( 𝜑 → 𝑅 ∈ ( ⟨ ( 1^st ‘ 𝐾 ) , ( 2^nd ‘ 𝐾 ) ⟩ 𝑁 ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ ) )
14	3 13 4 10 11 7 8 9	nati	⊢ ( 𝜑 → ( ( 𝑅 ‘ 𝑍 ) ( ⟨ ( ( 1^st ‘ 𝐾 ) ‘ 𝑌 ) , ( ( 1^st ‘ 𝐾 ) ‘ 𝑍 ) ⟩ · ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ) ( ( 𝑌 ( 2^nd ‘ 𝐾 ) 𝑍 ) ‘ 𝑀 ) ) = ( ( ( 𝑌 ( 2^nd ‘ 𝐹 ) 𝑍 ) ‘ 𝑀 ) ( ⟨ ( ( 1^st ‘ 𝐾 ) ‘ 𝑌 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ⟩ · ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ) ( 𝑅 ‘ 𝑌 ) ) )
15	3 13	natrcl3	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) ( 𝐷 Func 𝐶 ) ( 2^nd ‘ 𝐹 ) )
16	15	funcrcl3	⊢ ( 𝜑 → 𝐶 ∈ Cat )
17	15	funcrcl2	⊢ ( 𝜑 → 𝐷 ∈ Cat )
18	1 16 17 2 6 5 4 7	diag11	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐾 ) ‘ 𝑌 ) = 𝑋 )
19	1 16 17 2 6 5 4 8	diag11	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐾 ) ‘ 𝑍 ) = 𝑋 )
20	18 19	opeq12d	⊢ ( 𝜑 → ⟨ ( ( 1^st ‘ 𝐾 ) ‘ 𝑌 ) , ( ( 1^st ‘ 𝐾 ) ‘ 𝑍 ) ⟩ = ⟨ 𝑋 , 𝑋 ⟩ )
21	20	oveq1d	⊢ ( 𝜑 → ( ⟨ ( ( 1^st ‘ 𝐾 ) ‘ 𝑌 ) , ( ( 1^st ‘ 𝐾 ) ‘ 𝑍 ) ⟩ · ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ) = ( ⟨ 𝑋 , 𝑋 ⟩ · ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ) )
22		eqidd	⊢ ( 𝜑 → ( 𝑅 ‘ 𝑍 ) = ( 𝑅 ‘ 𝑍 ) )
23		eqid	⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
24	1 16 17 2 6 5 4 7 10 23 8 9	diag12	⊢ ( 𝜑 → ( ( 𝑌 ( 2^nd ‘ 𝐾 ) 𝑍 ) ‘ 𝑀 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) )
25	21 22 24	oveq123d	⊢ ( 𝜑 → ( ( 𝑅 ‘ 𝑍 ) ( ⟨ ( ( 1^st ‘ 𝐾 ) ‘ 𝑌 ) , ( ( 1^st ‘ 𝐾 ) ‘ 𝑍 ) ⟩ · ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ) ( ( 𝑌 ( 2^nd ‘ 𝐾 ) 𝑍 ) ‘ 𝑀 ) ) = ( ( 𝑅 ‘ 𝑍 ) ( ⟨ 𝑋 , 𝑋 ⟩ · ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ) ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) )
26		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
27	4 2 15	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) : 𝐵 ⟶ 𝐴 )
28	27 8	ffvelcdmd	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ∈ 𝐴 )
29	1 2 3 4 5 6 8 26 12	concl	⊢ ( 𝜑 → ( 𝑅 ‘ 𝑍 ) ∈ ( 𝑋 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ) )
30	2 26 23 16 6 11 28 29	catrid	⊢ ( 𝜑 → ( ( 𝑅 ‘ 𝑍 ) ( ⟨ 𝑋 , 𝑋 ⟩ · ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ) ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) = ( 𝑅 ‘ 𝑍 ) )
31	25 30	eqtrd	⊢ ( 𝜑 → ( ( 𝑅 ‘ 𝑍 ) ( ⟨ ( ( 1^st ‘ 𝐾 ) ‘ 𝑌 ) , ( ( 1^st ‘ 𝐾 ) ‘ 𝑍 ) ⟩ · ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ) ( ( 𝑌 ( 2^nd ‘ 𝐾 ) 𝑍 ) ‘ 𝑀 ) ) = ( 𝑅 ‘ 𝑍 ) )
32	18	opeq1d	⊢ ( 𝜑 → ⟨ ( ( 1^st ‘ 𝐾 ) ‘ 𝑌 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ⟩ = ⟨ 𝑋 , ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ⟩ )
33	32	oveq1d	⊢ ( 𝜑 → ( ⟨ ( ( 1^st ‘ 𝐾 ) ‘ 𝑌 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ⟩ · ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ) = ( ⟨ 𝑋 , ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ⟩ · ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ) )
34	33	oveqd	⊢ ( 𝜑 → ( ( ( 𝑌 ( 2^nd ‘ 𝐹 ) 𝑍 ) ‘ 𝑀 ) ( ⟨ ( ( 1^st ‘ 𝐾 ) ‘ 𝑌 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ⟩ · ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ) ( 𝑅 ‘ 𝑌 ) ) = ( ( ( 𝑌 ( 2^nd ‘ 𝐹 ) 𝑍 ) ‘ 𝑀 ) ( ⟨ 𝑋 , ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ⟩ · ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ) ( 𝑅 ‘ 𝑌 ) ) )
35	14 31 34	3eqtr3d	⊢ ( 𝜑 → ( 𝑅 ‘ 𝑍 ) = ( ( ( 𝑌 ( 2^nd ‘ 𝐹 ) 𝑍 ) ‘ 𝑀 ) ( ⟨ 𝑋 , ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ⟩ · ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ) ( 𝑅 ‘ 𝑌 ) ) )

Metamath Proof Explorer

Theorem concom

Proof