Metamath Proof Explorer

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 = ( Base ` C )
paridval.h 
|- H = ( Hom ` C )
paridval.hv 
|- H = ( x e. B , y e. B |-> if ( x = y , { J } , if ( ( x = X /\ y = Y ) , S , (/) ) ) )
paridval.c 
|- ( ph -> C e. Cat )
parcoval2.o 
|- .x. = ( comp ` C )
parcoval2.f 
|- ( ph -> F e. ( U H V ) )
parcoval2.g 
|- ( ph -> G e. ( V H W ) )
Assertion parcoval2 
|- ( ph -> ( G ( <. U , V >. .x. W ) F ) = if ( U = V , G , F ) )

Proof

Step Hyp Ref Expression
1 paridval.b 
 |-  B = ( Base ` C )
2 paridval.h 
 |-  H = ( Hom ` C )
3 paridval.hv 
 |-  H = ( x e. B , y e. B |-> if ( x = y , { J } , if ( ( x = X /\ y = Y ) , S , (/) ) ) )
4 paridval.c 
 |-  ( ph -> C e. Cat )
5 parcoval2.o 
 |-  .x. = ( comp ` C )
6 parcoval2.f 
 |-  ( ph -> F e. ( U H V ) )
7 parcoval2.g 
 |-  ( ph -> G e. ( V H W ) )
8 simpr 
 |-  ( ( ph /\ U = V ) -> U = V )
9 8 opeq1d 
 |-  ( ( ph /\ U = V ) -> <. U , V >. = <. V , V >. )
10 9 oveq1d 
 |-  ( ( ph /\ U = V ) -> ( <. U , V >. .x. W ) = ( <. V , V >. .x. W ) )
11 eqidd 
 |-  ( ( ph /\ U = V ) -> G = G )
12 6 adantr 
 |-  ( ( ph /\ U = V ) -> F e. ( U H V ) )
13 3 12 8 parhomideq 
 |-  ( ( ph /\ U = V ) -> F = J )
14 3 elmpocl2 
 |-  ( F e. ( U H V ) -> V e. B )
15 6 14 syl 
 |-  ( ph -> V e. B )
16 1 2 3 4 15 paridval 
 |-  ( ph -> ( ( Id ` C ) ` V ) = J )
17 16 adantr 
 |-  ( ( ph /\ U = V ) -> ( ( Id ` C ) ` V ) = J )
18 13 17 eqtr4d 
 |-  ( ( ph /\ U = V ) -> F = ( ( Id ` C ) ` V ) )
19 10 11 18 oveq123d 
 |-  ( ( ph /\ U = V ) -> ( G ( <. U , V >. .x. W ) F ) = ( G ( <. V , V >. .x. W ) ( ( Id ` C ) ` V ) ) )
20 eqid 
 |-  ( Id ` C ) = ( Id ` C )
21 3 elmpocl2 
 |-  ( G e. ( V H W ) -> W e. B )
22 7 21 syl 
 |-  ( ph -> W e. B )
23 1 2 20 4 15 5 22 7 catrid 
 |-  ( ph -> ( G ( <. V , V >. .x. W ) ( ( Id ` C ) ` V ) ) = G )
24 23 adantr 
 |-  ( ( ph /\ U = V ) -> ( G ( <. V , V >. .x. W ) ( ( Id ` C ) ` V ) ) = G )
25 19 24 eqtrd 
 |-  ( ( ph /\ U = V ) -> ( G ( <. U , V >. .x. W ) F ) = G )
26 8 iftrued 
 |-  ( ( ph /\ U = V ) -> if ( U = V , G , F ) = G )
27 25 26 eqtr4d 
 |-  ( ( ph /\ U = V ) -> ( G ( <. U , V >. .x. W ) F ) = if ( U = V , G , F ) )
28 3 6 7 parhomeqor 
 |-  ( ph -> ( U = V \/ V = W ) )
29 28 orcanai 
 |-  ( ( ph /\ -. U = V ) -> V = W )
30 29 eqcomd 
 |-  ( ( ph /\ -. U = V ) -> W = V )
31 30 oveq2d 
 |-  ( ( ph /\ -. U = V ) -> ( <. U , V >. .x. W ) = ( <. U , V >. .x. V ) )
32 7 adantr 
 |-  ( ( ph /\ -. U = V ) -> G e. ( V H W ) )
33 3 32 29 parhomideq 
 |-  ( ( ph /\ -. U = V ) -> G = J )
34 16 adantr 
 |-  ( ( ph /\ -. U = V ) -> ( ( Id ` C ) ` V ) = J )
35 33 34 eqtr4d 
 |-  ( ( ph /\ -. U = V ) -> G = ( ( Id ` C ) ` V ) )
36 eqidd 
 |-  ( ( ph /\ -. U = V ) -> F = F )
37 31 35 36 oveq123d 
 |-  ( ( ph /\ -. U = V ) -> ( G ( <. U , V >. .x. W ) F ) = ( ( ( Id ` C ) ` V ) ( <. U , V >. .x. V ) F ) )
38 3 elmpocl1 
 |-  ( F e. ( U H V ) -> U e. B )
39 6 38 syl 
 |-  ( ph -> U e. B )
40 1 2 20 4 39 5 15 6 catlid 
 |-  ( ph -> ( ( ( Id ` C ) ` V ) ( <. U , V >. .x. V ) F ) = F )
41 40 adantr 
 |-  ( ( ph /\ -. U = V ) -> ( ( ( Id ` C ) ` V ) ( <. U , V >. .x. V ) F ) = F )
42 37 41 eqtrd 
 |-  ( ( ph /\ -. U = V ) -> ( G ( <. U , V >. .x. W ) F ) = F )
43 simpr 
 |-  ( ( ph /\ -. U = V ) -> -. U = V )
44 43 iffalsed 
 |-  ( ( ph /\ -. U = V ) -> if ( U = V , G , F ) = F )
45 42 44 eqtr4d 
 |-  ( ( ph /\ -. U = V ) -> ( G ( <. U , V >. .x. W ) F ) = if ( U = V , G , F ) )
46 27 45 pm2.61dan 
 |-  ( ph -> ( G ( <. U , V >. .x. W ) F ) = if ( U = V , G , F ) )