Definition df-tgrp 40745

Description: Define the class of all translation groups. 𝑘 is normally a member of HL. Each base set is the set of all lattice translations with respect to a hyperplane 𝑤, and the operation is function composition. Similar to definition of G in [Crawley] p. 116, third paragraph (which defines this for geomodular lattices). (Contributed by NM, 5-Jun-2013.)

Assertion

Ref	Expression
df-tgrp	⊢ TGrp = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {⟨(Base‘ndx), ((LTrn‘𝑘)‘𝑤)⟩, ⟨(+g‘ndx), (𝑓 ∈ ((LTrn‘𝑘)‘𝑤), 𝑔 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑓 ∘ 𝑔))⟩}))

Distinct variable group:   𝑤,𝑘,𝑓,𝑔

Detailed syntax breakdown of Definition df-tgrp

Step	Hyp	Ref	Expression
1		ctgrp 40744	. 2 class TGrp
2		vk	. . 3 setvar 𝑘
3		cvv 3480	. . 3 class V
4		vw	. . . 4 setvar 𝑤
5	2	cv 1539	. . . . 5 class 𝑘
6		clh 39986	. . . . 5 class LHyp
7	5, 6	cfv 6561	. . . 4 class (LHyp‘𝑘)
8		cnx 17230	. . . . . . 7 class ndx
9		cbs 17247	. . . . . . 7 class Base
10	8, 9	cfv 6561	. . . . . 6 class (Base‘ndx)
11	4	cv 1539	. . . . . . 7 class 𝑤
12		cltrn 40103	. . . . . . . 8 class LTrn
13	5, 12	cfv 6561	. . . . . . 7 class (LTrn‘𝑘)
14	11, 13	cfv 6561	. . . . . 6 class ((LTrn‘𝑘)‘𝑤)
15	10, 14	cop 4632	. . . . 5 class ⟨(Base‘ndx), ((LTrn‘𝑘)‘𝑤)⟩
16		cplusg 17297	. . . . . . 7 class +g
17	8, 16	cfv 6561	. . . . . 6 class (+g‘ndx)
18		vf	. . . . . . 7 setvar 𝑓
19		vg	. . . . . . 7 setvar 𝑔
20	18	cv 1539	. . . . . . . 8 class 𝑓
21	19	cv 1539	. . . . . . . 8 class 𝑔
22	20, 21	ccom 5689	. . . . . . 7 class (𝑓 ∘ 𝑔)
23	18, 19, 14, 14, 22	cmpo 7433	. . . . . 6 class (𝑓 ∈ ((LTrn‘𝑘)‘𝑤), 𝑔 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑓 ∘ 𝑔))
24	17, 23	cop 4632	. . . . 5 class ⟨(+g‘ndx), (𝑓 ∈ ((LTrn‘𝑘)‘𝑤), 𝑔 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑓 ∘ 𝑔))⟩
25	15, 24	cpr 4628	. . . 4 class {⟨(Base‘ndx), ((LTrn‘𝑘)‘𝑤)⟩, ⟨(+g‘ndx), (𝑓 ∈ ((LTrn‘𝑘)‘𝑤), 𝑔 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑓 ∘ 𝑔))⟩}
26	4, 7, 25	cmpt 5225	. . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ {⟨(Base‘ndx), ((LTrn‘𝑘)‘𝑤)⟩, ⟨(+g‘ndx), (𝑓 ∈ ((LTrn‘𝑘)‘𝑤), 𝑔 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑓 ∘ 𝑔))⟩})
27	2, 3, 26	cmpt 5225	. 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {⟨(Base‘ndx), ((LTrn‘𝑘)‘𝑤)⟩, ⟨(+g‘ndx), (𝑓 ∈ ((LTrn‘𝑘)‘𝑤), 𝑔 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑓 ∘ 𝑔))⟩}))
28	1, 27	wceq 1540	1 wff TGrp = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {⟨(Base‘ndx), ((LTrn‘𝑘)‘𝑤)⟩, ⟨(+g‘ndx), (𝑓 ∈ ((LTrn‘𝑘)‘𝑤), 𝑔 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑓 ∘ 𝑔))⟩}))

This definition is referenced by:  tgrpfset  40746