Theorem parcoval2

Description: Composition in a category with the parallel-arrow hom construction. Every composable pair contains an identity, so the category identity laws determine the value. (Contributed by Zhi Wang, 17-Sep-2026)

	Ref	Expression
Hypotheses	paridval.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	paridval.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
	paridval.hv	⊢ 𝐻 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ if ( 𝑥 = 𝑦 , { 𝐽 } , if ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) , 𝑆 , ∅ ) ) )
	paridval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	parcoval2.o	⊢ · = ( comp ‘ 𝐶 )
	parcoval2.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑈 𝐻 𝑉 ) )
	parcoval2.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑉 𝐻 𝑊 ) )
Assertion	parcoval2	⊢ ( 𝜑 → ( 𝐺 ( ⟨ 𝑈 , 𝑉 ⟩ · 𝑊 ) 𝐹 ) = if ( 𝑈 = 𝑉 , 𝐺 , 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		paridval.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
2		paridval.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
3		paridval.hv	⊢ 𝐻 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ if ( 𝑥 = 𝑦 , { 𝐽 } , if ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) , 𝑆 , ∅ ) ) )
4		paridval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
5		parcoval2.o	⊢ · = ( comp ‘ 𝐶 )
6		parcoval2.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑈 𝐻 𝑉 ) )
7		parcoval2.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑉 𝐻 𝑊 ) )
8		simpr	⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → 𝑈 = 𝑉 )
9	8	opeq1d	⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → ⟨ 𝑈 , 𝑉 ⟩ = ⟨ 𝑉 , 𝑉 ⟩ )
10	9	oveq1d	⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → ( ⟨ 𝑈 , 𝑉 ⟩ · 𝑊 ) = ( ⟨ 𝑉 , 𝑉 ⟩ · 𝑊 ) )
11		eqidd	⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → 𝐺 = 𝐺 )
12	6	adantr	⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → 𝐹 ∈ ( 𝑈 𝐻 𝑉 ) )
13	3 12 8	parhomideq	⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → 𝐹 = 𝐽 )
14	3	elmpocl2	⊢ ( 𝐹 ∈ ( 𝑈 𝐻 𝑉 ) → 𝑉 ∈ 𝐵 )
15	6 14	syl	⊢ ( 𝜑 → 𝑉 ∈ 𝐵 )
16	1 2 3 4 15	paridval	⊢ ( 𝜑 → ( ( Id ‘ 𝐶 ) ‘ 𝑉 ) = 𝐽 )
17	16	adantr	⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → ( ( Id ‘ 𝐶 ) ‘ 𝑉 ) = 𝐽 )
18	13 17	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → 𝐹 = ( ( Id ‘ 𝐶 ) ‘ 𝑉 ) )
19	10 11 18	oveq123d	⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → ( 𝐺 ( ⟨ 𝑈 , 𝑉 ⟩ · 𝑊 ) 𝐹 ) = ( 𝐺 ( ⟨ 𝑉 , 𝑉 ⟩ · 𝑊 ) ( ( Id ‘ 𝐶 ) ‘ 𝑉 ) ) )
20		eqid	⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
21	3	elmpocl2	⊢ ( 𝐺 ∈ ( 𝑉 𝐻 𝑊 ) → 𝑊 ∈ 𝐵 )
22	7 21	syl	⊢ ( 𝜑 → 𝑊 ∈ 𝐵 )
23	1 2 20 4 15 5 22 7	catrid	⊢ ( 𝜑 → ( 𝐺 ( ⟨ 𝑉 , 𝑉 ⟩ · 𝑊 ) ( ( Id ‘ 𝐶 ) ‘ 𝑉 ) ) = 𝐺 )
24	23	adantr	⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → ( 𝐺 ( ⟨ 𝑉 , 𝑉 ⟩ · 𝑊 ) ( ( Id ‘ 𝐶 ) ‘ 𝑉 ) ) = 𝐺 )
25	19 24	eqtrd	⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → ( 𝐺 ( ⟨ 𝑈 , 𝑉 ⟩ · 𝑊 ) 𝐹 ) = 𝐺 )
26	8	iftrued	⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → if ( 𝑈 = 𝑉 , 𝐺 , 𝐹 ) = 𝐺 )
27	25 26	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → ( 𝐺 ( ⟨ 𝑈 , 𝑉 ⟩ · 𝑊 ) 𝐹 ) = if ( 𝑈 = 𝑉 , 𝐺 , 𝐹 ) )
28	3 6 7	parhomeqor	⊢ ( 𝜑 → ( 𝑈 = 𝑉 ∨ 𝑉 = 𝑊 ) )
29	28	orcanai	⊢ ( ( 𝜑 ∧ ¬ 𝑈 = 𝑉 ) → 𝑉 = 𝑊 )
30	29	eqcomd	⊢ ( ( 𝜑 ∧ ¬ 𝑈 = 𝑉 ) → 𝑊 = 𝑉 )
31	30	oveq2d	⊢ ( ( 𝜑 ∧ ¬ 𝑈 = 𝑉 ) → ( ⟨ 𝑈 , 𝑉 ⟩ · 𝑊 ) = ( ⟨ 𝑈 , 𝑉 ⟩ · 𝑉 ) )
32	7	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑈 = 𝑉 ) → 𝐺 ∈ ( 𝑉 𝐻 𝑊 ) )
33	3 32 29	parhomideq	⊢ ( ( 𝜑 ∧ ¬ 𝑈 = 𝑉 ) → 𝐺 = 𝐽 )
34	16	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑈 = 𝑉 ) → ( ( Id ‘ 𝐶 ) ‘ 𝑉 ) = 𝐽 )
35	33 34	eqtr4d	⊢ ( ( 𝜑 ∧ ¬ 𝑈 = 𝑉 ) → 𝐺 = ( ( Id ‘ 𝐶 ) ‘ 𝑉 ) )
36		eqidd	⊢ ( ( 𝜑 ∧ ¬ 𝑈 = 𝑉 ) → 𝐹 = 𝐹 )
37	31 35 36	oveq123d	⊢ ( ( 𝜑 ∧ ¬ 𝑈 = 𝑉 ) → ( 𝐺 ( ⟨ 𝑈 , 𝑉 ⟩ · 𝑊 ) 𝐹 ) = ( ( ( Id ‘ 𝐶 ) ‘ 𝑉 ) ( ⟨ 𝑈 , 𝑉 ⟩ · 𝑉 ) 𝐹 ) )
38	3	elmpocl1	⊢ ( 𝐹 ∈ ( 𝑈 𝐻 𝑉 ) → 𝑈 ∈ 𝐵 )
39	6 38	syl	⊢ ( 𝜑 → 𝑈 ∈ 𝐵 )
40	1 2 20 4 39 5 15 6	catlid	⊢ ( 𝜑 → ( ( ( Id ‘ 𝐶 ) ‘ 𝑉 ) ( ⟨ 𝑈 , 𝑉 ⟩ · 𝑉 ) 𝐹 ) = 𝐹 )
41	40	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑈 = 𝑉 ) → ( ( ( Id ‘ 𝐶 ) ‘ 𝑉 ) ( ⟨ 𝑈 , 𝑉 ⟩ · 𝑉 ) 𝐹 ) = 𝐹 )
42	37 41	eqtrd	⊢ ( ( 𝜑 ∧ ¬ 𝑈 = 𝑉 ) → ( 𝐺 ( ⟨ 𝑈 , 𝑉 ⟩ · 𝑊 ) 𝐹 ) = 𝐹 )
43		simpr	⊢ ( ( 𝜑 ∧ ¬ 𝑈 = 𝑉 ) → ¬ 𝑈 = 𝑉 )
44	43	iffalsed	⊢ ( ( 𝜑 ∧ ¬ 𝑈 = 𝑉 ) → if ( 𝑈 = 𝑉 , 𝐺 , 𝐹 ) = 𝐹 )
45	42 44	eqtr4d	⊢ ( ( 𝜑 ∧ ¬ 𝑈 = 𝑉 ) → ( 𝐺 ( ⟨ 𝑈 , 𝑉 ⟩ · 𝑊 ) 𝐹 ) = if ( 𝑈 = 𝑉 , 𝐺 , 𝐹 ) )
46	27 45	pm2.61dan	⊢ ( 𝜑 → ( 𝐺 ( ⟨ 𝑈 , 𝑉 ⟩ · 𝑊 ) 𝐹 ) = if ( 𝑈 = 𝑉 , 𝐺 , 𝐹 ) )