Metamath Proof Explorer

Theorem upciclem2

Description: Lemma for upciclem3 and upeu2 . (Contributed by Zhi Wang, 19-Sep-2025)

Ref Expression
Hypotheses upcic.b 
|- B = ( Base ` D )
upcic.c 
|- C = ( Base ` E )
upcic.h 
|- H = ( Hom ` D )
upcic.j 
|- J = ( Hom ` E )
upcic.o 
|- O = ( comp ` E )
upcic.f 
|- ( ph -> F ( D Func E ) G )
upcic.x 
|- ( ph -> X e. B )
upcic.y 
|- ( ph -> Y e. B )
upciclem2.z 
|- ( ph -> Z e. B )
upciclem2.w 
|- ( ph -> W e. C )
upciclem2.m 
|- ( ph -> M e. ( W J ( F ` X ) ) )
upciclem2.od 
|- .x. = ( comp ` D )
upciclem2.k 
|- ( ph -> K e. ( X H Y ) )
upciclem2.l 
|- ( ph -> L e. ( Y H Z ) )
upciclem2.nm 
|- ( ph -> N = ( ( ( X G Y ) ` K ) ( <. W , ( F ` X ) >. O ( F ` Y ) ) M ) )
Assertion upciclem2 
|- ( ph -> ( ( ( X G Z ) ` ( L ( <. X , Y >. .x. Z ) K ) ) ( <. W , ( F ` X ) >. O ( F ` Z ) ) M ) = ( ( ( Y G Z ) ` L ) ( <. W , ( F ` Y ) >. O ( F ` Z ) ) N ) )

Proof

Step Hyp Ref Expression
1 upcic.b 
 |-  B = ( Base ` D )
2 upcic.c 
 |-  C = ( Base ` E )
3 upcic.h 
 |-  H = ( Hom ` D )
4 upcic.j 
 |-  J = ( Hom ` E )
5 upcic.o 
 |-  O = ( comp ` E )
6 upcic.f 
 |-  ( ph -> F ( D Func E ) G )
7 upcic.x 
 |-  ( ph -> X e. B )
8 upcic.y 
 |-  ( ph -> Y e. B )
9 upciclem2.z 
 |-  ( ph -> Z e. B )
10 upciclem2.w 
 |-  ( ph -> W e. C )
11 upciclem2.m 
 |-  ( ph -> M e. ( W J ( F ` X ) ) )
12 upciclem2.od 
 |-  .x. = ( comp ` D )
13 upciclem2.k 
 |-  ( ph -> K e. ( X H Y ) )
14 upciclem2.l 
 |-  ( ph -> L e. ( Y H Z ) )
15 upciclem2.nm 
 |-  ( ph -> N = ( ( ( X G Y ) ` K ) ( <. W , ( F ` X ) >. O ( F ` Y ) ) M ) )
16 6 funcrcl3 
 |-  ( ph -> E e. Cat )
17 1 2 6 funcf1 
 |-  ( ph -> F : B --> C )
18 17 7 ffvelcdmd 
 |-  ( ph -> ( F ` X ) e. C )
19 17 8 ffvelcdmd 
 |-  ( ph -> ( F ` Y ) e. C )
20 1 3 4 6 7 8 funcf2 
 |-  ( ph -> ( X G Y ) : ( X H Y ) --> ( ( F ` X ) J ( F ` Y ) ) )
21 20 13 ffvelcdmd 
 |-  ( ph -> ( ( X G Y ) ` K ) e. ( ( F ` X ) J ( F ` Y ) ) )
22 17 9 ffvelcdmd 
 |-  ( ph -> ( F ` Z ) e. C )
23 1 3 4 6 8 9 funcf2 
 |-  ( ph -> ( Y G Z ) : ( Y H Z ) --> ( ( F ` Y ) J ( F ` Z ) ) )
24 23 14 ffvelcdmd 
 |-  ( ph -> ( ( Y G Z ) ` L ) e. ( ( F ` Y ) J ( F ` Z ) ) )
25 2 4 5 16 10 18 19 11 21 22 24 catass 
 |-  ( ph -> ( ( ( ( Y G Z ) ` L ) ( <. ( F ` X ) , ( F ` Y ) >. O ( F ` Z ) ) ( ( X G Y ) ` K ) ) ( <. W , ( F ` X ) >. O ( F ` Z ) ) M ) = ( ( ( Y G Z ) ` L ) ( <. W , ( F ` Y ) >. O ( F ` Z ) ) ( ( ( X G Y ) ` K ) ( <. W , ( F ` X ) >. O ( F ` Y ) ) M ) ) )
26 1 3 12 5 6 7 8 9 13 14 funcco 
 |-  ( ph -> ( ( X G Z ) ` ( L ( <. X , Y >. .x. Z ) K ) ) = ( ( ( Y G Z ) ` L ) ( <. ( F ` X ) , ( F ` Y ) >. O ( F ` Z ) ) ( ( X G Y ) ` K ) ) )
27 26 oveq1d 
 |-  ( ph -> ( ( ( X G Z ) ` ( L ( <. X , Y >. .x. Z ) K ) ) ( <. W , ( F ` X ) >. O ( F ` Z ) ) M ) = ( ( ( ( Y G Z ) ` L ) ( <. ( F ` X ) , ( F ` Y ) >. O ( F ` Z ) ) ( ( X G Y ) ` K ) ) ( <. W , ( F ` X ) >. O ( F ` Z ) ) M ) )
28 15 oveq2d 
 |-  ( ph -> ( ( ( Y G Z ) ` L ) ( <. W , ( F ` Y ) >. O ( F ` Z ) ) N ) = ( ( ( Y G Z ) ` L ) ( <. W , ( F ` Y ) >. O ( F ` Z ) ) ( ( ( X G Y ) ` K ) ( <. W , ( F ` X ) >. O ( F ` Y ) ) M ) ) )
29 25 27 28 3eqtr4d 
 |-  ( ph -> ( ( ( X G Z ) ` ( L ( <. X , Y >. .x. Z ) K ) ) ( <. W , ( F ` X ) >. O ( F ` Z ) ) M ) = ( ( ( Y G Z ) ` L ) ( <. W , ( F ` Y ) >. O ( F ` Z ) ) N ) )