Detailed syntax breakdown of Definition df-ghm
Step | Hyp | Ref
| Expression |
1 | | cghm 18619 |
. 2
class
GrpHom |
2 | | vs |
. . 3
setvar 𝑠 |
3 | | vt |
. . 3
setvar 𝑡 |
4 | | cgrp 18365 |
. . 3
class
Grp |
5 | | vw |
. . . . . . . 8
setvar 𝑤 |
6 | 5 | cv 1542 |
. . . . . . 7
class 𝑤 |
7 | 3 | cv 1542 |
. . . . . . . 8
class 𝑡 |
8 | | cbs 16760 |
. . . . . . . 8
class
Base |
9 | 7, 8 | cfv 6380 |
. . . . . . 7
class
(Base‘𝑡) |
10 | | vg |
. . . . . . . 8
setvar 𝑔 |
11 | 10 | cv 1542 |
. . . . . . 7
class 𝑔 |
12 | 6, 9, 11 | wf 6376 |
. . . . . 6
wff 𝑔:𝑤⟶(Base‘𝑡) |
13 | | vx |
. . . . . . . . . . . 12
setvar 𝑥 |
14 | 13 | cv 1542 |
. . . . . . . . . . 11
class 𝑥 |
15 | | vy |
. . . . . . . . . . . 12
setvar 𝑦 |
16 | 15 | cv 1542 |
. . . . . . . . . . 11
class 𝑦 |
17 | 2 | cv 1542 |
. . . . . . . . . . . 12
class 𝑠 |
18 | | cplusg 16802 |
. . . . . . . . . . . 12
class
+g |
19 | 17, 18 | cfv 6380 |
. . . . . . . . . . 11
class
(+g‘𝑠) |
20 | 14, 16, 19 | co 7213 |
. . . . . . . . . 10
class (𝑥(+g‘𝑠)𝑦) |
21 | 20, 11 | cfv 6380 |
. . . . . . . . 9
class (𝑔‘(𝑥(+g‘𝑠)𝑦)) |
22 | 14, 11 | cfv 6380 |
. . . . . . . . . 10
class (𝑔‘𝑥) |
23 | 16, 11 | cfv 6380 |
. . . . . . . . . 10
class (𝑔‘𝑦) |
24 | 7, 18 | cfv 6380 |
. . . . . . . . . 10
class
(+g‘𝑡) |
25 | 22, 23, 24 | co 7213 |
. . . . . . . . 9
class ((𝑔‘𝑥)(+g‘𝑡)(𝑔‘𝑦)) |
26 | 21, 25 | wceq 1543 |
. . . . . . . 8
wff (𝑔‘(𝑥(+g‘𝑠)𝑦)) = ((𝑔‘𝑥)(+g‘𝑡)(𝑔‘𝑦)) |
27 | 26, 15, 6 | wral 3061 |
. . . . . . 7
wff
∀𝑦 ∈
𝑤 (𝑔‘(𝑥(+g‘𝑠)𝑦)) = ((𝑔‘𝑥)(+g‘𝑡)(𝑔‘𝑦)) |
28 | 27, 13, 6 | wral 3061 |
. . . . . 6
wff
∀𝑥 ∈
𝑤 ∀𝑦 ∈ 𝑤 (𝑔‘(𝑥(+g‘𝑠)𝑦)) = ((𝑔‘𝑥)(+g‘𝑡)(𝑔‘𝑦)) |
29 | 12, 28 | wa 399 |
. . . . 5
wff (𝑔:𝑤⟶(Base‘𝑡) ∧ ∀𝑥 ∈ 𝑤 ∀𝑦 ∈ 𝑤 (𝑔‘(𝑥(+g‘𝑠)𝑦)) = ((𝑔‘𝑥)(+g‘𝑡)(𝑔‘𝑦))) |
30 | 17, 8 | cfv 6380 |
. . . . 5
class
(Base‘𝑠) |
31 | 29, 5, 30 | wsbc 3694 |
. . . 4
wff
[(Base‘𝑠) / 𝑤](𝑔:𝑤⟶(Base‘𝑡) ∧ ∀𝑥 ∈ 𝑤 ∀𝑦 ∈ 𝑤 (𝑔‘(𝑥(+g‘𝑠)𝑦)) = ((𝑔‘𝑥)(+g‘𝑡)(𝑔‘𝑦))) |
32 | 31, 10 | cab 2714 |
. . 3
class {𝑔 ∣
[(Base‘𝑠) /
𝑤](𝑔:𝑤⟶(Base‘𝑡) ∧ ∀𝑥 ∈ 𝑤 ∀𝑦 ∈ 𝑤 (𝑔‘(𝑥(+g‘𝑠)𝑦)) = ((𝑔‘𝑥)(+g‘𝑡)(𝑔‘𝑦)))} |
33 | 2, 3, 4, 4, 32 | cmpo 7215 |
. 2
class (𝑠 ∈ Grp, 𝑡 ∈ Grp ↦ {𝑔 ∣ [(Base‘𝑠) / 𝑤](𝑔:𝑤⟶(Base‘𝑡) ∧ ∀𝑥 ∈ 𝑤 ∀𝑦 ∈ 𝑤 (𝑔‘(𝑥(+g‘𝑠)𝑦)) = ((𝑔‘𝑥)(+g‘𝑡)(𝑔‘𝑦)))}) |
34 | 1, 33 | wceq 1543 |
1
wff GrpHom =
(𝑠 ∈ Grp, 𝑡 ∈ Grp ↦ {𝑔 ∣
[(Base‘𝑠) /
𝑤](𝑔:𝑤⟶(Base‘𝑡) ∧ ∀𝑥 ∈ 𝑤 ∀𝑦 ∈ 𝑤 (𝑔‘(𝑥(+g‘𝑠)𝑦)) = ((𝑔‘𝑥)(+g‘𝑡)(𝑔‘𝑦)))}) |