Metamath Proof Explorer

Theorem functhinclem4

Description: Lemma for functhinc . Other requirements on the morphism part are automatically satisfied. (Contributed by Zhi Wang, 1-Oct-2024)

Ref Expression
Hypotheses functhinc.b 
|- B = ( Base ` D )
functhinc.c 
|- C = ( Base ` E )
functhinc.h 
|- H = ( Hom ` D )
functhinc.j 
|- J = ( Hom ` E )
functhinc.d 
|- ( ph -> D e. Cat )
functhinc.e 
|- ( ph -> E e. ThinCat )
functhinc.f 
|- ( ph -> F : B --> C )
functhinc.k 
|- K = ( x e. B , y e. B |-> ( ( x H y ) X. ( ( F ` x ) J ( F ` y ) ) ) )
functhinc.1 
|- ( ph -> A. z e. B A. w e. B ( ( ( F ` z ) J ( F ` w ) ) = (/) -> ( z H w ) = (/) ) )
functhinclem4.1 
|- .1. = ( Id ` D )
functhinclem4.i 
|- I = ( Id ` E )
functhinclem4.x 
|- .x. = ( comp ` D )
functhinclem4.o 
|- O = ( comp ` E )
Assertion functhinclem4 
|- ( ( ph /\ G = K ) -> A. a e. B ( ( ( a G a ) ` ( .1. ` a ) ) = ( I ` ( F ` a ) ) /\ A. b e. B A. c e. B A. m e. ( a H b ) A. n e. ( b H c ) ( ( a G c ) ` ( n ( <. a , b >. .x. c ) m ) ) = ( ( ( b G c ) ` n ) ( <. ( F ` a ) , ( F ` b ) >. O ( F ` c ) ) ( ( a G b ) ` m ) ) ) )

Proof

Step Hyp Ref Expression
1 functhinc.b 
 |-  B = ( Base ` D )
2 functhinc.c 
 |-  C = ( Base ` E )
3 functhinc.h 
 |-  H = ( Hom ` D )
4 functhinc.j 
 |-  J = ( Hom ` E )
5 functhinc.d 
 |-  ( ph -> D e. Cat )
6 functhinc.e 
 |-  ( ph -> E e. ThinCat )
7 functhinc.f 
 |-  ( ph -> F : B --> C )
8 functhinc.k 
 |-  K = ( x e. B , y e. B |-> ( ( x H y ) X. ( ( F ` x ) J ( F ` y ) ) ) )
9 functhinc.1 
 |-  ( ph -> A. z e. B A. w e. B ( ( ( F ` z ) J ( F ` w ) ) = (/) -> ( z H w ) = (/) ) )
10 functhinclem4.1 
 |-  .1. = ( Id ` D )
11 functhinclem4.i 
 |-  I = ( Id ` E )
12 functhinclem4.x 
 |-  .x. = ( comp ` D )
13 functhinclem4.o 
 |-  O = ( comp ` E )
14 6 ad2antrr 
 |-  ( ( ( ph /\ G = K ) /\ a e. B ) -> E e. ThinCat )
15 7 adantr 
 |-  ( ( ph /\ G = K ) -> F : B --> C )
16 15 ffvelrnda 
 |-  ( ( ( ph /\ G = K ) /\ a e. B ) -> ( F ` a ) e. C )
17 simpr 
 |-  ( ( ( ph /\ G = K ) /\ a e. B ) -> a e. B )
18 5 ad2antrr 
 |-  ( ( ( ph /\ G = K ) /\ a e. B ) -> D e. Cat )
19 1 3 10 18 17 catidcl 
 |-  ( ( ( ph /\ G = K ) /\ a e. B ) -> ( .1. ` a ) e. ( a H a ) )
20 simplr 
 |-  ( ( ( ph /\ G = K ) /\ a e. B ) -> G = K )
21 oveq1 
 |-  ( x = v -> ( x H y ) = ( v H y ) )
22 fveq2 
 |-  ( x = v -> ( F ` x ) = ( F ` v ) )
23 22 oveq1d 
 |-  ( x = v -> ( ( F ` x ) J ( F ` y ) ) = ( ( F ` v ) J ( F ` y ) ) )
24 21 23 xpeq12d 
 |-  ( x = v -> ( ( x H y ) X. ( ( F ` x ) J ( F ` y ) ) ) = ( ( v H y ) X. ( ( F ` v ) J ( F ` y ) ) ) )
