Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Norm Megill
Construction of a vector space from a Hilbert lattice
ltrnval1
Next ⟩
ltrnid
Metamath Proof Explorer
Ascii
Unicode
Theorem
ltrnval1
Description:
Value of a lattice translation under its co-atom.
(Contributed by
NM
, 20-May-2012)
Ref
Expression
Hypotheses
ltrnval1.b
⊢
B
=
Base
K
ltrnval1.l
⊢
≤
˙
=
≤
K
ltrnval1.h
⊢
H
=
LHyp
⁡
K
ltrnval1.t
⊢
T
=
LTrn
⁡
K
⁡
W
Assertion
ltrnval1
⊢
K
∈
V
∧
W
∈
H
∧
F
∈
T
∧
X
∈
B
∧
X
≤
˙
W
→
F
⁡
X
=
X
Proof
Step
Hyp
Ref
Expression
1
ltrnval1.b
⊢
B
=
Base
K
2
ltrnval1.l
⊢
≤
˙
=
≤
K
3
ltrnval1.h
⊢
H
=
LHyp
⁡
K
4
ltrnval1.t
⊢
T
=
LTrn
⁡
K
⁡
W
5
eqid
⊢
LDil
⁡
K
⁡
W
=
LDil
⁡
K
⁡
W
6
3
5
4
ltrnldil
⊢
K
∈
V
∧
W
∈
H
∧
F
∈
T
→
F
∈
LDil
⁡
K
⁡
W
7
6
3adant3
⊢
K
∈
V
∧
W
∈
H
∧
F
∈
T
∧
X
∈
B
∧
X
≤
˙
W
→
F
∈
LDil
⁡
K
⁡
W
8
1
2
3
5
ldilval
⊢
K
∈
V
∧
W
∈
H
∧
F
∈
LDil
⁡
K
⁡
W
∧
X
∈
B
∧
X
≤
˙
W
→
F
⁡
X
=
X
9
7
8
syld3an2
⊢
K
∈
V
∧
W
∈
H
∧
F
∈
T
∧
X
∈
B
∧
X
≤
˙
W
→
F
⁡
X
=
X