This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = ( 𝑘 ∈ 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 ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( 𝑓 ∘ 𝑔 ) ) ⟩ } ) )