25 oveq2 
 |-  ( y = u -> ( v H y ) = ( v H u ) )
26 fveq2 
 |-  ( y = u -> ( F ` y ) = ( F ` u ) )
27 26 oveq2d 
 |-  ( y = u -> ( ( F ` v ) J ( F ` y ) ) = ( ( F ` v ) J ( F ` u ) ) )
28 25 27 xpeq12d 
 |-  ( y = u -> ( ( v H y ) X. ( ( F ` v ) J ( F ` y ) ) ) = ( ( v H u ) X. ( ( F ` v ) J ( F ` u ) ) ) )
29 24 28 cbvmpov 
 |-  ( x e. B , y e. B |-> ( ( x H y ) X. ( ( F ` x ) J ( F ` y ) ) ) ) = ( v e. B , u e. B |-> ( ( v H u ) X. ( ( F ` v ) J ( F ` u ) ) ) )
30 8 29 eqtri 
 |-  K = ( v e. B , u e. B |-> ( ( v H u ) X. ( ( F ` v ) J ( F ` u ) ) ) )
31 20 30 eqtrdi 
 |-  ( ( ( ph /\ G = K ) /\ a e. B ) -> G = ( v e. B , u e. B |-> ( ( v H u ) X. ( ( F ` v ) J ( F ` u ) ) ) ) )
32 9 ad2antrr 
 |-  ( ( ( ph /\ G = K ) /\ a e. B ) -> A. z e. B A. w e. B ( ( ( F ` z ) J ( F ` w ) ) = (/) -> ( z H w ) = (/) ) )
33 17 17 32 functhinclem2 
 |-  ( ( ( ph /\ G = K ) /\ a e. B ) -> ( ( ( F ` a ) J ( F ` a ) ) = (/) -> ( a H a ) = (/) ) )
34 14 16 16 2 4 thincmo 
 |-  ( ( ( ph /\ G = K ) /\ a e. B ) -> E* p p e. ( ( F ` a ) J ( F ` a ) ) )
35 17 17 19 31 33 34 functhinclem3 
 |-  ( ( ( ph /\ G = K ) /\ a e. B ) -> ( ( a G a ) ` ( .1. ` a ) ) e. ( ( F ` a ) J ( F ` a ) ) )
36 14 2 4 16 11 35 thincid 
 |-  ( ( ( ph /\ G = K ) /\ a e. B ) -> ( ( a G a ) ` ( .1. ` a ) ) = ( I ` ( F ` a ) ) )
37 16 ad2antrr 
 |-  ( ( ( ( ( ph /\ G = K ) /\ a e. B ) /\ ( b e. B /\ c e. B ) ) /\ ( m e. ( a H b ) /\ n e. ( b H c ) ) ) -> ( F ` a ) e. C )
38 7 ad4antr 
 |-  ( ( ( ( ( ph /\ G = K ) /\ a e. B ) /\ ( b e. B /\ c e. B ) ) /\ ( m e. ( a H b ) /\ n e. ( b H c ) ) ) -> F : B --> C )
39 simplrr 
 |-  ( ( ( ( ( ph /\ G = K ) /\ a e. B ) /\ ( b e. B /\ c e. B ) ) /\ ( m e. ( a H b ) /\ n e. ( b H c ) ) ) -> c e. B )
40 38 39 ffvelrnd 
 |-  ( ( ( ( ( ph /\ G = K ) /\ a e. B ) /\ ( b e. B /\ c e. B ) ) /\ ( m e. ( a H b ) /\ n e. ( b H c ) ) ) -> ( F ` c ) e. C )
41 17 ad2antrr 
 |-  ( ( ( ( ( ph /\ G = K ) /\ a e. B ) /\ ( b e. B /\ c e. B ) ) /\ ( m e. ( a H b ) /\ n e. ( b H c ) ) ) -> a e. B )
42 5 ad4antr 
 |-  ( ( ( ( ( ph /\ G = K ) /\ a e. B ) /\ ( b e. B /\ c e. B ) ) /\ ( m e. ( a H b ) /\ n e. ( b H c ) ) ) -> D e. Cat )
43 simplrl 
 |-  ( ( ( ( ( ph /\ G = K ) /\ a e. B ) /\ ( b e. B /\ c e. B ) ) /\ ( m e. ( a H b ) /\ n e. ( b H c ) ) ) -> b e. B )
