Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-tgrp Structured version   Visualization version   GIF version

Definition df-tgrp 36348
 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
StepHypRef Expression
1 ctgrp 36347 . 2 class TGrp
2 vk . . 3 setvar 𝑘
3 cvv 3231 . . 3 class V
4 vw . . . 4 setvar 𝑤
52cv 1522 . . . . 5 class 𝑘
6 clh 35588 . . . . 5 class LHyp
75, 6cfv 5926 . . . 4 class (LHyp‘𝑘)
8 cnx 15901 . . . . . . 7 class ndx
9 cbs 15904 . . . . . . 7 class Base
108, 9cfv 5926 . . . . . 6 class (Base‘ndx)
114cv 1522 . . . . . . 7 class 𝑤
12 cltrn 35705 . . . . . . . 8 class LTrn
135, 12cfv 5926 . . . . . . 7 class (LTrn‘𝑘)
1411, 13cfv 5926 . . . . . 6 class ((LTrn‘𝑘)‘𝑤)
1510, 14cop 4216 . . . . 5 class ⟨(Base‘ndx), ((LTrn‘𝑘)‘𝑤)⟩
16 cplusg 15988 . . . . . . 7 class +g
178, 16cfv 5926 . . . . . 6 class (+g‘ndx)
18 vf . . . . . . 7 setvar 𝑓
19 vg . . . . . . 7 setvar 𝑔
2018cv 1522 . . . . . . . 8 class 𝑓
2119cv 1522 . . . . . . . 8 class 𝑔
2220, 21ccom 5147 . . . . . . 7 class (𝑓𝑔)
2318, 19, 14, 14, 22cmpt2 6692 . . . . . 6 class (𝑓 ∈ ((LTrn‘𝑘)‘𝑤), 𝑔 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑓𝑔))
2417, 23cop 4216 . . . . 5 class ⟨(+g‘ndx), (𝑓 ∈ ((LTrn‘𝑘)‘𝑤), 𝑔 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑓𝑔))⟩
2515, 24cpr 4212 . . . 4 class {⟨(Base‘ndx), ((LTrn‘𝑘)‘𝑤)⟩, ⟨(+g‘ndx), (𝑓 ∈ ((LTrn‘𝑘)‘𝑤), 𝑔 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑓𝑔))⟩}
264, 7, 25cmpt 4762 . . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ {⟨(Base‘ndx), ((LTrn‘𝑘)‘𝑤)⟩, ⟨(+g‘ndx), (𝑓 ∈ ((LTrn‘𝑘)‘𝑤), 𝑔 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑓𝑔))⟩})
272, 3, 26cmpt 4762 . 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {⟨(Base‘ndx), ((LTrn‘𝑘)‘𝑤)⟩, ⟨(+g‘ndx), (𝑓 ∈ ((LTrn‘𝑘)‘𝑤), 𝑔 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑓𝑔))⟩}))
281, 27wceq 1523 1 wff TGrp = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {⟨(Base‘ndx), ((LTrn‘𝑘)‘𝑤)⟩, ⟨(+g‘ndx), (𝑓 ∈ ((LTrn‘𝑘)‘𝑤), 𝑔 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑓𝑔))⟩}))
 Colors of variables: wff setvar class This definition is referenced by:  tgrpfset  36349
 Copyright terms: Public domain W3C validator