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