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	$$⊢B={\mathrm{Base}}_C$$
	paridval.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
	paridval.hv	$$⊢H=\left(x\in B,y\in B⟼if\left(x=y,\left\{J\right\},if\left(\left(x=X\wedge y=Y\right),S,\varnothing \right)\right)\right)$$
	paridval.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	parcoval2.o	$$⊢\underset{\dot{}}{·}=\mathrm{comp}\left(C\right)$$
	parcoval2.f	$$⊢\phi \to F\in \left(UHV\right)$$
	parcoval2.g	$$⊢\phi \to G\in \left(VHW\right)$$
Assertion	parcoval2	$$⊢\phi \to G\left(⟨U,V⟩\underset{\dot{}}{·}W\right)F=if\left(U=V,G,F\right)$$

Proof

Step	Hyp	Ref	Expression
1		paridval.b	$$⊢B={\mathrm{Base}}_C$$
2		paridval.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
3		paridval.hv	$$⊢H=\left(x\in B,y\in B⟼if\left(x=y,\left\{J\right\},if\left(\left(x=X\wedge y=Y\right),S,\varnothing \right)\right)\right)$$
4		paridval.c	$$⊢\phi \to C\in \mathrm{Cat}$$
5		parcoval2.o	$$⊢\underset{\dot{}}{·}=\mathrm{comp}\left(C\right)$$
6		parcoval2.f	$$⊢\phi \to F\in \left(UHV\right)$$
7		parcoval2.g	$$⊢\phi \to G\in \left(VHW\right)$$
8		simpr	$$⊢\left(\phi \wedge U=V\right)\to U=V$$
9	8	opeq1d	$$⊢\left(\phi \wedge U=V\right)\to ⟨U,V⟩=⟨V,V⟩$$
10	9	oveq1d	$$⊢\left(\phi \wedge U=V\right)\to ⟨U,V⟩\underset{\dot{}}{·}W=⟨V,V⟩\underset{\dot{}}{·}W$$
11		eqidd	$$⊢\left(\phi \wedge U=V\right)\to G=G$$
12	6	adantr	$$⊢\left(\phi \wedge U=V\right)\to F\in \left(UHV\right)$$
13	3 12 8	parhomideq	$$⊢\left(\phi \wedge U=V\right)\to F=J$$
14	3	elmpocl2	$$⊢F\in \left(UHV\right)\to V\in B$$
15	6 14	syl	$$⊢\phi \to V\in B$$
16	1 2 3 4 15	paridval	$$⊢\phi \to \mathrm{Id}\left(C\right)\left(V\right)=J$$
17	16	adantr	$$⊢\left(\phi \wedge U=V\right)\to \mathrm{Id}\left(C\right)\left(V\right)=J$$
18	13 17	eqtr4d	$$⊢\left(\phi \wedge U=V\right)\to F=\mathrm{Id}\left(C\right)\left(V\right)$$
19	10 11 18	oveq123d	$$⊢\left(\phi \wedge U=V\right)\to G\left(⟨U,V⟩\underset{\dot{}}{·}W\right)F=G\left(⟨V,V⟩\underset{\dot{}}{·}W\right)\mathrm{Id}\left(C\right)\left(V\right)$$
20		eqid	$$⊢\mathrm{Id}\left(C\right)=\mathrm{Id}\left(C\right)$$
21	3	elmpocl2	$$⊢G\in \left(VHW\right)\to W\in B$$
22	7 21	syl	$$⊢\phi \to W\in B$$
23	1 2 20 4 15 5 22 7	catrid	$$⊢\phi \to G\left(⟨V,V⟩\underset{\dot{}}{·}W\right)\mathrm{Id}\left(C\right)\left(V\right)=G$$
24	23	adantr	$$⊢\left(\phi \wedge U=V\right)\to G\left(⟨V,V⟩\underset{\dot{}}{·}W\right)\mathrm{Id}\left(C\right)\left(V\right)=G$$
25	19 24	eqtrd	$$⊢\left(\phi \wedge U=V\right)\to G\left(⟨U,V⟩\underset{\dot{}}{·}W\right)F=G$$
26	8	iftrued	$$⊢\left(\phi \wedge U=V\right)\to if\left(U=V,G,F\right)=G$$
27	25 26	eqtr4d	$$⊢\left(\phi \wedge U=V\right)\to G\left(⟨U,V⟩\underset{\dot{}}{·}W\right)F=if\left(U=V,G,F\right)$$
28	3 6 7	parhomeqor	$$⊢\phi \to \left(U=V\vee V=W\right)$$
29	28	orcanai	$$⊢\left(\phi \wedge \neg U=V\right)\to V=W$$
30	29	eqcomd	$$⊢\left(\phi \wedge \neg U=V\right)\to W=V$$
31	30	oveq2d	$$⊢\left(\phi \wedge \neg U=V\right)\to ⟨U,V⟩\underset{\dot{}}{·}W=⟨U,V⟩\underset{\dot{}}{·}V$$
32	7	adantr	$$⊢\left(\phi \wedge \neg U=V\right)\to G\in \left(VHW\right)$$
33	3 32 29	parhomideq	$$⊢\left(\phi \wedge \neg U=V\right)\to G=J$$
34	16	adantr	$$⊢\left(\phi \wedge \neg U=V\right)\to \mathrm{Id}\left(C\right)\left(V\right)=J$$
35	33 34	eqtr4d	$$⊢\left(\phi \wedge \neg U=V\right)\to G=\mathrm{Id}\left(C\right)\left(V\right)$$
36		eqidd	$$⊢\left(\phi \wedge \neg U=V\right)\to F=F$$
37	31 35 36	oveq123d	$$⊢\left(\phi \wedge \neg U=V\right)\to G\left(⟨U,V⟩\underset{\dot{}}{·}W\right)F=\mathrm{Id}\left(C\right)\left(V\right)\left(⟨U,V⟩\underset{\dot{}}{·}V\right)F$$
38	3	elmpocl1	$$⊢F\in \left(UHV\right)\to U\in B$$
39	6 38	syl	$$⊢\phi \to U\in B$$
40	1 2 20 4 39 5 15 6	catlid	$$⊢\phi \to \mathrm{Id}\left(C\right)\left(V\right)\left(⟨U,V⟩\underset{\dot{}}{·}V\right)F=F$$
41	40	adantr	$$⊢\left(\phi \wedge \neg U=V\right)\to \mathrm{Id}\left(C\right)\left(V\right)\left(⟨U,V⟩\underset{\dot{}}{·}V\right)F=F$$
42	37 41	eqtrd	$$⊢\left(\phi \wedge \neg U=V\right)\to G\left(⟨U,V⟩\underset{\dot{}}{·}W\right)F=F$$
43		simpr	$$⊢\left(\phi \wedge \neg U=V\right)\to \neg U=V$$
44	43	iffalsed	$$⊢\left(\phi \wedge \neg U=V\right)\to if\left(U=V,G,F\right)=F$$
45	42 44	eqtr4d	$$⊢\left(\phi \wedge \neg U=V\right)\to G\left(⟨U,V⟩\underset{\dot{}}{·}W\right)F=if\left(U=V,G,F\right)$$
46	27 45	pm2.61dan	$$⊢\phi \to G\left(⟨U,V⟩\underset{\dot{}}{·}W\right)F=if\left(U=V,G,F\right)$$