44 simprl 
 |-  ( ( ( ( ( ph /\ G = K ) /\ a e. B ) /\ ( b e. B /\ c e. B ) ) /\ ( m e. ( a H b ) /\ n e. ( b H c ) ) ) -> m e. ( a H b ) )
45 simprr 
 |-  ( ( ( ( ( ph /\ G = K ) /\ a e. B ) /\ ( b e. B /\ c e. B ) ) /\ ( m e. ( a H b ) /\ n e. ( b H c ) ) ) -> n e. ( b H c ) )
46 1 3 12 42 41 43 39 44 45 catcocl 
 |-  ( ( ( ( ( ph /\ G = K ) /\ a e. B ) /\ ( b e. B /\ c e. B ) ) /\ ( m e. ( a H b ) /\ n e. ( b H c ) ) ) -> ( n ( <. a , b >. .x. c ) m ) e. ( a H c ) )
47 31 ad2antrr 
 |-  ( ( ( ( ( ph /\ G = K ) /\ a e. B ) /\ ( b e. B /\ c e. B ) ) /\ ( m e. ( a H b ) /\ n e. ( b H c ) ) ) -> G = ( v e. B , u e. B |-> ( ( v H u ) X. ( ( F ` v ) J ( F ` u ) ) ) ) )
48 9 ad4antr 
 |-  ( ( ( ( ( ph /\ G = K ) /\ a e. B ) /\ ( b e. B /\ c e. B ) ) /\ ( m e. ( a H b ) /\ n e. ( b H c ) ) ) -> A. z e. B A. w e. B ( ( ( F ` z ) J ( F ` w ) ) = (/) -> ( z H w ) = (/) ) )
49 41 39 48 functhinclem2 
 |-  ( ( ( ( ( ph /\ G = K ) /\ a e. B ) /\ ( b e. B /\ c e. B ) ) /\ ( m e. ( a H b ) /\ n e. ( b H c ) ) ) -> ( ( ( F ` a ) J ( F ` c ) ) = (/) -> ( a H c ) = (/) ) )
50 6 ad4antr 
 |-  ( ( ( ( ( ph /\ G = K ) /\ a e. B ) /\ ( b e. B /\ c e. B ) ) /\ ( m e. ( a H b ) /\ n e. ( b H c ) ) ) -> E e. ThinCat )
51 50 37 40 2 4 thincmo 
 |-  ( ( ( ( ( ph /\ G = K ) /\ a e. B ) /\ ( b e. B /\ c e. B ) ) /\ ( m e. ( a H b ) /\ n e. ( b H c ) ) ) -> E* p p e. ( ( F ` a ) J ( F ` c ) ) )
52 41 39 46 47 49 51 functhinclem3 
 |-  ( ( ( ( ( ph /\ G = K ) /\ a e. B ) /\ ( b e. B /\ c e. B ) ) /\ ( m e. ( a H b ) /\ n e. ( b H c ) ) ) -> ( ( a G c ) ` ( n ( <. a , b >. .x. c ) m ) ) e. ( ( F ` a ) J ( F ` c ) ) )
53 14 thinccd 
 |-  ( ( ( ph /\ G = K ) /\ a e. B ) -> E e. Cat )
54 53 ad2antrr 
 |-  ( ( ( ( ( ph /\ G = K ) /\ a e. B ) /\ ( b e. B /\ c e. B ) ) /\ ( m e. ( a H b ) /\ n e. ( b H c ) ) ) -> E e. Cat )
55 38 43 ffvelrnd 
 |-  ( ( ( ( ( ph /\ G = K ) /\ a e. B ) /\ ( b e. B /\ c e. B ) ) /\ ( m e. ( a H b ) /\ n e. ( b H c ) ) ) -> ( F ` b ) e. C )
56 41 43 48 functhinclem2 
 |-  ( ( ( ( ( ph /\ G = K ) /\ a e. B ) /\ ( b e. B /\ c e. B ) ) /\ ( m e. ( a H b ) /\ n e. ( b H c ) ) ) -> ( ( ( F ` a ) J ( F ` b ) ) = (/) -> ( a H b ) = (/) ) )
57 50 37 55 2 4 thincmo 
 |-  ( ( ( ( ( ph /\ G = K ) /\ a e. B ) /\ ( b e. B /\ c e. B ) ) /\ ( m e. ( a H b ) /\ n e. ( b H c ) ) ) -> E* p p e. ( ( F ` a ) J ( F ` b ) ) )
