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 = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ { ⟨ ( Base ‘ ndx ) , ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) , 𝑔 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( 𝑓 ∘ 𝑔 ) ) ⟩ } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctgrp	⊢ TGrp
1		vk	⊢ 𝑘
2		cvv	⊢ V
3		vw	⊢ 𝑤
4		clh	⊢ LHyp
5	1	cv	⊢ 𝑘
6	5 4	cfv	⊢ ( LHyp ‘ 𝑘 )
7		cbs	⊢ Base
8		cnx	⊢ ndx
9	8 7	cfv	⊢ ( Base ‘ ndx )
10		cltrn	⊢ LTrn
11	5 10	cfv	⊢ ( LTrn ‘ 𝑘 )
12	3	cv	⊢ 𝑤
13	12 11	cfv	⊢ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 )
14	9 13	cop	⊢ ⟨ ( Base ‘ ndx ) , ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ⟩
15		cplusg	⊢ +g
16	8 15	cfv	⊢ ( +g ‘ ndx )
17		vf	⊢ 𝑓
18		vg	⊢ 𝑔
19	17	cv	⊢ 𝑓
20	18	cv	⊢ 𝑔
21	19 20	ccom	⊢ ( 𝑓 ∘ 𝑔 )
22	17 18 13 13 21	cmpo	⊢ ( 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) , 𝑔 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( 𝑓 ∘ 𝑔 ) )
23	16 22	cop	⊢ ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) , 𝑔 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( 𝑓 ∘ 𝑔 ) ) ⟩
24	14 23	cpr	⊢ { ⟨ ( Base ‘ ndx ) , ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) , 𝑔 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( 𝑓 ∘ 𝑔 ) ) ⟩ }
25	3 6 24	cmpt	⊢ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ { ⟨ ( Base ‘ ndx ) , ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) , 𝑔 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( 𝑓 ∘ 𝑔 ) ) ⟩ } )
26	1 2 25	cmpt	⊢ ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ { ⟨ ( Base ‘ ndx ) , ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) , 𝑔 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( 𝑓 ∘ 𝑔 ) ) ⟩ } ) )
27	0 26	wceq	⊢ TGrp = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ { ⟨ ( Base ‘ ndx ) , ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) , 𝑔 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( 𝑓 ∘ 𝑔 ) ) ⟩ } ) )