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

Metamath Proof Explorer

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 ‘ 𝑡 ) ( 𝑔 ‘ 𝑦 ) ) ) } )