Metamath Proof Explorer


Definition df-tgrp

Description: Define the class of all translation groups. k is normally a member of HL . Each base set is the set of all lattice translations with respect to a hyperplane w , 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)

Ref Expression
Assertion df-tgrp TGrp = k V w LHyp k Base ndx LTrn k w + ndx f LTrn k w , g LTrn k w f g

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctgrp class TGrp
1 vk setvar k
2 cvv class V
3 vw setvar w
4 clh class LHyp
5 1 cv setvar k
6 5 4 cfv class LHyp k
7 cbs class Base
8 cnx class ndx
9 8 7 cfv class Base ndx
10 cltrn class LTrn
11 5 10 cfv class LTrn k
12 3 cv setvar w
13 12 11 cfv class LTrn k w
14 9 13 cop class Base ndx LTrn k w
15 cplusg class + 𝑔
16 8 15 cfv class + ndx
17 vf setvar f
18 vg setvar g
19 17 cv setvar f
20 18 cv setvar g
21 19 20 ccom class f g
22 17 18 13 13 21 cmpo class f LTrn k w , g LTrn k w f g
23 16 22 cop class + ndx f LTrn k w , g LTrn k w f g
24 14 23 cpr class Base ndx LTrn k w + ndx f LTrn k w , g LTrn k w f g
25 3 6 24 cmpt class w LHyp k Base ndx LTrn k w + ndx f LTrn k w , g LTrn k w f g
26 1 2 25 cmpt class k V w LHyp k Base ndx LTrn k w + ndx f LTrn k w , g LTrn k w f g
27 0 26 wceq wff TGrp = k V w LHyp k Base ndx LTrn k w + ndx f LTrn k w , g LTrn k w f g