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	⊢ ( 𝜑 → ( ( 𝐾 ( ⟨ 𝑌 , 𝑍 ⟩ · 𝑊 ) 𝐺 ) ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑊 ) 𝐹 ) = ( 𝐾 ( ⟨ 𝑋 , 𝑍 ⟩ · 𝑊 ) ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ) )