Metamath Proof Explorer

Theorem catass

Description: Associativity of composition in a category. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses catcocl.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
catcocl.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
catcocl.o ⊢ · = ( comp ‘ 𝐶 )
catcocl.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
catcocl.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
catcocl.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
catcocl.z ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
catcocl.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
catcocl.g ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑌 𝐻 𝑍 ) )
catass.w ⊢ ( 𝜑 → 𝑊 ∈ 𝐵 )
catass.g ⊢ ( 𝜑 → 𝐾 ∈ ( 𝑍 𝐻 𝑊 ) )
Assertion catass ( 𝜑 → ( ( 𝐾 ( ⟨ 𝑌 , 𝑍 ⟩ · 𝑊 ) 𝐺 ) ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑊 ) 𝐹 ) = ( 𝐾 ( ⟨ 𝑋 , 𝑍 ⟩ · 𝑊 ) ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 catcocl.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
2 catcocl.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
3 catcocl.o ⊢ · = ( comp ‘ 𝐶 )
4 catcocl.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
5 catcocl.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6 catcocl.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
7 catcocl.z ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
8 catcocl.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
9 catcocl.g ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑌 𝐻 𝑍 ) )
10 catass.w ⊢ ( 𝜑 → 𝑊 ∈ 𝐵 )
11 catass.g ⊢ ( 𝜑 → 𝐾 ∈ ( 𝑍 𝐻 𝑊 ) )
12 1 2 3 iscat ⊢ ( 𝐶 ∈ Cat → ( 𝐶 ∈ Cat ↔ ∀ 𝑥 ∈ 𝐵 ( ∃ 𝑔 ∈ ( 𝑥 𝐻 𝑥 ) ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 𝑔 ) = 𝑓 ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ∀ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ) ) ) )
13 12 ibi ⊢ ( 𝐶 ∈ Cat → ∀ 𝑥 ∈ 𝐵 ( ∃ 𝑔 ∈ ( 𝑥 𝐻 𝑥 ) ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 𝑔 ) = 𝑓 ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ∀ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ) ) )
14 4 13 syl ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ( ∃ 𝑔 ∈ ( 𝑥 𝐻 𝑥 ) ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 𝑔 ) = 𝑓 ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ∀ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ) ) )
15 6 adantr ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → 𝑌 ∈ 𝐵 )
16 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) → 𝑍 ∈ 𝐵 )
17 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
18 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) → 𝑥 = 𝑋 )
19 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) → 𝑦 = 𝑌 )
20 18 19 oveq12d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) → ( 𝑥 𝐻 𝑦 ) = ( 𝑋 𝐻 𝑌 ) )
21 17 20 eleqtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) → 𝐹 ∈ ( 𝑥 𝐻 𝑦 ) )
22 9 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑓 = 𝐹 ) → 𝐺 ∈ ( 𝑌 𝐻 𝑍 ) )
23 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑓 = 𝐹 ) → 𝑦 = 𝑌 )
24 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑓 = 𝐹 ) → 𝑧 = 𝑍 )
25 23 24 oveq12d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑓 = 𝐹 ) → ( 𝑦 𝐻 𝑧 ) = ( 𝑌 𝐻 𝑍 ) )
26 22 25 eleqtrrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑓 = 𝐹 ) → 𝐺 ∈ ( 𝑦 𝐻 𝑧 ) )
27 10 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → 𝑊 ∈ 𝐵 )
28 11 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) ∧ 𝑤 = 𝑊 ) → 𝐾 ∈ ( 𝑍 𝐻 𝑊 ) )
29 simp-4r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) ∧ 𝑤 = 𝑊 ) → 𝑧 = 𝑍 )
30 simpr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) ∧ 𝑤 = 𝑊 ) → 𝑤 = 𝑊 )
31 29 30 oveq12d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) ∧ 𝑤 = 𝑊 ) → ( 𝑧 𝐻 𝑤 ) = ( 𝑍 𝐻 𝑊 ) )
32 28 31 eleqtrrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) ∧ 𝑤 = 𝑊 ) → 𝐾 ∈ ( 𝑧 𝐻 𝑤 ) )
33 simp-7r ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) → 𝑥 = 𝑋 )
34 simp-6r ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) → 𝑦 = 𝑌 )
35 33 34 opeq12d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑋 , 𝑌 ⟩ )
36 simplr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) → 𝑤 = 𝑊 )
37 35 36 oveq12d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) → ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) = ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑊 ) )
38 simp-5r ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) → 𝑧 = 𝑍 )
39 34 38 opeq12d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) → ⟨ 𝑦 , 𝑧 ⟩ = ⟨ 𝑌 , 𝑍 ⟩ )
40 39 36 oveq12d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) → ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) = ( ⟨ 𝑌 , 𝑍 ⟩ · 𝑊 ) )
41 simpr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) → 𝑘 = 𝐾 )
42 simpllr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) → 𝑔 = 𝐺 )
43 40 41 42 oveq123d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) → ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) = ( 𝐾 ( ⟨ 𝑌 , 𝑍 ⟩ · 𝑊 ) 𝐺 ) )
44 simp-4r ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) → 𝑓 = 𝐹 )
45 37 43 44 oveq123d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) → ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( ( 𝐾 ( ⟨ 𝑌 , 𝑍 ⟩ · 𝑊 ) 𝐺 ) ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑊 ) 𝐹 ) )
46 33 38 opeq12d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) → ⟨ 𝑥 , 𝑧 ⟩ = ⟨ 𝑋 , 𝑍 ⟩ )
47 46 36 oveq12d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) → ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) = ( ⟨ 𝑋 , 𝑍 ⟩ · 𝑊 ) )
48 35 38 oveq12d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) → ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) = ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) )
49 48 42 44 oveq123d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) = ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) )
50 47 41 49 oveq123d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) → ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) = ( 𝐾 ( ⟨ 𝑋 , 𝑍 ⟩ · 𝑊 ) ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ) )
51 45 50 eqeq12d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) → ( ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ↔ ( ( 𝐾 ( ⟨ 𝑌 , 𝑍 ⟩ · 𝑊 ) 𝐺 ) ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑊 ) 𝐹 ) = ( 𝐾 ( ⟨ 𝑋 , 𝑍 ⟩ · 𝑊 ) ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ) ) )
52 32 51 rspcdv ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) ∧ 𝑤 = 𝑊 ) → ( ∀ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) → ( ( 𝐾 ( ⟨ 𝑌 , 𝑍 ⟩ · 𝑊 ) 𝐺 ) ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑊 ) 𝐹 ) = ( 𝐾 ( ⟨ 𝑋 , 𝑍 ⟩ · 𝑊 ) ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ) ) )
53 27 52 rspcimdv ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( ∀ 𝑤 ∈ 𝐵 ∀ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) → ( ( 𝐾 ( ⟨ 𝑌 , 𝑍 ⟩ · 𝑊 ) 𝐺 ) ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑊 ) 𝐹 ) = ( 𝐾 ( ⟨ 𝑋 , 𝑍 ⟩ · 𝑊 ) ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ) ) )
54 53 adantld ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ∀ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ) → ( ( 𝐾 ( ⟨ 𝑌 , 𝑍 ⟩ · 𝑊 ) 𝐺 ) ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑊 ) 𝐹 ) = ( 𝐾 ( ⟨ 𝑋 , 𝑍 ⟩ · 𝑊 ) ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ) ) )
55 26 54 rspcimdv ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑓 = 𝐹 ) → ( ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ∀ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ) → ( ( 𝐾 ( ⟨ 𝑌 , 𝑍 ⟩ · 𝑊 ) 𝐺 ) ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑊 ) 𝐹 ) = ( 𝐾 ( ⟨ 𝑋 , 𝑍 ⟩ · 𝑊 ) ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ) ) )
56 21 55 rspcimdv ⊢ ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) → ( ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ∀ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ) → ( ( 𝐾 ( ⟨ 𝑌 , 𝑍 ⟩ · 𝑊 ) 𝐺 ) ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑊 ) 𝐹 ) = ( 𝐾 ( ⟨ 𝑋 , 𝑍 ⟩ · 𝑊 ) ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ) ) )
57 16 56 rspcimdv ⊢ ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) → ( ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ∀ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ) → ( ( 𝐾 ( ⟨ 𝑌 , 𝑍 ⟩ · 𝑊 ) 𝐺 ) ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑊 ) 𝐹 ) = ( 𝐾 ( ⟨ 𝑋 , 𝑍 ⟩ · 𝑊 ) ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ) ) )
58 15 57 rspcimdv ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ∀ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ) → ( ( 𝐾 ( ⟨ 𝑌 , 𝑍 ⟩ · 𝑊 ) 𝐺 ) ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑊 ) 𝐹 ) = ( 𝐾 ( ⟨ 𝑋 , 𝑍 ⟩ · 𝑊 ) ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ) ) )
59 58 adantld ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( ( ∃ 𝑔 ∈ ( 𝑥 𝐻 𝑥 ) ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 𝑔 ) = 𝑓 ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ∀ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ) ) → ( ( 𝐾 ( ⟨ 𝑌 , 𝑍 ⟩ · 𝑊 ) 𝐺 ) ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑊 ) 𝐹 ) = ( 𝐾 ( ⟨ 𝑋 , 𝑍 ⟩ · 𝑊 ) ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ) ) )
60 5 59 rspcimdv ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐵 ( ∃ 𝑔 ∈ ( 𝑥 𝐻 𝑥 ) ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 𝑔 ) = 𝑓 ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ∀ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ) ) → ( ( 𝐾 ( ⟨ 𝑌 , 𝑍 ⟩ · 𝑊 ) 𝐺 ) ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑊 ) 𝐹 ) = ( 𝐾 ( ⟨ 𝑋 , 𝑍 ⟩ · 𝑊 ) ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ) ) )
61 14 60 mpd ⊢ ( 𝜑 → ( ( 𝐾 ( ⟨ 𝑌 , 𝑍 ⟩ · 𝑊 ) 𝐺 ) ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑊 ) 𝐹 ) = ( 𝐾 ( ⟨ 𝑋 , 𝑍 ⟩ · 𝑊 ) ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ) )