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 ⊢ 𝐵 = ( Base ‘ 𝐶 )
parmapfunc.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
parmapfunc.c ⊢ 𝐶 ∈ Cat
parmapfunc.hv ⊢ 𝐻 = ( 𝑟 ∈ 𝐵 , 𝑠 ∈ 𝐵 ↦ if ( 𝑟 = 𝑠 , { 𝐽 } , if ( ( 𝑟 = 𝑋 ∧ 𝑠 = 𝑌 ) , 𝑆 , ∅ ) ) )
parmapfunc.l ⊢ 𝐿 = ( 𝑢 ∈ 𝐵 , 𝑣 ∈ 𝐵 ↦ ( 𝑎 ∈ ( 𝑢 𝐻 𝑣 ) ↦ ( 𝐴 ‘ 𝑎 ) ) )
parmapfunc.ai ⊢ ( 𝐴 ‘ 𝐽 ) = 𝐽
parmapfunc.as ⊢ ∀ 𝑡 ∈ 𝑆 ( 𝐴 ‘ 𝑡 ) ∈ 𝑆
parmapfunc2.i ⊢ 𝐼 = ( Id ‘ 𝐶 )
parmapfunc2.o ⊢ · = ( comp ‘ 𝐶 )
parmapfunc2.s ⊢ 𝑆 ∈ V
parmapfunc2.j ⊢ 𝐽 ∈ V
parmapfunc2.p ⊢ 𝑆 ⊆ 𝒫 𝐽
parmapfunc2.n ⊢ 𝑋 ≠ 𝑌
parmapfunc2.k ⊢ 𝐾 = ( 𝑆 ∪ { 𝐽 } )
parmapfunc2.mv ⊢ 𝑀 = ( 𝑓 ∈ 𝐾 , 𝑔 ∈ 𝐾 ↦ ( 𝑓 ∩ 𝑔 ) )
parmapfunc2.ov ⊢ · = ( 𝑝 ∈ ( 𝐵 × 𝐵 ) , 𝑞 ∈ 𝐵 ↦ 𝑀 )
parmapfunc2.iv ⊢ 𝐼 = ( 𝑡 ∈ 𝐵 ↦ 𝐽 )
Assertion parmapfunc2 ( I ↾ 𝐵 ) ( 𝐶 Func 𝐶 ) 𝐿

Proof

