Definition df-ghm

Description: A homomorphism of groups is a map between two structures which preserves the group operation. Requiring both sides to be groups simplifies most theorems at the cost of complicating the theorem which pushes forward a group structure. (Contributed by Stefan O'Rear, 31-Dec-2014)

	Ref	Expression
Assertion	df-ghm	⊢ GrpHom = ( 𝑠 ∈ Grp , 𝑡 ∈ Grp ↦ { 𝑔 ∣ [ ( Base ‘ 𝑠 ) / 𝑤 ] ( 𝑔 : 𝑤 ⟶ ( Base ‘ 𝑡 ) ∧ ∀ 𝑥 ∈ 𝑤 ∀ 𝑦 ∈ 𝑤 ( 𝑔 ‘ ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 ) ) = ( ( 𝑔 ‘ 𝑥 ) ( +g ‘ 𝑡 ) ( 𝑔 ‘ 𝑦 ) ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cghm	⊢ GrpHom
1		vs	⊢ 𝑠
2		cgrp	⊢ Grp
3		vt	⊢ 𝑡
4		vg	⊢ 𝑔
5		cbs	⊢ Base
6	1	cv	⊢ 𝑠
7	6 5	cfv	⊢ ( Base ‘ 𝑠 )
8		vw	⊢ 𝑤
9	4	cv	⊢ 𝑔
10	8	cv	⊢ 𝑤
11	3	cv	⊢ 𝑡
12	11 5	cfv	⊢ ( Base ‘ 𝑡 )
13	10 12 9	wf	⊢ 𝑔 : 𝑤 ⟶ ( Base ‘ 𝑡 )
14		vx	⊢ 𝑥
15		vy	⊢ 𝑦
16	14	cv	⊢ 𝑥
17		cplusg	⊢ +g
18	6 17	cfv	⊢ ( +g ‘ 𝑠 )
19	15	cv	⊢ 𝑦
20	16 19 18	co	⊢ ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 )
21	20 9	cfv	⊢ ( 𝑔 ‘ ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 ) )
22	16 9	cfv	⊢ ( 𝑔 ‘ 𝑥 )
23	11 17	cfv	⊢ ( +g ‘ 𝑡 )
24	19 9	cfv	⊢ ( 𝑔 ‘ 𝑦 )
25	22 24 23	co	⊢ ( ( 𝑔 ‘ 𝑥 ) ( +g ‘ 𝑡 ) ( 𝑔 ‘ 𝑦 ) )
26	21 25	wceq	⊢ ( 𝑔 ‘ ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 ) ) = ( ( 𝑔 ‘ 𝑥 ) ( +g ‘ 𝑡 ) ( 𝑔 ‘ 𝑦 ) )
27	26 15 10	wral	⊢ ∀ 𝑦 ∈ 𝑤 ( 𝑔 ‘ ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 ) ) = ( ( 𝑔 ‘ 𝑥 ) ( +g ‘ 𝑡 ) ( 𝑔 ‘ 𝑦 ) )
28	27 14 10	wral	⊢ ∀ 𝑥 ∈ 𝑤 ∀ 𝑦 ∈ 𝑤 ( 𝑔 ‘ ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 ) ) = ( ( 𝑔 ‘ 𝑥 ) ( +g ‘ 𝑡 ) ( 𝑔 ‘ 𝑦 ) )
29	13 28	wa	⊢ ( 𝑔 : 𝑤 ⟶ ( Base ‘ 𝑡 ) ∧ ∀ 𝑥 ∈ 𝑤 ∀ 𝑦 ∈ 𝑤 ( 𝑔 ‘ ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 ) ) = ( ( 𝑔 ‘ 𝑥 ) ( +g ‘ 𝑡 ) ( 𝑔 ‘ 𝑦 ) ) )
30	29 8 7	wsbc	⊢ [ ( Base ‘ 𝑠 ) / 𝑤 ] ( 𝑔 : 𝑤 ⟶ ( Base ‘ 𝑡 ) ∧ ∀ 𝑥 ∈ 𝑤 ∀ 𝑦 ∈ 𝑤 ( 𝑔 ‘ ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 ) ) = ( ( 𝑔 ‘ 𝑥 ) ( +g ‘ 𝑡 ) ( 𝑔 ‘ 𝑦 ) ) )
31	30 4	cab	⊢ { 𝑔 ∣ [ ( Base ‘ 𝑠 ) / 𝑤 ] ( 𝑔 : 𝑤 ⟶ ( Base ‘ 𝑡 ) ∧ ∀ 𝑥 ∈ 𝑤 ∀ 𝑦 ∈ 𝑤 ( 𝑔 ‘ ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 ) ) = ( ( 𝑔 ‘ 𝑥 ) ( +g ‘ 𝑡 ) ( 𝑔 ‘ 𝑦 ) ) ) }
32	1 3 2 2 31	cmpo	⊢ ( 𝑠 ∈ Grp , 𝑡 ∈ Grp ↦ { 𝑔 ∣ [ ( Base ‘ 𝑠 ) / 𝑤 ] ( 𝑔 : 𝑤 ⟶ ( Base ‘ 𝑡 ) ∧ ∀ 𝑥 ∈ 𝑤 ∀ 𝑦 ∈ 𝑤 ( 𝑔 ‘ ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 ) ) = ( ( 𝑔 ‘ 𝑥 ) ( +g ‘ 𝑡 ) ( 𝑔 ‘ 𝑦 ) ) ) } )
33	0 32	wceq	⊢ GrpHom = ( 𝑠 ∈ Grp , 𝑡 ∈ Grp ↦ { 𝑔 ∣ [ ( Base ‘ 𝑠 ) / 𝑤 ] ( 𝑔 : 𝑤 ⟶ ( Base ‘ 𝑡 ) ∧ ∀ 𝑥 ∈ 𝑤 ∀ 𝑦 ∈ 𝑤 ( 𝑔 ‘ ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 ) ) = ( ( 𝑔 ‘ 𝑥 ) ( +g ‘ 𝑡 ) ( 𝑔 ‘ 𝑦 ) ) ) } )