58 41 43 44 47 56 57 functhinclem3 
 |-  ( ( ( ( ( ph /\ G = K ) /\ a e. B ) /\ ( b e. B /\ c e. B ) ) /\ ( m e. ( a H b ) /\ n e. ( b H c ) ) ) -> ( ( a G b ) ` m ) e. ( ( F ` a ) J ( F ` b ) ) )
59 43 39 48 functhinclem2 
 |-  ( ( ( ( ( ph /\ G = K ) /\ a e. B ) /\ ( b e. B /\ c e. B ) ) /\ ( m e. ( a H b ) /\ n e. ( b H c ) ) ) -> ( ( ( F ` b ) J ( F ` c ) ) = (/) -> ( b H c ) = (/) ) )
60 50 55 40 2 4 thincmo 
 |-  ( ( ( ( ( ph /\ G = K ) /\ a e. B ) /\ ( b e. B /\ c e. B ) ) /\ ( m e. ( a H b ) /\ n e. ( b H c ) ) ) -> E* p p e. ( ( F ` b ) J ( F ` c ) ) )
61 43 39 45 47 59 60 functhinclem3 
 |-  ( ( ( ( ( ph /\ G = K ) /\ a e. B ) /\ ( b e. B /\ c e. B ) ) /\ ( m e. ( a H b ) /\ n e. ( b H c ) ) ) -> ( ( b G c ) ` n ) e. ( ( F ` b ) J ( F ` c ) ) )
62 2 4 13 54 37 55 40 58 61 catcocl 
 |-  ( ( ( ( ( ph /\ G = K ) /\ a e. B ) /\ ( b e. B /\ c e. B ) ) /\ ( m e. ( a H b ) /\ n e. ( b H c ) ) ) -> ( ( ( b G c ) ` n ) ( <. ( F ` a ) , ( F ` b ) >. O ( F ` c ) ) ( ( a G b ) ` m ) ) e. ( ( F ` a ) J ( F ` c ) ) )
63 37 40 52 62 2 4 50 thincmo2 
 |-  ( ( ( ( ( ph /\ G = K ) /\ a e. B ) /\ ( b e. B /\ c e. B ) ) /\ ( m e. ( a H b ) /\ n e. ( b H c ) ) ) -> ( ( a G c ) ` ( n ( <. a , b >. .x. c ) m ) ) = ( ( ( b G c ) ` n ) ( <. ( F ` a ) , ( F ` b ) >. O ( F ` c ) ) ( ( a G b ) ` m ) ) )
64 63 ralrimivva 
 |-  ( ( ( ( ph /\ G = K ) /\ a e. B ) /\ ( b e. B /\ c e. B ) ) -> A. m e. ( a H b ) A. n e. ( b H c ) ( ( a G c ) ` ( n ( <. a , b >. .x. c ) m ) ) = ( ( ( b G c ) ` n ) ( <. ( F ` a ) , ( F ` b ) >. O ( F ` c ) ) ( ( a G b ) ` m ) ) )
65 64 ralrimivva 
 |-  ( ( ( ph /\ G = K ) /\ a e. B ) -> A. b e. B A. c e. B A. m e. ( a H b ) A. n e. ( b H c ) ( ( a G c ) ` ( n ( <. a , b >. .x. c ) m ) ) = ( ( ( b G c ) ` n ) ( <. ( F ` a ) , ( F ` b ) >. O ( F ` c ) ) ( ( a G b ) ` m ) ) )
66 36 65 jca 
 |-  ( ( ( ph /\ G = K ) /\ a e. B ) -> ( ( ( a G a ) ` ( .1. ` a ) ) = ( I ` ( F ` a ) ) /\ A. b e. B A. c e. B A. m e. ( a H b ) A. n e. ( b H c ) ( ( a G c ) ` ( n ( <. a , b >. .x. c ) m ) ) = ( ( ( b G c ) ` n ) ( <. ( F ` a ) , ( F ` b ) >. O ( F ` c ) ) ( ( a G b ) ` m ) ) ) )
67 66 ralrimiva 
 |-  ( ( ph /\ G = K ) -> A. a e. B ( ( ( a G a ) ` ( .1. ` a ) ) = ( I ` ( F ` a ) ) /\ A. b e. B A. c e. B A. m e. ( a H b ) A. n e. ( b H c ) ( ( a G c ) ` ( n ( <. a , b >. .x. c ) m ) ) = ( ( ( b G c ) ` n ) ( <. ( F ` a ) , ( F ` b ) >. O ( F ` c ) ) ( ( a G b ) ` m ) ) ) )