Definition df-tgrp 39614

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 39613	. 2 class TGrp
2		vk	. . 3 setvar 𝑘
3		cvv 3475	. . 3 class V
4		vw	. . . 4 setvar 𝑤
5	2	cv 1541	. . . . 5 class 𝑘
6		clh 38855	. . . . 5 class LHyp
7	5, 6	cfv 6544	. . . 4 class (LHyp‘𝑘)
8		cnx 17126	. . . . . . 7 class ndx
9		cbs 17144	. . . . . . 7 class Base
10	8, 9	cfv 6544	. . . . . 6 class (Base‘ndx)
11	4	cv 1541	. . . . . . 7 class 𝑤
12		cltrn 38972	. . . . . . . 8 class LTrn
13	5, 12	cfv 6544	. . . . . . 7 class (LTrn‘𝑘)
14	11, 13	cfv 6544	. . . . . 6 class ((LTrn‘𝑘)‘𝑤)
15	10, 14	cop 4635	. . . . 5 class ⟨(Base‘ndx), ((LTrn‘𝑘)‘𝑤)⟩
16		cplusg 17197	. . . . . . 7 class +g
17	8, 16	cfv 6544	. . . . . 6 class (+g‘ndx)
18		vf	. . . . . . 7 setvar 𝑓
19		vg	. . . . . . 7 setvar 𝑔
20	18	cv 1541	. . . . . . . 8 class 𝑓
21	19	cv 1541	. . . . . . . 8 class 𝑔
22	20, 21	ccom 5681	. . . . . . 7 class (𝑓 ∘ 𝑔)
23	18, 19, 14, 14, 22	cmpo 7411	. . . . . 6 class (𝑓 ∈ ((LTrn‘𝑘)‘𝑤), 𝑔 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑓 ∘ 𝑔))
24	17, 23	cop 4635	. . . . 5 class ⟨(+g‘ndx), (𝑓 ∈ ((LTrn‘𝑘)‘𝑤), 𝑔 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑓 ∘ 𝑔))⟩
25	15, 24	cpr 4631	. . . 4 class {⟨(Base‘ndx), ((LTrn‘𝑘)‘𝑤)⟩, ⟨(+g‘ndx), (𝑓 ∈ ((LTrn‘𝑘)‘𝑤), 𝑔 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑓 ∘ 𝑔))⟩}
26	4, 7, 25	cmpt 5232	. . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ {⟨(Base‘ndx), ((LTrn‘𝑘)‘𝑤)⟩, ⟨(+g‘ndx), (𝑓 ∈ ((LTrn‘𝑘)‘𝑤), 𝑔 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑓 ∘ 𝑔))⟩})
27	2, 3, 26	cmpt 5232	. 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {⟨(Base‘ndx), ((LTrn‘𝑘)‘𝑤)⟩, ⟨(+g‘ndx), (𝑓 ∈ ((LTrn‘𝑘)‘𝑤), 𝑔 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑓 ∘ 𝑔))⟩}))
28	1, 27	wceq 1542	1 wff TGrp = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {⟨(Base‘ndx), ((LTrn‘𝑘)‘𝑤)⟩, ⟨(+g‘ndx), (𝑓 ∈ ((LTrn‘𝑘)‘𝑤), 𝑔 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑓 ∘ 𝑔))⟩}))

This definition is referenced by:  tgrpfset  39615