Metamath Proof Explorer

Theorem lanpropd

Description: If the categories have the same set of objects, morphisms, and compositions, then they have the same left Kan extensions. (Contributed by Zhi Wang, 21-Nov-2025)

Ref Expression
Hypotheses lanpropd.1 
|- ( ph -> ( Homf ` A ) = ( Homf ` B ) )
lanpropd.2 
|- ( ph -> ( comf ` A ) = ( comf ` B ) )
lanpropd.3 
|- ( ph -> ( Homf ` C ) = ( Homf ` D ) )
lanpropd.4 
|- ( ph -> ( comf ` C ) = ( comf ` D ) )
lanpropd.5 
|- ( ph -> ( Homf ` E ) = ( Homf ` F ) )
lanpropd.6 
|- ( ph -> ( comf ` E ) = ( comf ` F ) )
lanpropd.a 
|- ( ph -> A e. V )
lanpropd.b 
|- ( ph -> B e. V )
lanpropd.c 
|- ( ph -> C e. V )
lanpropd.d 
|- ( ph -> D e. V )
lanpropd.e 
|- ( ph -> E e. V )
lanpropd.f 
|- ( ph -> F e. V )
Assertion lanpropd 
|- ( ph -> ( <. A , C >. Lan E ) = ( <. B , D >. Lan F ) )

Proof

Step Hyp Ref Expression
1 lanpropd.1 
 |-  ( ph -> ( Homf ` A ) = ( Homf ` B ) )
2 lanpropd.2 
 |-  ( ph -> ( comf ` A ) = ( comf ` B ) )
3 lanpropd.3 
 |-  ( ph -> ( Homf ` C ) = ( Homf ` D ) )
4 lanpropd.4 
 |-  ( ph -> ( comf ` C ) = ( comf ` D ) )
5 lanpropd.5 
 |-  ( ph -> ( Homf ` E ) = ( Homf ` F ) )
6 lanpropd.6 
 |-  ( ph -> ( comf ` E ) = ( comf ` F ) )
7 lanpropd.a 
 |-  ( ph -> A e. V )
8 lanpropd.b 
 |-  ( ph -> B e. V )
9 lanpropd.c 
 |-  ( ph -> C e. V )
10 lanpropd.d 
 |-  ( ph -> D e. V )
11 lanpropd.e 
 |-  ( ph -> E e. V )
12 lanpropd.f 
 |-  ( ph -> F e. V )
13 1 2 3 4 7 8 9 10 funcpropd 
 |-  ( ph -> ( A Func C ) = ( B Func D ) )
14 1 2 5 6 7 8 11 12 funcpropd 
 |-  ( ph -> ( A Func E ) = ( B Func F ) )
15 14 adantr 
 |-  ( ( ph /\ f e. ( A Func C ) ) -> ( A Func E ) = ( B Func F ) )
16 3 adantr 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> ( Homf ` C ) = ( Homf ` D ) )
17 4 adantr 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> ( comf ` C ) = ( comf ` D ) )
18 5 adantr 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> ( Homf ` E ) = ( Homf ` F ) )
19 6 adantr 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> ( comf ` E ) = ( comf ` F ) )
20 funcrcl 
 |-  ( f e. ( A Func C ) -> ( A e. Cat /\ C e. Cat ) )
21 20 ad2antrl 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> ( A e. Cat /\ C e. Cat ) )
22 21 simprd 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> C e. Cat )
23 10 adantr 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> D e. V )
24 16 17 22 23 catpropd 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> ( C e. Cat <-> D e. Cat ) )
25 22 24 mpbid 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> D e. Cat )
26 funcrcl 
 |-  ( x e. ( A Func E ) -> ( A e. Cat /\ E e. Cat ) )
27 26 ad2antll 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> ( A e. Cat /\ E e. Cat ) )
28 27 simprd 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> E e. Cat )
29 12 adantr 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> F e. V )
30 18 19 28 29 catpropd 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> ( E e. Cat <-> F e. Cat ) )
31 28 30 mpbid 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> F e. Cat )
32 16 17 18 19 22 25 28 31 fucpropd 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> ( C FuncCat E ) = ( D FuncCat F ) )
33 1 adantr 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> ( Homf ` A ) = ( Homf ` B ) )
34 2 adantr 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> ( comf ` A ) = ( comf ` B ) )
35 21 simpld 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> A e. Cat )
36 8 adantr 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> B e. V )
37 33 34 35 36 catpropd 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> ( A e. Cat <-> B e. Cat ) )
38 35 37 mpbid 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> B e. Cat )
39 33 34 18 19 35 38 28 31 fucpropd 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> ( A FuncCat E ) = ( B FuncCat F ) )
40 32 39 oveq12d 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> ( ( C FuncCat E ) UP ( A FuncCat E ) ) = ( ( D FuncCat F ) UP ( B FuncCat F ) ) )
41 simprl 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> f e. ( A Func C ) )
42 16 17 18 19 22 25 28 31 41 prcofpropd 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> ( <. C , E >. -o.F f ) = ( <. D , F >. -o.F f ) )
43 eqidd 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> x = x )
44 40 42 43 oveq123d 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> ( ( <. C , E >. -o.F f ) ( ( C FuncCat E ) UP ( A FuncCat E ) ) x ) = ( ( <. D , F >. -o.F f ) ( ( D FuncCat F ) UP ( B FuncCat F ) ) x ) )
45 13 15 44 mpoeq123dva 
 |-  ( ph -> ( f e. ( A Func C ) , x e. ( A Func E ) |-> ( ( <. C , E >. -o.F f ) ( ( C FuncCat E ) UP ( A FuncCat E ) ) x ) ) = ( f e. ( B Func D ) , x e. ( B Func F ) |-> ( ( <. D , F >. -o.F f ) ( ( D FuncCat F ) UP ( B FuncCat F ) ) x ) ) )
46 eqid 
 |-  ( C FuncCat E ) = ( C FuncCat E )
47 eqid 
 |-  ( A FuncCat E ) = ( A FuncCat E )
48 46 47 7 9 11 lanfval 
 |-  ( ph -> ( <. A , C >. Lan E ) = ( f e. ( A Func C ) , x e. ( A Func E ) |-> ( ( <. C , E >. -o.F f ) ( ( C FuncCat E ) UP ( A FuncCat E ) ) x ) ) )
49 eqid 
 |-  ( D FuncCat F ) = ( D FuncCat F )
50 eqid 
 |-  ( B FuncCat F ) = ( B FuncCat F )
51 49 50 8 10 12 lanfval 
 |-  ( ph -> ( <. B , D >. Lan F ) = ( f e. ( B Func D ) , x e. ( B Func F ) |-> ( ( <. D , F >. -o.F f ) ( ( D FuncCat F ) UP ( B FuncCat F ) ) x ) ) )
52 45 48 51 3eqtr4d 
 |-  ( ph -> ( <. A , C >. Lan E ) = ( <. B , D >. Lan F ) )