This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem frgpup1

Description: Any assignment of the generators to target elements can be extended (uniquely) to a homomorphism from a free monoid to an arbitrary other monoid. (Contributed by Mario Carneiro, 2-Oct-2015) (Revised by Mario Carneiro, 28-Feb-2016)

Ref Expression
Hypotheses frgpup.b ⊢ 𝐵 = ( Base ‘ 𝐻 )
frgpup.n ⊢ 𝑁 = ( invg ‘ 𝐻 )
frgpup.t ⊢ 𝑇 = ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ if ( 𝑧 = ∅ , ( 𝐹 ‘ 𝑦 ) , ( 𝑁 ‘ ( 𝐹 ‘ 𝑦 ) ) ) )
frgpup.h ⊢ ( 𝜑 → 𝐻 ∈ Grp )
frgpup.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
frgpup.a ⊢ ( 𝜑 → 𝐹 : 𝐼 ⟶ 𝐵 )
frgpup.w ⊢ 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) )
frgpup.r ⊢ ∼ = ( ~FG ‘ 𝐼 )
frgpup.g ⊢ 𝐺 = ( freeGrp ‘ 𝐼 )
frgpup.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
frgpup.e ⊢ 𝐸 = ran ( 𝑔 ∈ 𝑊 ↦ ⟨ [ 𝑔 ] ∼ , ( 𝐻 Σg ( 𝑇 ∘ 𝑔 ) ) ⟩ )
Assertion frgpup1 ( 𝜑 → 𝐸 ∈ ( 𝐺 GrpHom 𝐻 ) )

Proof

Step Hyp Ref Expression
1 frgpup.b ⊢ 𝐵 = ( Base ‘ 𝐻 )
2 frgpup.n ⊢ 𝑁 = ( invg ‘ 𝐻 )
3 frgpup.t ⊢ 𝑇 = ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ if ( 𝑧 = ∅ , ( 𝐹 ‘ 𝑦 ) , ( 𝑁 ‘ ( 𝐹 ‘ 𝑦 ) ) ) )
4 frgpup.h ⊢ ( 𝜑 → 𝐻 ∈ Grp )
5 frgpup.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
6 frgpup.a ⊢ ( 𝜑 → 𝐹 : 𝐼 ⟶ 𝐵 )
7 frgpup.w ⊢ 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) )
8 frgpup.r ⊢ ∼ = ( ~FG ‘ 𝐼 )
9 frgpup.g ⊢ 𝐺 = ( freeGrp ‘ 𝐼 )
10 frgpup.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
11 frgpup.e ⊢ 𝐸 = ran ( 𝑔 ∈ 𝑊 ↦ ⟨ [ 𝑔 ] ∼ , ( 𝐻 Σg ( 𝑇 ∘ 𝑔 ) ) ⟩ )
12 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
13 eqid ⊢ ( +g ‘ 𝐻 ) = ( +g ‘ 𝐻 )
14 9 frgpgrp ⊢ ( 𝐼 ∈ 𝑉 → 𝐺 ∈ Grp )
15 5 14 syl ⊢ ( 𝜑 → 𝐺 ∈ Grp )
16 1 2 3 4 5 6 7 8 9 10 11 frgpupf ⊢ ( 𝜑 → 𝐸 : 𝑋 ⟶ 𝐵 )
17 eqid ⊢ ( freeMnd ‘ ( 𝐼 × 2o ) ) = ( freeMnd ‘ ( 𝐼 × 2o ) )
18 9 17 8 frgpval ⊢ ( 𝐼 ∈ 𝑉 → 𝐺 = ( ( freeMnd ‘ ( 𝐼 × 2o ) ) /s ∼ ) )
19 5 18 syl ⊢ ( 𝜑 → 𝐺 = ( ( freeMnd ‘ ( 𝐼 × 2o ) ) /s ∼ ) )
20 2on ⊢ 2o ∈ On
21 xpexg ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 2o ∈ On ) → ( 𝐼 × 2o ) ∈ V )
22 5 20 21 sylancl ⊢ ( 𝜑 → ( 𝐼 × 2o ) ∈ V )
23 wrdexg ⊢ ( ( 𝐼 × 2o ) ∈ V → Word ( 𝐼 × 2o ) ∈ V )
24 fvi ⊢ ( Word ( 𝐼 × 2o ) ∈ V → ( I ‘ Word ( 𝐼 × 2o ) ) = Word ( 𝐼 × 2o ) )
25 22 23 24 3syl ⊢ ( 𝜑 → ( I ‘ Word ( 𝐼 × 2o ) ) = Word ( 𝐼 × 2o ) )
26 7 25 eqtrid ⊢ ( 𝜑 → 𝑊 = Word ( 𝐼 × 2o ) )
27 eqid ⊢ ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) = ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) )
28 17 27 frmdbas ⊢ ( ( 𝐼 × 2o ) ∈ V → ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) = Word ( 𝐼 × 2o ) )
29 22 28 syl ⊢ ( 𝜑 → ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) = Word ( 𝐼 × 2o ) )
30 26 29 eqtr4d ⊢ ( 𝜑 → 𝑊 = ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) )
31 8 fvexi ⊢ ∼ ∈ V
32 31 a1i ⊢ ( 𝜑 → ∼ ∈ V )
33 fvexd ⊢ ( 𝜑 → ( freeMnd ‘ ( 𝐼 × 2o ) ) ∈ V )
34 19 30 32 33 qusbas ⊢ ( 𝜑 → ( 𝑊 / ∼ ) = ( Base ‘ 𝐺 ) )
35 10 34 eqtr4id ⊢ ( 𝜑 → 𝑋 = ( 𝑊 / ∼ ) )
36 eqimss ⊢ ( 𝑋 = ( 𝑊 / ∼ ) → 𝑋 ⊆ ( 𝑊 / ∼ ) )
37 35 36 syl ⊢ ( 𝜑 → 𝑋 ⊆ ( 𝑊 / ∼ ) )
38 37 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑋 ) → 𝑋 ⊆ ( 𝑊 / ∼ ) )
39 38 sselda ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝑋 ) → 𝑐 ∈ ( 𝑊 / ∼ ) )
40 eqid ⊢ ( 𝑊 / ∼ ) = ( 𝑊 / ∼ )
41 oveq2 ⊢ ( [ 𝑢 ] ∼ = 𝑐 → ( 𝑎 ( +g ‘ 𝐺 ) [ 𝑢 ] ∼ ) = ( 𝑎 ( +g ‘ 𝐺 ) 𝑐 ) )
42 41 fveq2d ⊢ ( [ 𝑢 ] ∼ = 𝑐 → ( 𝐸 ‘ ( 𝑎 ( +g ‘ 𝐺 ) [ 𝑢 ] ∼ ) ) = ( 𝐸 ‘ ( 𝑎 ( +g ‘ 𝐺 ) 𝑐 ) ) )
43 fveq2 ⊢ ( [ 𝑢 ] ∼ = 𝑐 → ( 𝐸 ‘ [ 𝑢 ] ∼ ) = ( 𝐸 ‘ 𝑐 ) )
44 43 oveq2d ⊢ ( [ 𝑢 ] ∼ = 𝑐 → ( ( 𝐸 ‘ 𝑎 ) ( +g ‘ 𝐻 ) ( 𝐸 ‘ [ 𝑢 ] ∼ ) ) = ( ( 𝐸 ‘ 𝑎 ) ( +g ‘ 𝐻 ) ( 𝐸 ‘ 𝑐 ) ) )
45 42 44 eqeq12d ⊢ ( [ 𝑢 ] ∼ = 𝑐 → ( ( 𝐸 ‘ ( 𝑎 ( +g ‘ 𝐺 ) [ 𝑢 ] ∼ ) ) = ( ( 𝐸 ‘ 𝑎 ) ( +g ‘ 𝐻 ) ( 𝐸 ‘ [ 𝑢 ] ∼ ) ) ↔ ( 𝐸 ‘ ( 𝑎 ( +g ‘ 𝐺 ) 𝑐 ) ) = ( ( 𝐸 ‘ 𝑎 ) ( +g ‘ 𝐻 ) ( 𝐸 ‘ 𝑐 ) ) ) )
46 37 sselda ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑋 ) → 𝑎 ∈ ( 𝑊 / ∼ ) )
47 46 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑊 ) ∧ 𝑎 ∈ 𝑋 ) → 𝑎 ∈ ( 𝑊 / ∼ ) )
48 fvoveq1 ⊢ ( [ 𝑡 ] ∼ = 𝑎 → ( 𝐸 ‘ ( [ 𝑡 ] ∼ ( +g ‘ 𝐺 ) [ 𝑢 ] ∼ ) ) = ( 𝐸 ‘ ( 𝑎 ( +g ‘ 𝐺 ) [ 𝑢 ] ∼ ) ) )
49 fveq2 ⊢ ( [ 𝑡 ] ∼ = 𝑎 → ( 𝐸 ‘ [ 𝑡 ] ∼ ) = ( 𝐸 ‘ 𝑎 ) )
50 49 oveq1d ⊢ ( [ 𝑡 ] ∼ = 𝑎 → ( ( 𝐸 ‘ [ 𝑡 ] ∼ ) ( +g ‘ 𝐻 ) ( 𝐸 ‘ [ 𝑢 ] ∼ ) ) = ( ( 𝐸 ‘ 𝑎 ) ( +g ‘ 𝐻 ) ( 𝐸 ‘ [ 𝑢 ] ∼ ) ) )
51 48 50 eqeq12d ⊢ ( [ 𝑡 ] ∼ = 𝑎 → ( ( 𝐸 ‘ ( [ 𝑡 ] ∼ ( +g ‘ 𝐺 ) [ 𝑢 ] ∼ ) ) = ( ( 𝐸 ‘ [ 𝑡 ] ∼ ) ( +g ‘ 𝐻 ) ( 𝐸 ‘ [ 𝑢 ] ∼ ) ) ↔ ( 𝐸 ‘ ( 𝑎 ( +g ‘ 𝐺 ) [ 𝑢 ] ∼ ) ) = ( ( 𝐸 ‘ 𝑎 ) ( +g ‘ 𝐻 ) ( 𝐸 ‘ [ 𝑢 ] ∼ ) ) ) )
52 fviss ⊢ ( I ‘ Word ( 𝐼 × 2o ) ) ⊆ Word ( 𝐼 × 2o )
53 7 52 eqsstri ⊢ 𝑊 ⊆ Word ( 𝐼 × 2o )
54 53 sseli ⊢ ( 𝑡 ∈ 𝑊 → 𝑡 ∈ Word ( 𝐼 × 2o ) )
55 53 sseli ⊢ ( 𝑢 ∈ 𝑊 → 𝑢 ∈ Word ( 𝐼 × 2o ) )
56 ccatcl ⊢ ( ( 𝑡 ∈ Word ( 𝐼 × 2o ) ∧ 𝑢 ∈ Word ( 𝐼 × 2o ) ) → ( 𝑡 ++ 𝑢 ) ∈ Word ( 𝐼 × 2o ) )
57 54 55 56 syl2an ⊢ ( ( 𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ) → ( 𝑡 ++ 𝑢 ) ∈ Word ( 𝐼 × 2o ) )
58 7 efgrcl ⊢ ( 𝑡 ∈ 𝑊 → ( 𝐼 ∈ V ∧ 𝑊 = Word ( 𝐼 × 2o ) ) )
59 58 adantr ⊢ ( ( 𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ) → ( 𝐼 ∈ V ∧ 𝑊 = Word ( 𝐼 × 2o ) ) )
60 59 simprd ⊢ ( ( 𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ) → 𝑊 = Word ( 𝐼 × 2o ) )
61 57 60 eleqtrrd ⊢ ( ( 𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ) → ( 𝑡 ++ 𝑢 ) ∈ 𝑊 )
62 1 2 3 4 5 6 7 8 9 10 11 frgpupval ⊢ ( ( 𝜑 ∧ ( 𝑡 ++ 𝑢 ) ∈ 𝑊 ) → ( 𝐸 ‘ [ ( 𝑡 ++ 𝑢 ) ] ∼ ) = ( 𝐻 Σg ( 𝑇 ∘ ( 𝑡 ++ 𝑢 ) ) ) )
63 61 62 sylan2 ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ) ) → ( 𝐸 ‘ [ ( 𝑡 ++ 𝑢 ) ] ∼ ) = ( 𝐻 Σg ( 𝑇 ∘ ( 𝑡 ++ 𝑢 ) ) ) )
64 54 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ) ) → 𝑡 ∈ Word ( 𝐼 × 2o ) )
65 55 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ) ) → 𝑢 ∈ Word ( 𝐼 × 2o ) )
66 1 2 3 4 5 6 frgpuptf ⊢ ( 𝜑 → 𝑇 : ( 𝐼 × 2o ) ⟶ 𝐵 )
67 66 adantr ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ) ) → 𝑇 : ( 𝐼 × 2o ) ⟶ 𝐵 )
68 ccatco ⊢ ( ( 𝑡 ∈ Word ( 𝐼 × 2o ) ∧ 𝑢 ∈ Word ( 𝐼 × 2o ) ∧ 𝑇 : ( 𝐼 × 2o ) ⟶ 𝐵 ) → ( 𝑇 ∘ ( 𝑡 ++ 𝑢 ) ) = ( ( 𝑇 ∘ 𝑡 ) ++ ( 𝑇 ∘ 𝑢 ) ) )
69 64 65 67 68 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ) ) → ( 𝑇 ∘ ( 𝑡 ++ 𝑢 ) ) = ( ( 𝑇 ∘ 𝑡 ) ++ ( 𝑇 ∘ 𝑢 ) ) )
70 69 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ) ) → ( 𝐻 Σg ( 𝑇 ∘ ( 𝑡 ++ 𝑢 ) ) ) = ( 𝐻 Σg ( ( 𝑇 ∘ 𝑡 ) ++ ( 𝑇 ∘ 𝑢 ) ) ) )
71 4 grpmndd ⊢ ( 𝜑 → 𝐻 ∈ Mnd )
72 71 adantr ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ) ) → 𝐻 ∈ Mnd )
73 wrdco ⊢ ( ( 𝑡 ∈ Word ( 𝐼 × 2o ) ∧ 𝑇 : ( 𝐼 × 2o ) ⟶ 𝐵 ) → ( 𝑇 ∘ 𝑡 ) ∈ Word 𝐵 )
74 54 66 73 syl2anr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑊 ) → ( 𝑇 ∘ 𝑡 ) ∈ Word 𝐵 )
75 74 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ) ) → ( 𝑇 ∘ 𝑡 ) ∈ Word 𝐵 )
76 wrdco ⊢ ( ( 𝑢 ∈ Word ( 𝐼 × 2o ) ∧ 𝑇 : ( 𝐼 × 2o ) ⟶ 𝐵 ) → ( 𝑇 ∘ 𝑢 ) ∈ Word 𝐵 )
77 65 67 76 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ) ) → ( 𝑇 ∘ 𝑢 ) ∈ Word 𝐵 )
78 1 13 gsumccat ⊢ ( ( 𝐻 ∈ Mnd ∧ ( 𝑇 ∘ 𝑡 ) ∈ Word 𝐵 ∧ ( 𝑇 ∘ 𝑢 ) ∈ Word 𝐵 ) → ( 𝐻 Σg ( ( 𝑇 ∘ 𝑡 ) ++ ( 𝑇 ∘ 𝑢 ) ) ) = ( ( 𝐻 Σg ( 𝑇 ∘ 𝑡 ) ) ( +g ‘ 𝐻 ) ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) ) )
79 72 75 77 78 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ) ) → ( 𝐻 Σg ( ( 𝑇 ∘ 𝑡 ) ++ ( 𝑇 ∘ 𝑢 ) ) ) = ( ( 𝐻 Σg ( 𝑇 ∘ 𝑡 ) ) ( +g ‘ 𝐻 ) ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) ) )
80 63 70 79 3eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ) ) → ( 𝐸 ‘ [ ( 𝑡 ++ 𝑢 ) ] ∼ ) = ( ( 𝐻 Σg ( 𝑇 ∘ 𝑡 ) ) ( +g ‘ 𝐻 ) ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) ) )
81 7 9 8 12 frgpadd ⊢ ( ( 𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ) → ( [ 𝑡 ] ∼ ( +g ‘ 𝐺 ) [ 𝑢 ] ∼ ) = [ ( 𝑡 ++ 𝑢 ) ] ∼ )
82 81 adantl ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ) ) → ( [ 𝑡 ] ∼ ( +g ‘ 𝐺 ) [ 𝑢 ] ∼ ) = [ ( 𝑡 ++ 𝑢 ) ] ∼ )
83 82 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ) ) → ( 𝐸 ‘ ( [ 𝑡 ] ∼ ( +g ‘ 𝐺 ) [ 𝑢 ] ∼ ) ) = ( 𝐸 ‘ [ ( 𝑡 ++ 𝑢 ) ] ∼ ) )
84 1 2 3 4 5 6 7 8 9 10 11 frgpupval ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑊 ) → ( 𝐸 ‘ [ 𝑡 ] ∼ ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑡 ) ) )
85 84 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ) ) → ( 𝐸 ‘ [ 𝑡 ] ∼ ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑡 ) ) )
86 1 2 3 4 5 6 7 8 9 10 11 frgpupval ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑊 ) → ( 𝐸 ‘ [ 𝑢 ] ∼ ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) )
87 86 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ) ) → ( 𝐸 ‘ [ 𝑢 ] ∼ ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) )
88 85 87 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ) ) → ( ( 𝐸 ‘ [ 𝑡 ] ∼ ) ( +g ‘ 𝐻 ) ( 𝐸 ‘ [ 𝑢 ] ∼ ) ) = ( ( 𝐻 Σg ( 𝑇 ∘ 𝑡 ) ) ( +g ‘ 𝐻 ) ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) ) )
89 80 83 88 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ) ) → ( 𝐸 ‘ ( [ 𝑡 ] ∼ ( +g ‘ 𝐺 ) [ 𝑢 ] ∼ ) ) = ( ( 𝐸 ‘ [ 𝑡 ] ∼ ) ( +g ‘ 𝐻 ) ( 𝐸 ‘ [ 𝑢 ] ∼ ) ) )
90 89 anass1rs ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑊 ) ∧ 𝑡 ∈ 𝑊 ) → ( 𝐸 ‘ ( [ 𝑡 ] ∼ ( +g ‘ 𝐺 ) [ 𝑢 ] ∼ ) ) = ( ( 𝐸 ‘ [ 𝑡 ] ∼ ) ( +g ‘ 𝐻 ) ( 𝐸 ‘ [ 𝑢 ] ∼ ) ) )
91 40 51 90 ectocld ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑊 ) ∧ 𝑎 ∈ ( 𝑊 / ∼ ) ) → ( 𝐸 ‘ ( 𝑎 ( +g ‘ 𝐺 ) [ 𝑢 ] ∼ ) ) = ( ( 𝐸 ‘ 𝑎 ) ( +g ‘ 𝐻 ) ( 𝐸 ‘ [ 𝑢 ] ∼ ) ) )
92 47 91 syldan ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑊 ) ∧ 𝑎 ∈ 𝑋 ) → ( 𝐸 ‘ ( 𝑎 ( +g ‘ 𝐺 ) [ 𝑢 ] ∼ ) ) = ( ( 𝐸 ‘ 𝑎 ) ( +g ‘ 𝐻 ) ( 𝐸 ‘ [ 𝑢 ] ∼ ) ) )
93 92 an32s ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑢 ∈ 𝑊 ) → ( 𝐸 ‘ ( 𝑎 ( +g ‘ 𝐺 ) [ 𝑢 ] ∼ ) ) = ( ( 𝐸 ‘ 𝑎 ) ( +g ‘ 𝐻 ) ( 𝐸 ‘ [ 𝑢 ] ∼ ) ) )
94 40 45 93 ectocld ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑐 ∈ ( 𝑊 / ∼ ) ) → ( 𝐸 ‘ ( 𝑎 ( +g ‘ 𝐺 ) 𝑐 ) ) = ( ( 𝐸 ‘ 𝑎 ) ( +g ‘ 𝐻 ) ( 𝐸 ‘ 𝑐 ) ) )
95 39 94 syldan ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝑋 ) → ( 𝐸 ‘ ( 𝑎 ( +g ‘ 𝐺 ) 𝑐 ) ) = ( ( 𝐸 ‘ 𝑎 ) ( +g ‘ 𝐻 ) ( 𝐸 ‘ 𝑐 ) ) )
96 95 anasss ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ) ) → ( 𝐸 ‘ ( 𝑎 ( +g ‘ 𝐺 ) 𝑐 ) ) = ( ( 𝐸 ‘ 𝑎 ) ( +g ‘ 𝐻 ) ( 𝐸 ‘ 𝑐 ) ) )
97 10 1 12 13 15 4 16 96 isghmd ⊢ ( 𝜑 → 𝐸 ∈ ( 𝐺 GrpHom 𝐻 ) )