Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Norm Megill
Construction of a vector space from a Hilbert lattice
tgrpfset
Next ⟩
tgrpset
Metamath Proof Explorer
Ascii
Unicode
Theorem
tgrpfset
Description:
The translation group maps for a lattice
K
.
(Contributed by
NM
, 5-Jun-2013)
Ref
Expression
Hypothesis
tgrpset.h
⊢
H
=
LHyp
⁡
K
Assertion
tgrpfset
⊢
K
∈
V
→
TGrp
⁡
K
=
w
∈
H
⟼
Base
ndx
LTrn
⁡
K
⁡
w
+
ndx
f
∈
LTrn
⁡
K
⁡
w
,
g
∈
LTrn
⁡
K
⁡
w
⟼
f
∘
g
Proof
Step
Hyp
Ref
Expression
1
tgrpset.h
⊢
H
=
LHyp
⁡
K
2
elex
⊢
K
∈
V
→
K
∈
V
3
fveq2
⊢
k
=
K
→
LHyp
⁡
k
=
LHyp
⁡
K
4
3
1
eqtr4di
⊢
k
=
K
→
LHyp
⁡
k
=
H
5
fveq2
⊢
k
=
K
→
LTrn
⁡
k
=
LTrn
⁡
K
6
5
fveq1d
⊢
k
=
K
→
LTrn
⁡
k
⁡
w
=
LTrn
⁡
K
⁡
w
7
6
opeq2d
⊢
k
=
K
→
Base
ndx
LTrn
⁡
k
⁡
w
=
Base
ndx
LTrn
⁡
K
⁡
w
8
eqidd
⊢
k
=
K
→
f
∘
g
=
f
∘
g
9
6
6
8
mpoeq123dv
⊢
k
=
K
→
f
∈
LTrn
⁡
k
⁡
w
,
g
∈
LTrn
⁡
k
⁡
w
⟼
f
∘
g
=
f
∈
LTrn
⁡
K
⁡
w
,
g
∈
LTrn
⁡
K
⁡
w
⟼
f
∘
g
10
9
opeq2d
⊢
k
=
K
→
+
ndx
f
∈
LTrn
⁡
k
⁡
w
,
g
∈
LTrn
⁡
k
⁡
w
⟼
f
∘
g
=
+
ndx
f
∈
LTrn
⁡
K
⁡
w
,
g
∈
LTrn
⁡
K
⁡
w
⟼
f
∘
g
11
7
10
preq12d
⊢
k
=
K
→
Base
ndx
LTrn
⁡
k
⁡
w
+
ndx
f
∈
LTrn
⁡
k
⁡
w
,
g
∈
LTrn
⁡
k
⁡
w
⟼
f
∘
g
=
Base
ndx
LTrn
⁡
K
⁡
w
+
ndx
f
∈
LTrn
⁡
K
⁡
w
,
g
∈
LTrn
⁡
K
⁡
w
⟼
f
∘
g
12
4
11
mpteq12dv
⊢
k
=
K
→
w
∈
LHyp
⁡
k
⟼
Base
ndx
LTrn
⁡
k
⁡
w
+
ndx
f
∈
LTrn
⁡
k
⁡
w
,
g
∈
LTrn
⁡
k
⁡
w
⟼
f
∘
g
=
w
∈
H
⟼
Base
ndx
LTrn
⁡
K
⁡
w
+
ndx
f
∈
LTrn
⁡
K
⁡
w
,
g
∈
LTrn
⁡
K
⁡
w
⟼
f
∘
g
13
df-tgrp
⊢
TGrp
=
k
∈
V
⟼
w
∈
LHyp
⁡
k
⟼
Base
ndx
LTrn
⁡
k
⁡
w
+
ndx
f
∈
LTrn
⁡
k
⁡
w
,
g
∈
LTrn
⁡
k
⁡
w
⟼
f
∘
g
14
12
13
1
mptfvmpt
⊢
K
∈
V
→
TGrp
⁡
K
=
w
∈
H
⟼
Base
ndx
LTrn
⁡
K
⁡
w
+
ndx
f
∈
LTrn
⁡
K
⁡
w
,
g
∈
LTrn
⁡
K
⁡
w
⟼
f
∘
g
15
2
14
syl
⊢
K
∈
V
→
TGrp
⁡
K
=
w
∈
H
⟼
Base
ndx
LTrn
⁡
K
⁡
w
+
ndx
f
∈
LTrn
⁡
K
⁡
w
,
g
∈
LTrn
⁡
K
⁡
w
⟼
f
∘
g