Detailed syntax breakdown of Definition df-tgrp
Step | Hyp | Ref
| Expression |
1 | | ctgrp 38519 |
. 2
class
TGrp |
2 | | vk |
. . 3
setvar 𝑘 |
3 | | cvv 3420 |
. . 3
class
V |
4 | | vw |
. . . 4
setvar 𝑤 |
5 | 2 | cv 1542 |
. . . . 5
class 𝑘 |
6 | | clh 37761 |
. . . . 5
class
LHyp |
7 | 5, 6 | cfv 6397 |
. . . 4
class
(LHyp‘𝑘) |
8 | | cnx 16768 |
. . . . . . 7
class
ndx |
9 | | cbs 16784 |
. . . . . . 7
class
Base |
10 | 8, 9 | cfv 6397 |
. . . . . 6
class
(Base‘ndx) |
11 | 4 | cv 1542 |
. . . . . . 7
class 𝑤 |
12 | | cltrn 37878 |
. . . . . . . 8
class
LTrn |
13 | 5, 12 | cfv 6397 |
. . . . . . 7
class
(LTrn‘𝑘) |
14 | 11, 13 | cfv 6397 |
. . . . . 6
class
((LTrn‘𝑘)‘𝑤) |
15 | 10, 14 | cop 4561 |
. . . . 5
class
〈(Base‘ndx), ((LTrn‘𝑘)‘𝑤)〉 |
16 | | cplusg 16826 |
. . . . . . 7
class
+g |
17 | 8, 16 | cfv 6397 |
. . . . . 6
class
(+g‘ndx) |
18 | | vf |
. . . . . . 7
setvar 𝑓 |
19 | | vg |
. . . . . . 7
setvar 𝑔 |
20 | 18 | cv 1542 |
. . . . . . . 8
class 𝑓 |
21 | 19 | cv 1542 |
. . . . . . . 8
class 𝑔 |
22 | 20, 21 | ccom 5569 |
. . . . . . 7
class (𝑓 ∘ 𝑔) |
23 | 18, 19, 14, 14, 22 | cmpo 7233 |
. . . . . 6
class (𝑓 ∈ ((LTrn‘𝑘)‘𝑤), 𝑔 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑓 ∘ 𝑔)) |
24 | 17, 23 | cop 4561 |
. . . . 5
class
〈(+g‘ndx), (𝑓 ∈ ((LTrn‘𝑘)‘𝑤), 𝑔 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑓 ∘ 𝑔))〉 |
25 | 15, 24 | cpr 4557 |
. . . 4
class
{〈(Base‘ndx), ((LTrn‘𝑘)‘𝑤)〉, 〈(+g‘ndx),
(𝑓 ∈
((LTrn‘𝑘)‘𝑤), 𝑔 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑓 ∘ 𝑔))〉} |
26 | 4, 7, 25 | cmpt 5149 |
. . 3
class (𝑤 ∈ (LHyp‘𝑘) ↦
{〈(Base‘ndx), ((LTrn‘𝑘)‘𝑤)〉, 〈(+g‘ndx),
(𝑓 ∈
((LTrn‘𝑘)‘𝑤), 𝑔 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑓 ∘ 𝑔))〉}) |
27 | 2, 3, 26 | cmpt 5149 |
. 2
class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦
{〈(Base‘ndx), ((LTrn‘𝑘)‘𝑤)〉, 〈(+g‘ndx),
(𝑓 ∈
((LTrn‘𝑘)‘𝑤), 𝑔 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑓 ∘ 𝑔))〉})) |
28 | 1, 27 | wceq 1543 |
1
wff TGrp =
(𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦
{〈(Base‘ndx), ((LTrn‘𝑘)‘𝑤)〉, 〈(+g‘ndx),
(𝑓 ∈
((LTrn‘𝑘)‘𝑤), 𝑔 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑓 ∘ 𝑔))〉})) |