Theorem catcocl

Description: Closure of a composition arrow. (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	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑌 𝐻 𝑍 ) )
Assertion	catcocl	⊢ ( 𝜑 → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ∈ ( 𝑋 𝐻 𝑍 ) )

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	1 2 3	iscat	⊢ ( 𝐶 ∈ Cat → ( 𝐶 ∈ Cat ↔ ∀ 𝑥 ∈ 𝐵 ( ∃ 𝑔 ∈ ( 𝑥 𝐻 𝑥 ) ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 𝑔 ) = 𝑓 ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ∀ 𝑣 ∈ ( 𝑧 𝐻 𝑤 ) ( ( 𝑣 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑣 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ) ) ) )
11	10	ibi	⊢ ( 𝐶 ∈ Cat → ∀ 𝑥 ∈ 𝐵 ( ∃ 𝑔 ∈ ( 𝑥 𝐻 𝑥 ) ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 𝑔 ) = 𝑓 ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ∀ 𝑣 ∈ ( 𝑧 𝐻 𝑤 ) ( ( 𝑣 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑣 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ) ) )
12		simpl	⊢ ( ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ∀ 𝑣 ∈ ( 𝑧 𝐻 𝑤 ) ( ( 𝑣 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑣 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) )
13	12	2ralimi	⊢ ( ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ∀ 𝑣 ∈ ( 𝑧 𝐻 𝑤 ) ( ( 𝑣 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑣 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ) → ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) )
14	13	2ralimi	⊢ ( ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ∀ 𝑣 ∈ ( 𝑧 𝐻 𝑤 ) ( ( 𝑣 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑣 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ) → ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) )
15	14	adantl	⊢ ( ( ∃ 𝑔 ∈ ( 𝑥 𝐻 𝑥 ) ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 𝑔 ) = 𝑓 ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ∀ 𝑣 ∈ ( 𝑧 𝐻 𝑤 ) ( ( 𝑣 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑣 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ) ) → ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) )
16	15	ralimi	⊢ ( ∀ 𝑥 ∈ 𝐵 ( ∃ 𝑔 ∈ ( 𝑥 𝐻 𝑥 ) ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 𝑔 ) = 𝑓 ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ∀ 𝑣 ∈ ( 𝑧 𝐻 𝑤 ) ( ( 𝑣 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑣 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ) ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) )
17	4 11 16	3syl	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) )
18	6	adantr	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → 𝑌 ∈ 𝐵 )
19	7	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) → 𝑍 ∈ 𝐵 )
20	8	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
21		simpllr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) → 𝑥 = 𝑋 )
22		simplr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) → 𝑦 = 𝑌 )
23	21 22	oveq12d	⊢ ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) → ( 𝑥 𝐻 𝑦 ) = ( 𝑋 𝐻 𝑌 ) )
24	20 23	eleqtrrd	⊢ ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) → 𝐹 ∈ ( 𝑥 𝐻 𝑦 ) )
25	9	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) → 𝐺 ∈ ( 𝑌 𝐻 𝑍 ) )
26		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) → 𝑧 = 𝑍 )
27	22 26	oveq12d	⊢ ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) → ( 𝑦 𝐻 𝑧 ) = ( 𝑌 𝐻 𝑍 ) )
28	25 27	eleqtrrd	⊢ ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) → 𝐺 ∈ ( 𝑦 𝐻 𝑧 ) )
29	28	adantr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑓 = 𝐹 ) → 𝐺 ∈ ( 𝑦 𝐻 𝑧 ) )
30		simp-5r	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → 𝑥 = 𝑋 )
31		simp-4r	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → 𝑦 = 𝑌 )
32	30 31	opeq12d	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑋 , 𝑌 ⟩ )
33		simpllr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → 𝑧 = 𝑍 )
34	32 33	oveq12d	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) = ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) )
35		simpr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → 𝑔 = 𝐺 )
36		simplr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → 𝑓 = 𝐹 )
37	34 35 36	oveq123d	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) = ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) )
38	30 33	oveq12d	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( 𝑥 𝐻 𝑧 ) = ( 𝑋 𝐻 𝑍 ) )
39	37 38	eleq12d	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ↔ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ∈ ( 𝑋 𝐻 𝑍 ) ) )
40	29 39	rspcdv	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑓 = 𝐹 ) → ( ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ∈ ( 𝑋 𝐻 𝑍 ) ) )
41	24 40	rspcimdv	⊢ ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) → ( ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ∈ ( 𝑋 𝐻 𝑍 ) ) )
42	19 41	rspcimdv	⊢ ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) → ( ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ∈ ( 𝑋 𝐻 𝑍 ) ) )
43	18 42	rspcimdv	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ∈ ( 𝑋 𝐻 𝑍 ) ) )
44	5 43	rspcimdv	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ∈ ( 𝑋 𝐻 𝑍 ) ) )
45	17 44	mpd	⊢ ( 𝜑 → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ∈ ( 𝑋 𝐻 𝑍 ) )