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 ⊢ 𝐵 = ( Base ‘ 𝐷 )
functhinc.c ⊢ 𝐶 = ( Base ‘ 𝐸 )
functhinc.h ⊢ 𝐻 = ( Hom ‘ 𝐷 )
functhinc.j ⊢ 𝐽 = ( Hom ‘ 𝐸 )
functhinc.d ⊢ ( 𝜑 → 𝐷 ∈ Cat )
functhinc.e ⊢ ( 𝜑 → 𝐸 ∈ ThinCat )
functhinc.f ⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ 𝐶 )
functhinc.k ⊢ 𝐾 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 𝐻 𝑦 ) × ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) )
functhinc.1 ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( ( ( 𝐹 ‘ 𝑧 ) 𝐽 ( 𝐹 ‘ 𝑤 ) ) = ∅ → ( 𝑧 𝐻 𝑤 ) = ∅ ) )
functhinclem4.1 ⊢ 1 = ( Id ‘ 𝐷 )
functhinclem4.i ⊢ 𝐼 = ( Id ‘ 𝐸 )
functhinclem4.x ⊢ · = ( comp ‘ 𝐷 )
functhinclem4.o ⊢ 𝑂 = ( comp ‘ 𝐸 )
Assertion functhinclem4 ( ( 𝜑 ∧ 𝐺 = 𝐾 ) → ∀ 𝑎 ∈ 𝐵 ( ( ( 𝑎 𝐺 𝑎 ) ‘ ( 1 ‘ 𝑎 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑎 ) ) ∧ ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑎 𝐻 𝑏 ) ∀ 𝑛 ∈ ( 𝑏 𝐻 𝑐 ) ( ( 𝑎 𝐺 𝑐 ) ‘ ( 𝑛 ( ⟨ 𝑎 , 𝑏 ⟩ · 𝑐 ) 𝑚 ) ) = ( ( ( 𝑏 𝐺 𝑐 ) ‘ 𝑛 ) ( ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑐 ) ) ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑚 ) ) ) )

Proof

