MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ghm Structured version   Visualization version   GIF version

Definition df-ghm 17481
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.)
Assertion
Ref Expression
df-ghm GrpHom = (𝑠 ∈ Grp, 𝑡 ∈ Grp ↦ {𝑔[(Base‘𝑠) / 𝑤](𝑔:𝑤⟶(Base‘𝑡) ∧ ∀𝑥𝑤𝑦𝑤 (𝑔‘(𝑥(+g𝑠)𝑦)) = ((𝑔𝑥)(+g𝑡)(𝑔𝑦)))})
Distinct variable group:   𝑔,𝑠,𝑡,𝑤,𝑥,𝑦

Detailed syntax breakdown of Definition df-ghm
StepHypRef Expression
1 cghm 17480 . 2 class GrpHom
2 vs . . 3 setvar 𝑠
3 vt . . 3 setvar 𝑡
4 cgrp 17245 . . 3 class Grp
5 vw . . . . . . . 8 setvar 𝑤
65cv 1474 . . . . . . 7 class 𝑤
73cv 1474 . . . . . . . 8 class 𝑡
8 cbs 15695 . . . . . . . 8 class Base
97, 8cfv 5804 . . . . . . 7 class (Base‘𝑡)
10 vg . . . . . . . 8 setvar 𝑔
1110cv 1474 . . . . . . 7 class 𝑔
126, 9, 11wf 5800 . . . . . 6 wff 𝑔:𝑤⟶(Base‘𝑡)
13 vx . . . . . . . . . . . 12 setvar 𝑥
1413cv 1474 . . . . . . . . . . 11 class 𝑥
15 vy . . . . . . . . . . . 12 setvar 𝑦
1615cv 1474 . . . . . . . . . . 11 class 𝑦
172cv 1474 . . . . . . . . . . . 12 class 𝑠
18 cplusg 15768 . . . . . . . . . . . 12 class +g
1917, 18cfv 5804 . . . . . . . . . . 11 class (+g𝑠)
2014, 16, 19co 6549 . . . . . . . . . 10 class (𝑥(+g𝑠)𝑦)
2120, 11cfv 5804 . . . . . . . . 9 class (𝑔‘(𝑥(+g𝑠)𝑦))
2214, 11cfv 5804 . . . . . . . . . 10 class (𝑔𝑥)
2316, 11cfv 5804 . . . . . . . . . 10 class (𝑔𝑦)
247, 18cfv 5804 . . . . . . . . . 10 class (+g𝑡)
2522, 23, 24co 6549 . . . . . . . . 9 class ((𝑔𝑥)(+g𝑡)(𝑔𝑦))
2621, 25wceq 1475 . . . . . . . 8 wff (𝑔‘(𝑥(+g𝑠)𝑦)) = ((𝑔𝑥)(+g𝑡)(𝑔𝑦))
2726, 15, 6wral 2896 . . . . . . 7 wff 𝑦𝑤 (𝑔‘(𝑥(+g𝑠)𝑦)) = ((𝑔𝑥)(+g𝑡)(𝑔𝑦))
2827, 13, 6wral 2896 . . . . . 6 wff 𝑥𝑤𝑦𝑤 (𝑔‘(𝑥(+g𝑠)𝑦)) = ((𝑔𝑥)(+g𝑡)(𝑔𝑦))
2912, 28wa 383 . . . . 5 wff (𝑔:𝑤⟶(Base‘𝑡) ∧ ∀𝑥𝑤𝑦𝑤 (𝑔‘(𝑥(+g𝑠)𝑦)) = ((𝑔𝑥)(+g𝑡)(𝑔𝑦)))
3017, 8cfv 5804 . . . . 5 class (Base‘𝑠)
3129, 5, 30wsbc 3402 . . . 4 wff [(Base‘𝑠) / 𝑤](𝑔:𝑤⟶(Base‘𝑡) ∧ ∀𝑥𝑤𝑦𝑤 (𝑔‘(𝑥(+g𝑠)𝑦)) = ((𝑔𝑥)(+g𝑡)(𝑔𝑦)))
3231, 10cab 2596 . . 3 class {𝑔[(Base‘𝑠) / 𝑤](𝑔:𝑤⟶(Base‘𝑡) ∧ ∀𝑥𝑤𝑦𝑤 (𝑔‘(𝑥(+g𝑠)𝑦)) = ((𝑔𝑥)(+g𝑡)(𝑔𝑦)))}
332, 3, 4, 4, 32cmpt2 6551 . 2 class (𝑠 ∈ Grp, 𝑡 ∈ Grp ↦ {𝑔[(Base‘𝑠) / 𝑤](𝑔:𝑤⟶(Base‘𝑡) ∧ ∀𝑥𝑤𝑦𝑤 (𝑔‘(𝑥(+g𝑠)𝑦)) = ((𝑔𝑥)(+g𝑡)(𝑔𝑦)))})
341, 33wceq 1475 1 wff GrpHom = (𝑠 ∈ Grp, 𝑡 ∈ Grp ↦ {𝑔[(Base‘𝑠) / 𝑤](𝑔:𝑤⟶(Base‘𝑡) ∧ ∀𝑥𝑤𝑦𝑤 (𝑔‘(𝑥(+g𝑠)𝑦)) = ((𝑔𝑥)(+g𝑡)(𝑔𝑦)))})
Colors of variables: wff setvar class
This definition is referenced by:  reldmghm  17482  isghm  17483
  Copyright terms: Public domain W3C validator