Metamath Proof Explorer

Theorem 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 DiagFunc D )
islmd.a 
|- A = ( Base ` C )
islmd.n 
|- N = ( D Nat C )
islmd.b 
|- B = ( Base ` D )
concl.k 
|- K = ( ( 1st ` L ) ` X )
concl.x 
|- ( ph -> X e. A )
concl.y 
|- ( ph -> Y e. B )
concom.z 
|- ( ph -> Z e. B )
concom.m 
|- ( ph -> M e. ( Y J Z ) )
concom.j 
|- J = ( Hom ` D )
concom.o 
|- .x. = ( comp ` C )
concom.r 
|- ( ph -> R e. ( K N F ) )
Assertion concom 
|- ( ph -> ( R ` Z ) = ( ( ( Y ( 2nd ` F ) Z ) ` M ) ( <. X , ( ( 1st ` F ) ` Y ) >. .x. ( ( 1st ` F ) ` Z ) ) ( R ` Y ) ) )

Proof

Step Hyp Ref Expression
1 islmd.l 
 |-  L = ( C DiagFunc D )
2 islmd.a 
 |-  A = ( Base ` C )
3 islmd.n 
 |-  N = ( D Nat C )
4 islmd.b 
 |-  B = ( Base ` D )
5 concl.k 
 |-  K = ( ( 1st ` L ) ` X )
6 concl.x 
 |-  ( ph -> X e. A )
7 concl.y 
 |-  ( ph -> Y e. B )
8 concom.z 
 |-  ( ph -> Z e. B )
9 concom.m 
 |-  ( ph -> M e. ( Y J Z ) )
10 concom.j 
 |-  J = ( Hom ` D )
11 concom.o 
 |-  .x. = ( comp ` C )
12 concom.r 
 |-  ( ph -> R e. ( K N F ) )
13 3 12 nat1st2nd 
 |-  ( ph -> R e. ( <. ( 1st ` K ) , ( 2nd ` K ) >. N <. ( 1st ` F ) , ( 2nd ` F ) >. ) )
14 3 13 4 10 11 7 8 9 nati 
 |-  ( ph -> ( ( R ` Z ) ( <. ( ( 1st ` K ) ` Y ) , ( ( 1st ` K ) ` Z ) >. .x. ( ( 1st ` F ) ` Z ) ) ( ( Y ( 2nd ` K ) Z ) ` M ) ) = ( ( ( Y ( 2nd ` F ) Z ) ` M ) ( <. ( ( 1st ` K ) ` Y ) , ( ( 1st ` F ) ` Y ) >. .x. ( ( 1st ` F ) ` Z ) ) ( R ` Y ) ) )
15 3 13 natrcl3 
 |-  ( ph -> ( 1st ` F ) ( D Func C ) ( 2nd ` F ) )
16 15 funcrcl3 
 |-  ( ph -> C e. Cat )
17 15 funcrcl2 
 |-  ( ph -> D e. Cat )
18 1 16 17 2 6 5 4 7 diag11 
 |-  ( ph -> ( ( 1st ` K ) ` Y ) = X )
19 1 16 17 2 6 5 4 8 diag11 
 |-  ( ph -> ( ( 1st ` K ) ` Z ) = X )
20 18 19 opeq12d 
 |-  ( ph -> <. ( ( 1st ` K ) ` Y ) , ( ( 1st ` K ) ` Z ) >. = <. X , X >. )
21 20 oveq1d 
 |-  ( ph -> ( <. ( ( 1st ` K ) ` Y ) , ( ( 1st ` K ) ` Z ) >. .x. ( ( 1st ` F ) ` Z ) ) = ( <. X , X >. .x. ( ( 1st ` F ) ` Z ) ) )
22 eqidd 
 |-  ( ph -> ( R ` Z ) = ( R ` Z ) )
23 eqid 
 |-  ( Id ` C ) = ( Id ` C )
24 1 16 17 2 6 5 4 7 10 23 8 9 diag12 
 |-  ( ph -> ( ( Y ( 2nd ` K ) Z ) ` M ) = ( ( Id ` C ) ` X ) )
25 21 22 24 oveq123d 
 |-  ( ph -> ( ( R ` Z ) ( <. ( ( 1st ` K ) ` Y ) , ( ( 1st ` K ) ` Z ) >. .x. ( ( 1st ` F ) ` Z ) ) ( ( Y ( 2nd ` K ) Z ) ` M ) ) = ( ( R ` Z ) ( <. X , X >. .x. ( ( 1st ` F ) ` Z ) ) ( ( Id ` C ) ` X ) ) )
26 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
27 4 2 15 funcf1 
 |-  ( ph -> ( 1st ` F ) : B --> A )
28 27 8 ffvelcdmd 
 |-  ( ph -> ( ( 1st ` F ) ` Z ) e. A )
29 1 2 3 4 5 6 8 26 12 concl 
 |-  ( ph -> ( R ` Z ) e. ( X ( Hom ` C ) ( ( 1st ` F ) ` Z ) ) )
30 2 26 23 16 6 11 28 29 catrid 
 |-  ( ph -> ( ( R ` Z ) ( <. X , X >. .x. ( ( 1st ` F ) ` Z ) ) ( ( Id ` C ) ` X ) ) = ( R ` Z ) )
31 25 30 eqtrd 
 |-  ( ph -> ( ( R ` Z ) ( <. ( ( 1st ` K ) ` Y ) , ( ( 1st ` K ) ` Z ) >. .x. ( ( 1st ` F ) ` Z ) ) ( ( Y ( 2nd ` K ) Z ) ` M ) ) = ( R ` Z ) )
32 18 opeq1d 
 |-  ( ph -> <. ( ( 1st ` K ) ` Y ) , ( ( 1st ` F ) ` Y ) >. = <. X , ( ( 1st ` F ) ` Y ) >. )
33 32 oveq1d 
 |-  ( ph -> ( <. ( ( 1st ` K ) ` Y ) , ( ( 1st ` F ) ` Y ) >. .x. ( ( 1st ` F ) ` Z ) ) = ( <. X , ( ( 1st ` F ) ` Y ) >. .x. ( ( 1st ` F ) ` Z ) ) )
34 33 oveqd 
 |-  ( ph -> ( ( ( Y ( 2nd ` F ) Z ) ` M ) ( <. ( ( 1st ` K ) ` Y ) , ( ( 1st ` F ) ` Y ) >. .x. ( ( 1st ` F ) ` Z ) ) ( R ` Y ) ) = ( ( ( Y ( 2nd ` F ) Z ) ` M ) ( <. X , ( ( 1st ` F ) ` Y ) >. .x. ( ( 1st ` F ) ` Z ) ) ( R ` Y ) ) )
35 14 31 34 3eqtr3d 
 |-  ( ph -> ( R ` Z ) = ( ( ( Y ( 2nd ` F ) Z ) ` M ) ( <. X , ( ( 1st ` F ) ` Y ) >. .x. ( ( 1st ` F ) ` Z ) ) ( R ` Y ) ) )