Step Hyp Ref Expression
1 functhinc.b ⊢ 𝐵 = ( Base ‘ 𝐷 )
2 functhinc.c ⊢ 𝐶 = ( Base ‘ 𝐸 )
3 functhinc.h ⊢ 𝐻 = ( Hom ‘ 𝐷 )
4 functhinc.j ⊢ 𝐽 = ( Hom ‘ 𝐸 )
5 functhinc.d ⊢ ( 𝜑 → 𝐷 ∈ Cat )
6 functhinc.e ⊢ ( 𝜑 → 𝐸 ∈ ThinCat )
7 functhinc.f ⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ 𝐶 )
8 functhinc.k ⊢ 𝐾 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 𝐻 𝑦 ) × ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) )
9 functhinc.1 ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( ( ( 𝐹 ‘ 𝑧 ) 𝐽 ( 𝐹 ‘ 𝑤 ) ) = ∅ → ( 𝑧 𝐻 𝑤 ) = ∅ ) )
10 functhinclem4.1 ⊢ 1 = ( Id ‘ 𝐷 )
11 functhinclem4.i ⊢ 𝐼 = ( Id ‘ 𝐸 )
12 functhinclem4.x ⊢ · = ( comp ‘ 𝐷 )
13 functhinclem4.o ⊢ 𝑂 = ( comp ‘ 𝐸 )
14 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐺 = 𝐾 ) ∧ 𝑎 ∈ 𝐵 ) → 𝐸 ∈ ThinCat )
15 7 adantr ⊢ ( ( 𝜑 ∧ 𝐺 = 𝐾 ) → 𝐹 : 𝐵 ⟶ 𝐶 )
16 15 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝐺 = 𝐾 ) ∧ 𝑎 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑎 ) ∈ 𝐶 )
17 simpr ⊢ ( ( ( 𝜑 ∧ 𝐺 = 𝐾 ) ∧ 𝑎 ∈ 𝐵 ) → 𝑎 ∈ 𝐵 )
18 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐺 = 𝐾 ) ∧ 𝑎 ∈ 𝐵 ) → 𝐷 ∈ Cat )
19 1 3 10 18 17 catidcl ⊢ ( ( ( 𝜑 ∧ 𝐺 = 𝐾 ) ∧ 𝑎 ∈ 𝐵 ) → ( 1 ‘ 𝑎 ) ∈ ( 𝑎 𝐻 𝑎 ) )
20 simplr ⊢ ( ( ( 𝜑 ∧ 𝐺 = 𝐾 ) ∧ 𝑎 ∈ 𝐵 ) → 𝐺 = 𝐾 )
21 oveq1 ⊢ ( 𝑥 = 𝑣 → ( 𝑥 𝐻 𝑦 ) = ( 𝑣 𝐻 𝑦 ) )
22 fveq2 ⊢ ( 𝑥 = 𝑣 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑣 ) )
23 22 oveq1d ⊢ ( 𝑥 = 𝑣 → ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑣 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) )
24 21 23 xpeq12d ⊢ ( 𝑥 = 𝑣 → ( ( 𝑥 𝐻 𝑦 ) × ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) = ( ( 𝑣 𝐻 𝑦 ) × ( ( 𝐹 ‘ 𝑣 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) )
25 oveq2 ⊢ ( 𝑦 = 𝑢 → ( 𝑣 𝐻 𝑦 ) = ( 𝑣 𝐻 𝑢 ) )
26 fveq2 ⊢ ( 𝑦 = 𝑢 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑢 ) )
27 26 oveq2d ⊢ ( 𝑦 = 𝑢 → ( ( 𝐹 ‘ 𝑣 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑣 ) 𝐽 ( 𝐹 ‘ 𝑢 ) ) )
28 25 27 xpeq12d ⊢ ( 𝑦 = 𝑢 → ( ( 𝑣 𝐻 𝑦 ) × ( ( 𝐹 ‘ 𝑣 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) = ( ( 𝑣 𝐻 𝑢 ) × ( ( 𝐹 ‘ 𝑣 ) 𝐽 ( 𝐹 ‘ 𝑢 ) ) ) )
29 24 28 cbvmpov ⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 𝐻 𝑦 ) × ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) ) = ( 𝑣 ∈ 𝐵 , 𝑢 ∈ 𝐵 ↦ ( ( 𝑣 𝐻 𝑢 ) × ( ( 𝐹 ‘ 𝑣 ) 𝐽 ( 𝐹 ‘ 𝑢 ) ) ) )
30 8 29 eqtri ⊢ 𝐾 = ( 𝑣 ∈ 𝐵 , 𝑢 ∈ 𝐵 ↦ ( ( 𝑣 𝐻 𝑢 ) × ( ( 𝐹 ‘ 𝑣 ) 𝐽 ( 𝐹 ‘ 𝑢 ) ) ) )
31 20 30 eqtrdi ⊢ ( ( ( 𝜑 ∧ 𝐺 = 𝐾 ) ∧ 𝑎 ∈ 𝐵 ) → 𝐺 = ( 𝑣 ∈ 𝐵 , 𝑢 ∈ 𝐵 ↦ ( ( 𝑣 𝐻 𝑢 ) × ( ( 𝐹 ‘ 𝑣 ) 𝐽 ( 𝐹 ‘ 𝑢 ) ) ) ) )
32 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐺 = 𝐾 ) ∧ 𝑎 ∈ 𝐵 ) → ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( ( ( 𝐹 ‘ 𝑧 ) 𝐽 ( 𝐹 ‘ 𝑤 ) ) = ∅ → ( 𝑧 𝐻 𝑤 ) = ∅ ) )
33 17 17 32 functhinclem2 ⊢ ( ( ( 𝜑 ∧ 𝐺 = 𝐾 ) ∧ 𝑎 ∈ 𝐵 ) → ( ( ( 𝐹 ‘ 𝑎 ) 𝐽 ( 𝐹 ‘ 𝑎 ) ) = ∅ → ( 𝑎 𝐻 𝑎 ) = ∅ ) )
34 14 16 16 2 4 thincmo ⊢ ( ( ( 𝜑 ∧ 𝐺 = 𝐾 ) ∧ 𝑎 ∈ 𝐵 ) → ∃* 𝑝 𝑝 ∈ ( ( 𝐹 ‘ 𝑎 ) 𝐽 ( 𝐹 ‘ 𝑎 ) ) )
35 17 17 19 31 33 34 functhinclem3 ⊢ ( ( ( 𝜑 ∧ 𝐺 = 𝐾 ) ∧ 𝑎 ∈ 𝐵 ) → ( ( 𝑎 𝐺 𝑎 ) ‘ ( 1 ‘ 𝑎 ) ) ∈ ( ( 𝐹 ‘ 𝑎 ) 𝐽 ( 𝐹 ‘ 𝑎 ) ) )
36 14 2 4 16 11 35 thincid ⊢ ( ( ( 𝜑 ∧ 𝐺 = 𝐾 ) ∧ 𝑎 ∈ 𝐵 ) → ( ( 𝑎 𝐺 𝑎 ) ‘ ( 1 ‘ 𝑎 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑎 ) ) )
37 16 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐺 = 𝐾 ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) ∧ ( 𝑚 ∈ ( 𝑎 𝐻 𝑏 ) ∧ 𝑛 ∈ ( 𝑏 𝐻 𝑐 ) ) ) → ( 𝐹 ‘ 𝑎 ) ∈ 𝐶 )
38 7 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐺 = 𝐾 ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) ∧ ( 𝑚 ∈ ( 𝑎 𝐻 𝑏 ) ∧ 𝑛 ∈ ( 𝑏 𝐻 𝑐 ) ) ) → 𝐹 : 𝐵 ⟶ 𝐶 )
39 simplrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐺 = 𝐾 ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) ∧ ( 𝑚 ∈ ( 𝑎 𝐻 𝑏 ) ∧ 𝑛 ∈ ( 𝑏 𝐻 𝑐 ) ) ) → 𝑐 ∈ 𝐵 )
40 38 39 ffvelcdmd ⊢ ( ( ( ( ( 𝜑 ∧ 𝐺 = 𝐾 ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) ∧ ( 𝑚 ∈ ( 𝑎 𝐻 𝑏 ) ∧ 𝑛 ∈ ( 𝑏 𝐻 𝑐 ) ) ) → ( 𝐹 ‘ 𝑐 ) ∈ 𝐶 )
41 17 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐺 = 𝐾 ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) ∧ ( 𝑚 ∈ ( 𝑎 𝐻 𝑏 ) ∧ 𝑛 ∈ ( 𝑏 𝐻 𝑐 ) ) ) → 𝑎 ∈ 𝐵 )
42 5 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐺 = 𝐾 ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) ∧ ( 𝑚 ∈ ( 𝑎 𝐻 𝑏 ) ∧ 𝑛 ∈ ( 𝑏 𝐻 𝑐 ) ) ) → 𝐷 ∈ Cat )
43 simplrl ⊢ ( ( ( ( ( 𝜑 ∧ 𝐺 = 𝐾 ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) ∧ ( 𝑚 ∈ ( 𝑎 𝐻 𝑏 ) ∧ 𝑛 ∈ ( 𝑏 𝐻 𝑐 ) ) ) → 𝑏 ∈ 𝐵 )
44 simprl ⊢ ( ( ( ( ( 𝜑 ∧ 𝐺 = 𝐾 ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) ∧ ( 𝑚 ∈ ( 𝑎 𝐻 𝑏 ) ∧ 𝑛 ∈ ( 𝑏 𝐻 𝑐 ) ) ) → 𝑚 ∈ ( 𝑎 𝐻 𝑏 ) )
45 simprr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐺 = 𝐾 ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) ∧ ( 𝑚 ∈ ( 𝑎 𝐻 𝑏 ) ∧ 𝑛 ∈ ( 𝑏 𝐻 𝑐 ) ) ) → 𝑛 ∈ ( 𝑏 𝐻 𝑐 ) )
46 1 3 12 42 41 43 39 44 45 catcocl ⊢ ( ( ( ( ( 𝜑 ∧ 𝐺 = 𝐾 ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) ∧ ( 𝑚 ∈ ( 𝑎 𝐻 𝑏 ) ∧ 𝑛 ∈ ( 𝑏 𝐻 𝑐 ) ) ) → ( 𝑛 ( ⟨ 𝑎 , 𝑏 ⟩ · 𝑐 ) 𝑚 ) ∈ ( 𝑎 𝐻 𝑐 ) )
47 31 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐺 = 𝐾 ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) ∧ ( 𝑚 ∈ ( 𝑎 𝐻 𝑏 ) ∧ 𝑛 ∈ ( 𝑏 𝐻 𝑐 ) ) ) → 𝐺 = ( 𝑣 ∈ 𝐵 , 𝑢 ∈ 𝐵 ↦ ( ( 𝑣 𝐻 𝑢 ) × ( ( 𝐹 ‘ 𝑣 ) 𝐽 ( 𝐹 ‘ 𝑢 ) ) ) ) )
48 9 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐺 = 𝐾 ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) ∧ ( 𝑚 ∈ ( 𝑎 𝐻 𝑏 ) ∧ 𝑛 ∈ ( 𝑏 𝐻 𝑐 ) ) ) → ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( ( ( 𝐹 ‘ 𝑧 ) 𝐽 ( 𝐹 ‘ 𝑤 ) ) = ∅ → ( 𝑧 𝐻 𝑤 ) = ∅ ) )
49 41 39 48 functhinclem2 ⊢ ( ( ( ( ( 𝜑 ∧ 𝐺 = 𝐾 ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) ∧ ( 𝑚 ∈ ( 𝑎 𝐻 𝑏 ) ∧ 𝑛 ∈ ( 𝑏 𝐻 𝑐 ) ) ) → ( ( ( 𝐹 ‘ 𝑎 ) 𝐽 ( 𝐹 ‘ 𝑐 ) ) = ∅ → ( 𝑎 𝐻 𝑐 ) = ∅ ) )
50 6 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐺 = 𝐾 ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) ∧ ( 𝑚 ∈ ( 𝑎 𝐻 𝑏 ) ∧ 𝑛 ∈ ( 𝑏 𝐻 𝑐 ) ) ) → 𝐸 ∈ ThinCat )
51 50 37 40 2 4 thincmo ⊢ ( ( ( ( ( 𝜑 ∧ 𝐺 = 𝐾 ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) ∧ ( 𝑚 ∈ ( 𝑎 𝐻 𝑏 ) ∧ 𝑛 ∈ ( 𝑏 𝐻 𝑐 ) ) ) → ∃* 𝑝 𝑝 ∈ ( ( 𝐹 ‘ 𝑎 ) 𝐽 ( 𝐹 ‘ 𝑐 ) ) )
52 41 39 46 47 49 51 functhinclem3 ⊢ ( ( ( ( ( 𝜑 ∧ 𝐺 = 𝐾 ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) ∧ ( 𝑚 ∈ ( 𝑎 𝐻 𝑏 ) ∧ 𝑛 ∈ ( 𝑏 𝐻 𝑐 ) ) ) → ( ( 𝑎 𝐺 𝑐 ) ‘ ( 𝑛 ( ⟨ 𝑎 , 𝑏 ⟩ · 𝑐 ) 𝑚 ) ) ∈ ( ( 𝐹 ‘ 𝑎 ) 𝐽 ( 𝐹 ‘ 𝑐 ) ) )
53 14 thinccatd ⊢ ( ( ( 𝜑 ∧ 𝐺 = 𝐾 ) ∧ 𝑎 ∈ 𝐵 ) → 𝐸 ∈ Cat )
54 53 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐺 = 𝐾 ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) ∧ ( 𝑚 ∈ ( 𝑎 𝐻 𝑏 ) ∧ 𝑛 ∈ ( 𝑏 𝐻 𝑐 ) ) ) → 𝐸 ∈ Cat )
55 38 43 ffvelcdmd ⊢ ( ( ( ( ( 𝜑 ∧ 𝐺 = 𝐾 ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) ∧ ( 𝑚 ∈ ( 𝑎 𝐻 𝑏 ) ∧ 𝑛 ∈ ( 𝑏 𝐻 𝑐 ) ) ) → ( 𝐹 ‘ 𝑏 ) ∈ 𝐶 )
56 41 43 48 functhinclem2 ⊢ ( ( ( ( ( 𝜑 ∧ 𝐺 = 𝐾 ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) ∧ ( 𝑚 ∈ ( 𝑎 𝐻 𝑏 ) ∧ 𝑛 ∈ ( 𝑏 𝐻 𝑐 ) ) ) → ( ( ( 𝐹 ‘ 𝑎 ) 𝐽 ( 𝐹 ‘ 𝑏 ) ) = ∅ → ( 𝑎 𝐻 𝑏 ) = ∅ ) )
57 50 37 55 2 4 thincmo ⊢ ( ( ( ( ( 𝜑 ∧ 𝐺 = 𝐾 ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) ∧ ( 𝑚 ∈ ( 𝑎 𝐻 𝑏 ) ∧ 𝑛 ∈ ( 𝑏 𝐻 𝑐 ) ) ) → ∃* 𝑝 𝑝 ∈ ( ( 𝐹 ‘ 𝑎 ) 𝐽 ( 𝐹 ‘ 𝑏 ) ) )
58 41 43 44 47 56 57 functhinclem3 ⊢ ( ( ( ( ( 𝜑 ∧ 𝐺 = 𝐾 ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) ∧ ( 𝑚 ∈ ( 𝑎 𝐻 𝑏 ) ∧ 𝑛 ∈ ( 𝑏 𝐻 𝑐 ) ) ) → ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑚 ) ∈ ( ( 𝐹 ‘ 𝑎 ) 𝐽 ( 𝐹 ‘ 𝑏 ) ) )
59 43 39 48 functhinclem2 ⊢ ( ( ( ( ( 𝜑 ∧ 𝐺 = 𝐾 ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) ∧ ( 𝑚 ∈ ( 𝑎 𝐻 𝑏 ) ∧ 𝑛 ∈ ( 𝑏 𝐻 𝑐 ) ) ) → ( ( ( 𝐹 ‘ 𝑏 ) 𝐽 ( 𝐹 ‘ 𝑐 ) ) = ∅ → ( 𝑏 𝐻 𝑐 ) = ∅ ) )
60 50 55 40 2 4 thincmo ⊢ ( ( ( ( ( 𝜑 ∧ 𝐺 = 𝐾 ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) ∧ ( 𝑚 ∈ ( 𝑎 𝐻 𝑏 ) ∧ 𝑛 ∈ ( 𝑏 𝐻 𝑐 ) ) ) → ∃* 𝑝 𝑝 ∈ ( ( 𝐹 ‘ 𝑏 ) 𝐽 ( 𝐹 ‘ 𝑐 ) ) )
61 43 39 45 47 59 60 functhinclem3 ⊢ ( ( ( ( ( 𝜑 ∧ 𝐺 = 𝐾 ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) ∧ ( 𝑚 ∈ ( 𝑎 𝐻 𝑏 ) ∧ 𝑛 ∈ ( 𝑏 𝐻 𝑐 ) ) ) → ( ( 𝑏 𝐺 𝑐 ) ‘ 𝑛 ) ∈ ( ( 𝐹 ‘ 𝑏 ) 𝐽 ( 𝐹 ‘ 𝑐 ) ) )
62 2 4 13 54 37 55 40 58 61 catcocl ⊢ ( ( ( ( ( 𝜑 ∧ 𝐺 = 𝐾 ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) ∧ ( 𝑚 ∈ ( 𝑎 𝐻 𝑏 ) ∧ 𝑛 ∈ ( 𝑏 𝐻 𝑐 ) ) ) → ( ( ( 𝑏 𝐺 𝑐 ) ‘ 𝑛 ) ( ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑐 ) ) ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑚 ) ) ∈ ( ( 𝐹 ‘ 𝑎 ) 𝐽 ( 𝐹 ‘ 𝑐 ) ) )
63 37 40 52 62 2 4 50 thincmo2 ⊢ ( ( ( ( ( 𝜑 ∧ 𝐺 = 𝐾 ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) ∧ ( 𝑚 ∈ ( 𝑎 𝐻 𝑏 ) ∧ 𝑛 ∈ ( 𝑏 𝐻 𝑐 ) ) ) → ( ( 𝑎 𝐺 𝑐 ) ‘ ( 𝑛 ( ⟨ 𝑎 , 𝑏 ⟩ · 𝑐 ) 𝑚 ) ) = ( ( ( 𝑏 𝐺 𝑐 ) ‘ 𝑛 ) ( ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑐 ) ) ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑚 ) ) )
64 63 ralrimivva ⊢ ( ( ( ( 𝜑 ∧ 𝐺 = 𝐾 ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → ∀ 𝑚 ∈ ( 𝑎 𝐻 𝑏 ) ∀ 𝑛 ∈ ( 𝑏 𝐻 𝑐 ) ( ( 𝑎 𝐺 𝑐 ) ‘ ( 𝑛 ( ⟨ 𝑎 , 𝑏 ⟩ · 𝑐 ) 𝑚 ) ) = ( ( ( 𝑏 𝐺 𝑐 ) ‘ 𝑛 ) ( ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑐 ) ) ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑚 ) ) )
65 64 ralrimivva ⊢ ( ( ( 𝜑 ∧ 𝐺 = 𝐾 ) ∧ 𝑎 ∈ 𝐵 ) → ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑎 𝐻 𝑏 ) ∀ 𝑛 ∈ ( 𝑏 𝐻 𝑐 ) ( ( 𝑎 𝐺 𝑐 ) ‘ ( 𝑛 ( ⟨ 𝑎 , 𝑏 ⟩ · 𝑐 ) 𝑚 ) ) = ( ( ( 𝑏 𝐺 𝑐 ) ‘ 𝑛 ) ( ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑐 ) ) ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑚 ) ) )
66 36 65 jca ⊢ ( ( ( 𝜑 ∧ 𝐺 = 𝐾 ) ∧ 𝑎 ∈ 𝐵 ) → ( ( ( 𝑎 𝐺 𝑎 ) ‘ ( 1 ‘ 𝑎 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑎 ) ) ∧ ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑎 𝐻 𝑏 ) ∀ 𝑛 ∈ ( 𝑏 𝐻 𝑐 ) ( ( 𝑎 𝐺 𝑐 ) ‘ ( 𝑛 ( ⟨ 𝑎 , 𝑏 ⟩ · 𝑐 ) 𝑚 ) ) = ( ( ( 𝑏 𝐺 𝑐 ) ‘ 𝑛 ) ( ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑐 ) ) ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑚 ) ) ) )
67 66 ralrimiva ⊢ ( ( 𝜑 ∧ 𝐺 = 𝐾 ) → ∀ 𝑎 ∈ 𝐵 ( ( ( 𝑎 𝐺 𝑎 ) ‘ ( 1 ‘ 𝑎 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑎 ) ) ∧ ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑎 𝐻 𝑏 ) ∀ 𝑛 ∈ ( 𝑏 𝐻 𝑐 ) ( ( 𝑎 𝐺 𝑐 ) ‘ ( 𝑛 ( ⟨ 𝑎 , 𝑏 ⟩ · 𝑐 ) 𝑚 ) ) = ( ( ( 𝑏 𝐺 𝑐 ) ‘ 𝑛 ) ( ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑐 ) ) ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑚 ) ) ) )