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 𝐻 ) )