Step Hyp Ref Expression
1 parmapfunc.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
2 parmapfunc.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
3 parmapfunc.c ⊢ 𝐶 ∈ Cat
4 parmapfunc.hv ⊢ 𝐻 = ( 𝑟 ∈ 𝐵 , 𝑠 ∈ 𝐵 ↦ if ( 𝑟 = 𝑠 , { 𝐽 } , if ( ( 𝑟 = 𝑋 ∧ 𝑠 = 𝑌 ) , 𝑆 , ∅ ) ) )
5 parmapfunc.l ⊢ 𝐿 = ( 𝑢 ∈ 𝐵 , 𝑣 ∈ 𝐵 ↦ ( 𝑎 ∈ ( 𝑢 𝐻 𝑣 ) ↦ ( 𝐴 ‘ 𝑎 ) ) )
6 parmapfunc.ai ⊢ ( 𝐴 ‘ 𝐽 ) = 𝐽
7 parmapfunc.as ⊢ ∀ 𝑡 ∈ 𝑆 ( 𝐴 ‘ 𝑡 ) ∈ 𝑆
8 parmapfunc2.i ⊢ 𝐼 = ( Id ‘ 𝐶 )
9 parmapfunc2.o ⊢ · = ( comp ‘ 𝐶 )
10 parmapfunc2.s ⊢ 𝑆 ∈ V
11 parmapfunc2.j ⊢ 𝐽 ∈ V
12 parmapfunc2.p ⊢ 𝑆 ⊆ 𝒫 𝐽
13 parmapfunc2.n ⊢ 𝑋 ≠ 𝑌
14 parmapfunc2.k ⊢ 𝐾 = ( 𝑆 ∪ { 𝐽 } )
15 parmapfunc2.mv ⊢ 𝑀 = ( 𝑓 ∈ 𝐾 , 𝑔 ∈ 𝐾 ↦ ( 𝑓 ∩ 𝑔 ) )
16 parmapfunc2.ov ⊢ · = ( 𝑝 ∈ ( 𝐵 × 𝐵 ) , 𝑞 ∈ 𝐵 ↦ 𝑀 )
17 parmapfunc2.iv ⊢ 𝐼 = ( 𝑡 ∈ 𝐵 ↦ 𝐽 )
18 3 a1i ⊢ ( ⊤ → 𝐶 ∈ Cat )
19 f1oi ⊢ ( I ↾ 𝐵 ) : 𝐵 –1-1-onto→ 𝐵
20 f1of ⊢ ( ( I ↾ 𝐵 ) : 𝐵 –1-1-onto→ 𝐵 → ( I ↾ 𝐵 ) : 𝐵 ⟶ 𝐵 )
21 19 20 mp1i ⊢ ( ⊤ → ( I ↾ 𝐵 ) : 𝐵 ⟶ 𝐵 )
22 5 fnmpompt ⊢ 𝐿 Fn ( 𝐵 × 𝐵 )
23 22 a1i ⊢ ( ⊤ → 𝐿 Fn ( 𝐵 × 𝐵 ) )
24 simprl ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑥 ∈ 𝐵 )
25 simprr ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑦 ∈ 𝐵 )
26 5 24 25 ovmpomptd ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 𝐿 𝑦 ) = ( 𝑎 ∈ ( 𝑥 𝐻 𝑦 ) ↦ ( 𝐴 ‘ 𝑎 ) ) )
27 simpr ⊢ ( ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑎 ∈ ( 𝑥 𝐻 𝑦 ) ) → 𝑎 ∈ ( 𝑥 𝐻 𝑦 ) )
28 6 a1i ⊢ ( ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑎 ∈ ( 𝑥 𝐻 𝑦 ) ) → ( 𝐴 ‘ 𝐽 ) = 𝐽 )
29 fveq2 ⊢ ( 𝑡 = 𝑎 → ( 𝐴 ‘ 𝑡 ) = ( 𝐴 ‘ 𝑎 ) )
30 29 eleq1d ⊢ ( 𝑡 = 𝑎 → ( ( 𝐴 ‘ 𝑡 ) ∈ 𝑆 ↔ ( 𝐴 ‘ 𝑎 ) ∈ 𝑆 ) )
31 30 7 vtoclri ⊢ ( 𝑎 ∈ 𝑆 → ( 𝐴 ‘ 𝑎 ) ∈ 𝑆 )
32 31 adantl ⊢ ( ( ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑎 ∈ ( 𝑥 𝐻 𝑦 ) ) ∧ 𝑎 ∈ 𝑆 ) → ( 𝐴 ‘ 𝑎 ) ∈ 𝑆 )
33 4 27 28 32 parmapcl ⊢ ( ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑎 ∈ ( 𝑥 𝐻 𝑦 ) ) → ( 𝐴 ‘ 𝑎 ) ∈ ( 𝑥 𝐻 𝑦 ) )
34 26 33 fmpt3d ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 𝐿 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( 𝑥 𝐻 𝑦 ) )
35 fvresi ⊢ ( 𝑥 ∈ 𝐵 → ( ( I ↾ 𝐵 ) ‘ 𝑥 ) = 𝑥 )
36 24 35 syl ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( I ↾ 𝐵 ) ‘ 𝑥 ) = 𝑥 )
37 fvresi ⊢ ( 𝑦 ∈ 𝐵 → ( ( I ↾ 𝐵 ) ‘ 𝑦 ) = 𝑦 )
38 25 37 syl ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( I ↾ 𝐵 ) ‘ 𝑦 ) = 𝑦 )
39 36 38 oveq12d ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( ( I ↾ 𝐵 ) ‘ 𝑥 ) 𝐻 ( ( I ↾ 𝐵 ) ‘ 𝑦 ) ) = ( 𝑥 𝐻 𝑦 ) )
40 39 feq3d ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑥 𝐿 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( ( ( I ↾ 𝐵 ) ‘ 𝑥 ) 𝐻 ( ( I ↾ 𝐵 ) ‘ 𝑦 ) ) ↔ ( 𝑥 𝐿 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( 𝑥 𝐻 𝑦 ) ) )
41 34 40 mpbird ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 𝐿 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( ( ( I ↾ 𝐵 ) ‘ 𝑥 ) 𝐻 ( ( I ↾ 𝐵 ) ‘ 𝑦 ) ) )
42 eqidd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑡 = 𝑥 ) → 𝐽 = 𝐽 )
43 simpr ⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
44 11 a1i ⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐵 ) → 𝐽 ∈ V )
45 17 42 43 44 fvmptd2 ⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐵 ) → ( 𝐼 ‘ 𝑥 ) = 𝐽 )
46 45 fveq2d ⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑥 𝐿 𝑥 ) ‘ ( 𝐼 ‘ 𝑥 ) ) = ( ( 𝑥 𝐿 𝑥 ) ‘ 𝐽 ) )
47 4 11 43 parhomid ⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐵 ) → 𝐽 ∈ ( 𝑥 𝐻 𝑥 ) )
48 5 43 43 47 fvmpomptd ⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑥 𝐿 𝑥 ) ‘ 𝐽 ) = ( 𝐴 ‘ 𝐽 ) )
49 46 48 eqtrd ⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑥 𝐿 𝑥 ) ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝐴 ‘ 𝐽 ) )
50 35 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐵 ) → ( ( I ↾ 𝐵 ) ‘ 𝑥 ) = 𝑥 )
51 50 fveq2d ⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐵 ) → ( 𝐼 ‘ ( ( I ↾ 𝐵 ) ‘ 𝑥 ) ) = ( 𝐼 ‘ 𝑥 ) )
52 51 45 eqtrd ⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐵 ) → ( 𝐼 ‘ ( ( I ↾ 𝐵 ) ‘ 𝑥 ) ) = 𝐽 )
53 6 49 52 3eqtr4a ⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑥 𝐿 𝑥 ) ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( ( I ↾ 𝐵 ) ‘ 𝑥 ) ) )
54 snex ⊢ { 𝐽 } ∈ V
55 10 54 unex ⊢ ( 𝑆 ∪ { 𝐽 } ) ∈ V
56 14 55 eqeltri ⊢ 𝐾 ∈ V
57 56 56 mpoex ⊢ ( 𝑓 ∈ 𝐾 , 𝑔 ∈ 𝐾 ↦ ( 𝑓 ∩ 𝑔 ) ) ∈ V
58 15 57 eqeltri ⊢ 𝑀 ∈ V
59 simp21 ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑖 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑗 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → 𝑥 ∈ 𝐵 )
60 simp22 ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑖 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑗 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → 𝑦 ∈ 𝐵 )
61 simp23 ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑖 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑗 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → 𝑧 ∈ 𝐵 )
62 simp3l ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑖 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑗 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → 𝑖 ∈ ( 𝑥 𝐻 𝑦 ) )
63 6 a1i ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑖 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑗 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( 𝐴 ‘ 𝐽 ) = 𝐽 )
64 fveq2 ⊢ ( 𝑡 = 𝑖 → ( 𝐴 ‘ 𝑡 ) = ( 𝐴 ‘ 𝑖 ) )
65 64 eleq1d ⊢ ( 𝑡 = 𝑖 → ( ( 𝐴 ‘ 𝑡 ) ∈ 𝑆 ↔ ( 𝐴 ‘ 𝑖 ) ∈ 𝑆 ) )
66 65 7 vtoclri ⊢ ( 𝑖 ∈ 𝑆 → ( 𝐴 ‘ 𝑖 ) ∈ 𝑆 )
67 66 adantl ⊢ ( ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑖 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑗 ∈ ( 𝑦 𝐻 𝑧 ) ) ) ∧ 𝑖 ∈ 𝑆 ) → ( 𝐴 ‘ 𝑖 ) ∈ 𝑆 )
68 4 62 63 67 parmapcl ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑖 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑗 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( 𝐴 ‘ 𝑖 ) ∈ ( 𝑥 𝐻 𝑦 ) )
69 4 14 68 parhomcl ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑖 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑗 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( 𝐴 ‘ 𝑖 ) ∈ 𝐾 )
70 simp3r ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑖 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑗 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → 𝑗 ∈ ( 𝑦 𝐻 𝑧 ) )
71 fveq2 ⊢ ( 𝑡 = 𝑗 → ( 𝐴 ‘ 𝑡 ) = ( 𝐴 ‘ 𝑗 ) )
72 71 eleq1d ⊢ ( 𝑡 = 𝑗 → ( ( 𝐴 ‘ 𝑡 ) ∈ 𝑆 ↔ ( 𝐴 ‘ 𝑗 ) ∈ 𝑆 ) )
73 72 7 vtoclri ⊢ ( 𝑗 ∈ 𝑆 → ( 𝐴 ‘ 𝑗 ) ∈ 𝑆 )
74 73 adantl ⊢ ( ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑖 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑗 ∈ ( 𝑦 𝐻 𝑧 ) ) ) ∧ 𝑗 ∈ 𝑆 ) → ( 𝐴 ‘ 𝑗 ) ∈ 𝑆 )
75 4 70 63 74 parmapcl ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑖 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑗 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( 𝐴 ‘ 𝑗 ) ∈ ( 𝑦 𝐻 𝑧 ) )
76 4 14 75 parhomcl ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑖 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑗 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( 𝐴 ‘ 𝑗 ) ∈ 𝐾 )
77 15 16 58 59 60 61 69 76 parcoval ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑖 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑗 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( ( 𝐴 ‘ 𝑗 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) ( 𝐴 ‘ 𝑖 ) ) = ( ( 𝐴 ‘ 𝑗 ) ∩ ( 𝐴 ‘ 𝑖 ) ) )
78 59 35 syl ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑖 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑗 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( ( I ↾ 𝐵 ) ‘ 𝑥 ) = 𝑥 )
79 60 37 syl ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑖 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑗 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( ( I ↾ 𝐵 ) ‘ 𝑦 ) = 𝑦 )
80 78 79 opeq12d ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑖 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑗 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ⟨ ( ( I ↾ 𝐵 ) ‘ 𝑥 ) , ( ( I ↾ 𝐵 ) ‘ 𝑦 ) ⟩ = ⟨ 𝑥 , 𝑦 ⟩ )
81 fvresi ⊢ ( 𝑧 ∈ 𝐵 → ( ( I ↾ 𝐵 ) ‘ 𝑧 ) = 𝑧 )
82 61 81 syl ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑖 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑗 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( ( I ↾ 𝐵 ) ‘ 𝑧 ) = 𝑧 )
83 80 82 oveq12d ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑖 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑗 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( ⟨ ( ( I ↾ 𝐵 ) ‘ 𝑥 ) , ( ( I ↾ 𝐵 ) ‘ 𝑦 ) ⟩ · ( ( I ↾ 𝐵 ) ‘ 𝑧 ) ) = ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) )
84 5 60 61 70 fvmpomptd ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑖 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑗 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( ( 𝑦 𝐿 𝑧 ) ‘ 𝑗 ) = ( 𝐴 ‘ 𝑗 ) )
85 5 59 60 62 fvmpomptd ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑖 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑗 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( ( 𝑥 𝐿 𝑦 ) ‘ 𝑖 ) = ( 𝐴 ‘ 𝑖 ) )
86 83 84 85 oveq123d ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑖 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑗 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( ( ( 𝑦 𝐿 𝑧 ) ‘ 𝑗 ) ( ⟨ ( ( I ↾ 𝐵 ) ‘ 𝑥 ) , ( ( I ↾ 𝐵 ) ‘ 𝑦 ) ⟩ · ( ( I ↾ 𝐵 ) ‘ 𝑧 ) ) ( ( 𝑥 𝐿 𝑦 ) ‘ 𝑖 ) ) = ( ( 𝐴 ‘ 𝑗 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) ( 𝐴 ‘ 𝑖 ) ) )
87 4 14 62 parhomcl ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑖 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑗 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → 𝑖 ∈ 𝐾 )
88 4 14 70 parhomcl ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑖 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑗 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → 𝑗 ∈ 𝐾 )
89 15 16 58 59 60 61 87 88 parcoval ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑖 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑗 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( 𝑗 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑖 ) = ( 𝑗 ∩ 𝑖 ) )
90 89 fveq2d ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑖 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑗 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( ( 𝑥 𝐿 𝑧 ) ‘ ( 𝑗 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑖 ) ) = ( ( 𝑥 𝐿 𝑧 ) ‘ ( 𝑗 ∩ 𝑖 ) ) )
91 4 62 70 12 parhomco ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑖 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑗 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( 𝑗 ∩ 𝑖 ) ∈ ( 𝑥 𝐻 𝑧 ) )
92 5 59 61 91 fvmpomptd ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑖 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑗 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( ( 𝑥 𝐿 𝑧 ) ‘ ( 𝑗 ∩ 𝑖 ) ) = ( 𝐴 ‘ ( 𝑗 ∩ 𝑖 ) ) )
93 90 92 eqtrd ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑖 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑗 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( ( 𝑥 𝐿 𝑧 ) ‘ ( 𝑗 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑖 ) ) = ( 𝐴 ‘ ( 𝑗 ∩ 𝑖 ) ) )
94 4 12 62 70 63 67 74 parmapco ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑖 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑗 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( 𝐴 ‘ ( 𝑗 ∩ 𝑖 ) ) = ( ( 𝐴 ‘ 𝑗 ) ∩ ( 𝐴 ‘ 𝑖 ) ) )
95 93 94 eqtrd ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑖 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑗 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( ( 𝑥 𝐿 𝑧 ) ‘ ( 𝑗 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑖 ) ) = ( ( 𝐴 ‘ 𝑗 ) ∩ ( 𝐴 ‘ 𝑖 ) ) )
96 77 86 95 3eqtr4rd ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑖 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑗 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( ( 𝑥 𝐿 𝑧 ) ‘ ( 𝑗 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑖 ) ) = ( ( ( 𝑦 𝐿 𝑧 ) ‘ 𝑗 ) ( ⟨ ( ( I ↾ 𝐵 ) ‘ 𝑥 ) , ( ( I ↾ 𝐵 ) ‘ 𝑦 ) ⟩ · ( ( I ↾ 𝐵 ) ‘ 𝑧 ) ) ( ( 𝑥 𝐿 𝑦 ) ‘ 𝑖 ) ) )
97 1 1 2 2 8 8 9 9 18 18 21 23 41 53 96 isfuncd ⊢ ( ⊤ → ( I ↾ 𝐵 ) ( 𝐶 Func 𝐶 ) 𝐿 )
98 97 mptru ⊢ ( I ↾ 𝐵 ) ( 𝐶 Func 𝐶 ) 𝐿