Metamath Proof Explorer

Theorem funcco

Description: A functor maps composition in the source category to composition in the target. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses funcco.b ⊢ 𝐵 = ( Base ‘ 𝐷 )
funcco.h ⊢ 𝐻 = ( Hom ‘ 𝐷 )
funcco.o ⊢ · = ( comp ‘ 𝐷 )
funcco.O ⊢ 𝑂 = ( comp ‘ 𝐸 )
funcco.f ⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
funcco.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
funcco.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
funcco.z ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
funcco.m ⊢ ( 𝜑 → 𝑀 ∈ ( 𝑋 𝐻 𝑌 ) )
funcco.n ⊢ ( 𝜑 → 𝑁 ∈ ( 𝑌 𝐻 𝑍 ) )
Assertion funcco ( 𝜑 → ( ( 𝑋 𝐺 𝑍 ) ‘ ( 𝑁 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝑀 ) ) = ( ( ( 𝑌 𝐺 𝑍 ) ‘ 𝑁 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑍 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑀 ) ) )

Proof

Step Hyp Ref Expression
1 funcco.b ⊢ 𝐵 = ( Base ‘ 𝐷 )
2 funcco.h ⊢ 𝐻 = ( Hom ‘ 𝐷 )
3 funcco.o ⊢ · = ( comp ‘ 𝐷 )
4 funcco.O ⊢ 𝑂 = ( comp ‘ 𝐸 )
5 funcco.f ⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
6 funcco.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
7 funcco.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
8 funcco.z ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
9 funcco.m ⊢ ( 𝜑 → 𝑀 ∈ ( 𝑋 𝐻 𝑌 ) )
10 funcco.n ⊢ ( 𝜑 → 𝑁 ∈ ( 𝑌 𝐻 𝑍 ) )
11 eqid ⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
12 eqid ⊢ ( Hom ‘ 𝐸 ) = ( Hom ‘ 𝐸 )
13 eqid ⊢ ( Id ‘ 𝐷 ) = ( Id ‘ 𝐷 )
14 eqid ⊢ ( Id ‘ 𝐸 ) = ( Id ‘ 𝐸 )
15 df-br ⊢ ( 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐷 Func 𝐸 ) )
16 5 15 sylib ⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐷 Func 𝐸 ) )
17 funcrcl ⊢ ( ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐷 Func 𝐸 ) → ( 𝐷 ∈ Cat ∧ 𝐸 ∈ Cat ) )
18 16 17 syl ⊢ ( 𝜑 → ( 𝐷 ∈ Cat ∧ 𝐸 ∈ Cat ) )
19 18 simpld ⊢ ( 𝜑 → 𝐷 ∈ Cat )
20 18 simprd ⊢ ( 𝜑 → 𝐸 ∈ Cat )
21 1 11 2 12 13 14 3 4 19 20 isfunc ⊢ ( 𝜑 → ( 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 ↔ ( 𝐹 : 𝐵 ⟶ ( Base ‘ 𝐸 ) ∧ 𝐺 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝐹 ‘ ( 1st ‘ 𝑧 ) ) ( Hom ‘ 𝐸 ) ( 𝐹 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑥 𝐺 𝑥 ) ‘ ( ( Id ‘ 𝐷 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐸 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝐺 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑧 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑚 ) ) ) ) ) )
22 5 21 mpbid ⊢ ( 𝜑 → ( 𝐹 : 𝐵 ⟶ ( Base ‘ 𝐸 ) ∧ 𝐺 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝐹 ‘ ( 1st ‘ 𝑧 ) ) ( Hom ‘ 𝐸 ) ( 𝐹 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑥 𝐺 𝑥 ) ‘ ( ( Id ‘ 𝐷 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐸 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝐺 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑧 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑚 ) ) ) ) )
23 22 simp3d ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑥 𝐺 𝑥 ) ‘ ( ( Id ‘ 𝐷 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐸 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝐺 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑧 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑚 ) ) ) )
24 7 adantr ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → 𝑌 ∈ 𝐵 )
25 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) → 𝑍 ∈ 𝐵 )
26 9 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) → 𝑀 ∈ ( 𝑋 𝐻 𝑌 ) )
27 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) → 𝑥 = 𝑋 )
28 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) → 𝑦 = 𝑌 )
29 27 28 oveq12d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) → ( 𝑥 𝐻 𝑦 ) = ( 𝑋 𝐻 𝑌 ) )
30 26 29 eleqtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) → 𝑀 ∈ ( 𝑥 𝐻 𝑦 ) )
31 10 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑚 = 𝑀 ) → 𝑁 ∈ ( 𝑌 𝐻 𝑍 ) )
32 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑚 = 𝑀 ) → 𝑦 = 𝑌 )
33 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑚 = 𝑀 ) → 𝑧 = 𝑍 )
34 32 33 oveq12d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑚 = 𝑀 ) → ( 𝑦 𝐻 𝑧 ) = ( 𝑌 𝐻 𝑍 ) )
35 31 34 eleqtrrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑚 = 𝑀 ) → 𝑁 ∈ ( 𝑦 𝐻 𝑧 ) )
36 simp-5r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑚 = 𝑀 ) ∧ 𝑛 = 𝑁 ) → 𝑥 = 𝑋 )
37 simpllr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑚 = 𝑀 ) ∧ 𝑛 = 𝑁 ) → 𝑧 = 𝑍 )
38 36 37 oveq12d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑚 = 𝑀 ) ∧ 𝑛 = 𝑁 ) → ( 𝑥 𝐺 𝑧 ) = ( 𝑋 𝐺 𝑍 ) )
39 simp-4r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑚 = 𝑀 ) ∧ 𝑛 = 𝑁 ) → 𝑦 = 𝑌 )
40 36 39 opeq12d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑚 = 𝑀 ) ∧ 𝑛 = 𝑁 ) → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑋 , 𝑌 ⟩ )
41 40 37 oveq12d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑚 = 𝑀 ) ∧ 𝑛 = 𝑁 ) → ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) = ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) )
42 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑚 = 𝑀 ) ∧ 𝑛 = 𝑁 ) → 𝑛 = 𝑁 )
43 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑚 = 𝑀 ) ∧ 𝑛 = 𝑁 ) → 𝑚 = 𝑀 )
44 41 42 43 oveq123d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑚 = 𝑀 ) ∧ 𝑛 = 𝑁 ) → ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) = ( 𝑁 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝑀 ) )
45 38 44 fveq12d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑚 = 𝑀 ) ∧ 𝑛 = 𝑁 ) → ( ( 𝑥 𝐺 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( 𝑋 𝐺 𝑍 ) ‘ ( 𝑁 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝑀 ) ) )
46 36 fveq2d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑚 = 𝑀 ) ∧ 𝑛 = 𝑁 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) )
47 39 fveq2d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑚 = 𝑀 ) ∧ 𝑛 = 𝑁 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑌 ) )
48 46 47 opeq12d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑚 = 𝑀 ) ∧ 𝑛 = 𝑁 ) → ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ = ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ )
49 37 fveq2d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑚 = 𝑀 ) ∧ 𝑛 = 𝑁 ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑍 ) )
50 48 49 oveq12d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑚 = 𝑀 ) ∧ 𝑛 = 𝑁 ) → ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑧 ) ) = ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑍 ) ) )
51 39 37 oveq12d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑚 = 𝑀 ) ∧ 𝑛 = 𝑁 ) → ( 𝑦 𝐺 𝑧 ) = ( 𝑌 𝐺 𝑍 ) )
52 51 42 fveq12d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑚 = 𝑀 ) ∧ 𝑛 = 𝑁 ) → ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑛 ) = ( ( 𝑌 𝐺 𝑍 ) ‘ 𝑁 ) )
53 36 39 oveq12d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑚 = 𝑀 ) ∧ 𝑛 = 𝑁 ) → ( 𝑥 𝐺 𝑦 ) = ( 𝑋 𝐺 𝑌 ) )
54 53 43 fveq12d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑚 = 𝑀 ) ∧ 𝑛 = 𝑁 ) → ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑚 ) = ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑀 ) )
55 50 52 54 oveq123d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑚 = 𝑀 ) ∧ 𝑛 = 𝑁 ) → ( ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑧 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑚 ) ) = ( ( ( 𝑌 𝐺 𝑍 ) ‘ 𝑁 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑍 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑀 ) ) )
56 45 55 eqeq12d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑚 = 𝑀 ) ∧ 𝑛 = 𝑁 ) → ( ( ( 𝑥 𝐺 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑧 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑚 ) ) ↔ ( ( 𝑋 𝐺 𝑍 ) ‘ ( 𝑁 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝑀 ) ) = ( ( ( 𝑌 𝐺 𝑍 ) ‘ 𝑁 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑍 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑀 ) ) ) )
57 35 56 rspcdv ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑚 = 𝑀 ) → ( ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝐺 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑧 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑚 ) ) → ( ( 𝑋 𝐺 𝑍 ) ‘ ( 𝑁 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝑀 ) ) = ( ( ( 𝑌 𝐺 𝑍 ) ‘ 𝑁 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑍 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑀 ) ) ) )
58 30 57 rspcimdv ⊢ ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) → ( ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝐺 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑧 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑚 ) ) → ( ( 𝑋 𝐺 𝑍 ) ‘ ( 𝑁 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝑀 ) ) = ( ( ( 𝑌 𝐺 𝑍 ) ‘ 𝑁 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑍 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑀 ) ) ) )
59 25 58 rspcimdv ⊢ ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) → ( ∀ 𝑧 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝐺 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑧 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑚 ) ) → ( ( 𝑋 𝐺 𝑍 ) ‘ ( 𝑁 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝑀 ) ) = ( ( ( 𝑌 𝐺 𝑍 ) ‘ 𝑁 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑍 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑀 ) ) ) )
60 24 59 rspcimdv ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝐺 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑧 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑚 ) ) → ( ( 𝑋 𝐺 𝑍 ) ‘ ( 𝑁 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝑀 ) ) = ( ( ( 𝑌 𝐺 𝑍 ) ‘ 𝑁 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑍 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑀 ) ) ) )
61 60 adantld ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( ( ( ( 𝑥 𝐺 𝑥 ) ‘ ( ( Id ‘ 𝐷 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐸 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝐺 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑧 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑚 ) ) ) → ( ( 𝑋 𝐺 𝑍 ) ‘ ( 𝑁 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝑀 ) ) = ( ( ( 𝑌 𝐺 𝑍 ) ‘ 𝑁 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑍 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑀 ) ) ) )
62 6 61 rspcimdv ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑥 𝐺 𝑥 ) ‘ ( ( Id ‘ 𝐷 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐸 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝐺 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑧 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑚 ) ) ) → ( ( 𝑋 𝐺 𝑍 ) ‘ ( 𝑁 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝑀 ) ) = ( ( ( 𝑌 𝐺 𝑍 ) ‘ 𝑁 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑍 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑀 ) ) ) )
63 23 62 mpd ⊢ ( 𝜑 → ( ( 𝑋 𝐺 𝑍 ) ‘ ( 𝑁 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝑀 ) ) = ( ( ( 𝑌 𝐺 𝑍 ) ‘ 𝑁 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑍 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑀 ) ) )