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 \in V ⟼ (w \in LHyp (k) ⟼ \{⟨{Base}_{ndx}, LTrn (k) (w)⟩, ⟨+_{ndx}, (f \in LTrn (k) (w), g \in LTrn (k) (w) ⟼ f \circ 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 \circ g)$
22	17 18 13 13 21	cmpo	$class (f \in LTrn (k) (w), g \in LTrn (k) (w) ⟼ f \circ g)$
23	16 22	cop	$class ⟨+_{ndx}, (f \in LTrn (k) (w), g \in LTrn (k) (w) ⟼ f \circ g)⟩$
24	14 23	cpr	$class \{⟨{Base}_{ndx}, LTrn (k) (w)⟩, ⟨+_{ndx}, (f \in LTrn (k) (w), g \in LTrn (k) (w) ⟼ f \circ g)⟩\}$
25	3 6 24	cmpt	$class (w \in LHyp (k) ⟼ \{⟨{Base}_{ndx}, LTrn (k) (w)⟩, ⟨+_{ndx}, (f \in LTrn (k) (w), g \in LTrn (k) (w) ⟼ f \circ g)⟩\})$
26	1 2 25	cmpt	$class (k \in V ⟼ (w \in LHyp (k) ⟼ \{⟨{Base}_{ndx}, LTrn (k) (w)⟩, ⟨+_{ndx}, (f \in LTrn (k) (w), g \in LTrn (k) (w) ⟼ f \circ g)⟩\}))$
27	0 26	wceq	$wff TGrp = (k \in V ⟼ (w \in LHyp (k) ⟼ \{⟨{Base}_{ndx}, LTrn (k) (w)⟩, ⟨+_{ndx}, (f \in LTrn (k) (w), g \in LTrn (k) (w) ⟼ f \circ g)⟩\}))$

Metamath Proof Explorer

Definition df-tgrp

Detailed syntax breakdown