Metamath Proof Explorer

Theorem parmapfunc2

Description: Variant of parmapfunc . (Contributed by Zhi Wang, 14-Sep-2026) (Revised by Zhi Wang, 17-Sep-2026) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses parmapfunc.b 
|- B = ( Base ` C )
parmapfunc.h 
|- H = ( Hom ` C )
parmapfunc.c 
|- C e. Cat
parmapfunc.hv 
|- H = ( r e. B , s e. B |-> if ( r = s , { J } , if ( ( r = X /\ s = Y ) , S , (/) ) ) )
parmapfunc.l 
|- L = ( u e. B , v e. B |-> ( a e. ( u H v ) |-> ( A ` a ) ) )
parmapfunc.ai 
|- ( A ` J ) = J
parmapfunc.as 
|- A. t e. S ( A ` t ) e. S
parmapfunc2.i 
|- I = ( Id ` C )
parmapfunc2.o 
|- .x. = ( comp ` C )
parmapfunc2.s 
|- S e. _V
parmapfunc2.j 
|- J e. _V
parmapfunc2.p 
|- S C_ ~P J
parmapfunc2.n 
|- X =/= Y
parmapfunc2.k 
|- K = ( S u. { J } )
parmapfunc2.mv 
|- M = ( f e. K , g e. K |-> ( f i^i g ) )
parmapfunc2.ov 
|- .x. = ( p e. ( B X. B ) , q e. B |-> M )
parmapfunc2.iv 
|- I = ( t e. B |-> J )
Assertion parmapfunc2 
|- ( _I |` B ) ( C Func C ) L

Proof

Step Hyp Ref Expression
1 parmapfunc.b 
 |-  B = ( Base ` C )
2 parmapfunc.h 
 |-  H = ( Hom ` C )
3 parmapfunc.c 
 |-  C e. Cat
4 parmapfunc.hv 
 |-  H = ( r e. B , s e. B |-> if ( r = s , { J } , if ( ( r = X /\ s = Y ) , S , (/) ) ) )
5 parmapfunc.l 
 |-  L = ( u e. B , v e. B |-> ( a e. ( u H v ) |-> ( A ` a ) ) )
6 parmapfunc.ai 
 |-  ( A ` J ) = J
7 parmapfunc.as 
 |-  A. t e. S ( A ` t ) e. S
8 parmapfunc2.i 
 |-  I = ( Id ` C )
9 parmapfunc2.o 
 |-  .x. = ( comp ` C )
10 parmapfunc2.s 
 |-  S e. _V
11 parmapfunc2.j 
 |-  J e. _V
12 parmapfunc2.p 
 |-  S C_ ~P J
13 parmapfunc2.n 
 |-  X =/= Y
14 parmapfunc2.k 
 |-  K = ( S u. { J } )
15 parmapfunc2.mv 
 |-  M = ( f e. K , g e. K |-> ( f i^i g ) )
16 parmapfunc2.ov 
 |-  .x. = ( p e. ( B X. B ) , q e. B |-> M )
17 parmapfunc2.iv 
 |-  I = ( t e. B |-> J )
18 3 a1i 
 |-  ( T. -> C e. Cat )
19 f1oi 
 |-  ( _I |` B ) : B -1-1-onto-> B
20 f1of 
 |-  ( ( _I |` B ) : B -1-1-onto-> B -> ( _I |` B ) : B --> B )
21 19 20 mp1i 
 |-  ( T. -> ( _I |` B ) : B --> B )
22 5 fnmpompt 
 |-  L Fn ( B X. B )
23 22 a1i 
 |-  ( T. -> L Fn ( B X. B ) )
24 simprl 
 |-  ( ( T. /\ ( x e. B /\ y e. B ) ) -> x e. B )
25 simprr 
 |-  ( ( T. /\ ( x e. B /\ y e. B ) ) -> y e. B )
26 5 24 25 ovmpomptd 
 |-  ( ( T. /\ ( x e. B /\ y e. B ) ) -> ( x L y ) = ( a e. ( x H y ) |-> ( A ` a ) ) )
27 simpr 
 |-  ( ( ( T. /\ ( x e. B /\ y e. B ) ) /\ a e. ( x H y ) ) -> a e. ( x H y ) )
28 6 a1i 
 |-  ( ( ( T. /\ ( x e. B /\ y e. B ) ) /\ a e. ( x H y ) ) -> ( A ` J ) = J )
29 fveq2 
 |-  ( t = a -> ( A ` t ) = ( A ` a ) )
30 29 eleq1d 
 |-  ( t = a -> ( ( A ` t ) e. S <-> ( A ` a ) e. S ) )
31 30 7 vtoclri 
 |-  ( a e. S -> ( A ` a ) e. S )
32 31 adantl 
 |-  ( ( ( ( T. /\ ( x e. B /\ y e. B ) ) /\ a e. ( x H y ) ) /\ a e. S ) -> ( A ` a ) e. S )
33 4 27 28 32 parmapcl 
 |-  ( ( ( T. /\ ( x e. B /\ y e. B ) ) /\ a e. ( x H y ) ) -> ( A ` a ) e. ( x H y ) )
34 26 33 fmpt3d 
 |-  ( ( T. /\ ( x e. B /\ y e. B ) ) -> ( x L y ) : ( x H y ) --> ( x H y ) )
35 fvresi 
 |-  ( x e. B -> ( ( _I |` B ) ` x ) = x )
36 24 35 syl 
 |-  ( ( T. /\ ( x e. B /\ y e. B ) ) -> ( ( _I |` B ) ` x ) = x )
37 fvresi 
 |-  ( y e. B -> ( ( _I |` B ) ` y ) = y )
38 25 37 syl 
 |-  ( ( T. /\ ( x e. B /\ y e. B ) ) -> ( ( _I |` B ) ` y ) = y )
39 36 38 oveq12d 
 |-  ( ( T. /\ ( x e. B /\ y e. B ) ) -> ( ( ( _I |` B ) ` x ) H ( ( _I |` B ) ` y ) ) = ( x H y ) )
40 39 feq3d 
 |-  ( ( T. /\ ( x e. B /\ y e. B ) ) -> ( ( x L y ) : ( x H y ) --> ( ( ( _I |` B ) ` x ) H ( ( _I |` B ) ` y ) ) <-> ( x L y ) : ( x H y ) --> ( x H y ) ) )
41 34 40 mpbird 
 |-  ( ( T. /\ ( x e. B /\ y e. B ) ) -> ( x L y ) : ( x H y ) --> ( ( ( _I |` B ) ` x ) H ( ( _I |` B ) ` y ) ) )
42 eqidd 
 |-  ( ( ( T. /\ x e. B ) /\ t = x ) -> J = J )
43 simpr 
 |-  ( ( T. /\ x e. B ) -> x e. B )
44 11 a1i 
 |-  ( ( T. /\ x e. B ) -> J e. _V )
45 17 42 43 44 fvmptd2 
 |-  ( ( T. /\ x e. B ) -> ( I ` x ) = J )
46 45 fveq2d 
 |-  ( ( T. /\ x e. B ) -> ( ( x L x ) ` ( I ` x ) ) = ( ( x L x ) ` J ) )
47 4 11 43 parhomid 
 |-  ( ( T. /\ x e. B ) -> J e. ( x H x ) )
48 5 43 43 47 fvmpomptd 
 |-  ( ( T. /\ x e. B ) -> ( ( x L x ) ` J ) = ( A ` J ) )
49 46 48 eqtrd 
 |-  ( ( T. /\ x e. B ) -> ( ( x L x ) ` ( I ` x ) ) = ( A ` J ) )
50 35 adantl 
 |-  ( ( T. /\ x e. B ) -> ( ( _I |` B ) ` x ) = x )
51 50 fveq2d 
 |-  ( ( T. /\ x e. B ) -> ( I ` ( ( _I |` B ) ` x ) ) = ( I ` x ) )
52 51 45 eqtrd 
 |-  ( ( T. /\ x e. B ) -> ( I ` ( ( _I |` B ) ` x ) ) = J )
53 6 49 52 3eqtr4a 
 |-  ( ( T. /\ x e. B ) -> ( ( x L x ) ` ( I ` x ) ) = ( I ` ( ( _I |` B ) ` x ) ) )
54 snex 
 |-  { J } e. _V
55 10 54 unex 
 |-  ( S u. { J } ) e. _V
56 14 55 eqeltri 
 |-  K e. _V
57 56 56 mpoex 
 |-  ( f e. K , g e. K |-> ( f i^i g ) ) e. _V
58 15 57 eqeltri 
 |-  M e. _V
59 simp21 
 |-  ( ( T. /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( i e. ( x H y ) /\ j e. ( y H z ) ) ) -> x e. B )
60 simp22 
 |-  ( ( T. /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( i e. ( x H y ) /\ j e. ( y H z ) ) ) -> y e. B )
61 simp23 
 |-  ( ( T. /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( i e. ( x H y ) /\ j e. ( y H z ) ) ) -> z e. B )
62 simp3l 
 |-  ( ( T. /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( i e. ( x H y ) /\ j e. ( y H z ) ) ) -> i e. ( x H y ) )
63 6 a1i 
 |-  ( ( T. /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( i e. ( x H y ) /\ j e. ( y H z ) ) ) -> ( A ` J ) = J )
64 fveq2 
 |-  ( t = i -> ( A ` t ) = ( A ` i ) )
65 64 eleq1d 
 |-  ( t = i -> ( ( A ` t ) e. S <-> ( A ` i ) e. S ) )
66 65 7 vtoclri 
 |-  ( i e. S -> ( A ` i ) e. S )
67 66 adantl 
 |-  ( ( ( T. /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( i e. ( x H y ) /\ j e. ( y H z ) ) ) /\ i e. S ) -> ( A ` i ) e. S )
68 4 62 63 67 parmapcl 
 |-  ( ( T. /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( i e. ( x H y ) /\ j e. ( y H z ) ) ) -> ( A ` i ) e. ( x H y ) )
69 4 14 68 parhomcl 
 |-  ( ( T. /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( i e. ( x H y ) /\ j e. ( y H z ) ) ) -> ( A ` i ) e. K )
70 simp3r 
 |-  ( ( T. /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( i e. ( x H y ) /\ j e. ( y H z ) ) ) -> j e. ( y H z ) )
71 fveq2 
 |-  ( t = j -> ( A ` t ) = ( A ` j ) )
72 71 eleq1d 
 |-  ( t = j -> ( ( A ` t ) e. S <-> ( A ` j ) e. S ) )
73 72 7 vtoclri 
 |-  ( j e. S -> ( A ` j ) e. S )
74 73 adantl 
 |-  ( ( ( T. /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( i e. ( x H y ) /\ j e. ( y H z ) ) ) /\ j e. S ) -> ( A ` j ) e. S )
75 4 70 63 74 parmapcl 
 |-  ( ( T. /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( i e. ( x H y ) /\ j e. ( y H z ) ) ) -> ( A ` j ) e. ( y H z ) )
76 4 14 75 parhomcl 
 |-  ( ( T. /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( i e. ( x H y ) /\ j e. ( y H z ) ) ) -> ( A ` j ) e. K )
77 15 16 58 59 60 61 69 76 parcoval 
 |-  ( ( T. /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( i e. ( x H y ) /\ j e. ( y H z ) ) ) -> ( ( A ` j ) ( <. x , y >. .x. z ) ( A ` i ) ) = ( ( A ` j ) i^i ( A ` i ) ) )
78 59 35 syl 
 |-  ( ( T. /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( i e. ( x H y ) /\ j e. ( y H z ) ) ) -> ( ( _I |` B ) ` x ) = x )
79 60 37 syl 
 |-  ( ( T. /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( i e. ( x H y ) /\ j e. ( y H z ) ) ) -> ( ( _I |` B ) ` y ) = y )
80 78 79 opeq12d 
 |-  ( ( T. /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( i e. ( x H y ) /\ j e. ( y H z ) ) ) -> <. ( ( _I |` B ) ` x ) , ( ( _I |` B ) ` y ) >. = <. x , y >. )
81 fvresi 
 |-  ( z e. B -> ( ( _I |` B ) ` z ) = z )
82 61 81 syl 
 |-  ( ( T. /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( i e. ( x H y ) /\ j e. ( y H z ) ) ) -> ( ( _I |` B ) ` z ) = z )
83 80 82 oveq12d 
 |-  ( ( T. /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( i e. ( x H y ) /\ j e. ( y H z ) ) ) -> ( <. ( ( _I |` B ) ` x ) , ( ( _I |` B ) ` y ) >. .x. ( ( _I |` B ) ` z ) ) = ( <. x , y >. .x. z ) )
84 5 60 61 70 fvmpomptd 
 |-  ( ( T. /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( i e. ( x H y ) /\ j e. ( y H z ) ) ) -> ( ( y L z ) ` j ) = ( A ` j ) )
85 5 59 60 62 fvmpomptd 
 |-  ( ( T. /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( i e. ( x H y ) /\ j e. ( y H z ) ) ) -> ( ( x L y ) ` i ) = ( A ` i ) )
86 83 84 85 oveq123d 
 |-  ( ( T. /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( i e. ( x H y ) /\ j e. ( y H z ) ) ) -> ( ( ( y L z ) ` j ) ( <. ( ( _I |` B ) ` x ) , ( ( _I |` B ) ` y ) >. .x. ( ( _I |` B ) ` z ) ) ( ( x L y ) ` i ) ) = ( ( A ` j ) ( <. x , y >. .x. z ) ( A ` i ) ) )
87 4 14 62 parhomcl 
 |-  ( ( T. /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( i e. ( x H y ) /\ j e. ( y H z ) ) ) -> i e. K )
88 4 14 70 parhomcl 
 |-  ( ( T. /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( i e. ( x H y ) /\ j e. ( y H z ) ) ) -> j e. K )
89 15 16 58 59 60 61 87 88 parcoval 
 |-  ( ( T. /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( i e. ( x H y ) /\ j e. ( y H z ) ) ) -> ( j ( <. x , y >. .x. z ) i ) = ( j i^i i ) )
90 89 fveq2d 
 |-  ( ( T. /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( i e. ( x H y ) /\ j e. ( y H z ) ) ) -> ( ( x L z ) ` ( j ( <. x , y >. .x. z ) i ) ) = ( ( x L z ) ` ( j i^i i ) ) )
91 4 62 70 12 parhomco 
 |-  ( ( T. /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( i e. ( x H y ) /\ j e. ( y H z ) ) ) -> ( j i^i i ) e. ( x H z ) )
92 5 59 61 91 fvmpomptd 
 |-  ( ( T. /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( i e. ( x H y ) /\ j e. ( y H z ) ) ) -> ( ( x L z ) ` ( j i^i i ) ) = ( A ` ( j i^i i ) ) )
93 90 92 eqtrd 
 |-  ( ( T. /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( i e. ( x H y ) /\ j e. ( y H z ) ) ) -> ( ( x L z ) ` ( j ( <. x , y >. .x. z ) i ) ) = ( A ` ( j i^i i ) ) )
94 4 12 62 70 63 67 74 parmapco 
 |-  ( ( T. /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( i e. ( x H y ) /\ j e. ( y H z ) ) ) -> ( A ` ( j i^i i ) ) = ( ( A ` j ) i^i ( A ` i ) ) )
95 93 94 eqtrd 
 |-  ( ( T. /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( i e. ( x H y ) /\ j e. ( y H z ) ) ) -> ( ( x L z ) ` ( j ( <. x , y >. .x. z ) i ) ) = ( ( A ` j ) i^i ( A ` i ) ) )
96 77 86 95 3eqtr4rd 
 |-  ( ( T. /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( i e. ( x H y ) /\ j e. ( y H z ) ) ) -> ( ( x L z ) ` ( j ( <. x , y >. .x. z ) i ) ) = ( ( ( y L z ) ` j ) ( <. ( ( _I |` B ) ` x ) , ( ( _I |` B ) ` y ) >. .x. ( ( _I |` B ) ` z ) ) ( ( x L y ) ` i ) ) )
97 1 1 2 2 8 8 9 9 18 18 21 23 41 53 96 isfuncd 
 |-  ( T. -> ( _I |` B ) ( C Func C ) L )
98 97 mptru 
 |-  ( _I |` B ) ( C Func C ) L