Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Norm Megill
Construction of a vector space from a Hilbert lattice
ltrncvr
Next ⟩
ltrnval1
Metamath Proof Explorer
Ascii
Unicode
Theorem
ltrncvr
Description:
Covering property of a lattice translation.
(Contributed by
NM
, 20-May-2012)
Ref
Expression
Hypotheses
ltrncvr.b
⊢
B
=
Base
K
ltrncvr.c
⊢
C
=
⋖
K
ltrncvr.h
⊢
H
=
LHyp
⁡
K
ltrncvr.t
⊢
T
=
LTrn
⁡
K
⁡
W
Assertion
ltrncvr
⊢
K
∈
V
∧
W
∈
H
∧
F
∈
T
∧
X
∈
B
∧
Y
∈
B
→
X
C
Y
↔
F
⁡
X
C
F
⁡
Y
Proof
Step
Hyp
Ref
Expression
1
ltrncvr.b
⊢
B
=
Base
K
2
ltrncvr.c
⊢
C
=
⋖
K
3
ltrncvr.h
⊢
H
=
LHyp
⁡
K
4
ltrncvr.t
⊢
T
=
LTrn
⁡
K
⁡
W
5
simp1l
⊢
K
∈
V
∧
W
∈
H
∧
F
∈
T
∧
X
∈
B
∧
Y
∈
B
→
K
∈
V
6
eqid
⊢
LAut
⁡
K
=
LAut
⁡
K
7
3
6
4
ltrnlaut
⊢
K
∈
V
∧
W
∈
H
∧
F
∈
T
→
F
∈
LAut
⁡
K
8
7
3adant3
⊢
K
∈
V
∧
W
∈
H
∧
F
∈
T
∧
X
∈
B
∧
Y
∈
B
→
F
∈
LAut
⁡
K
9
simp3l
⊢
K
∈
V
∧
W
∈
H
∧
F
∈
T
∧
X
∈
B
∧
Y
∈
B
→
X
∈
B
10
simp3r
⊢
K
∈
V
∧
W
∈
H
∧
F
∈
T
∧
X
∈
B
∧
Y
∈
B
→
Y
∈
B
11
1
2
6
lautcvr
⊢
K
∈
V
∧
F
∈
LAut
⁡
K
∧
X
∈
B
∧
Y
∈
B
→
X
C
Y
↔
F
⁡
X
C
F
⁡
Y
12
5
8
9
10
11
syl13anc
⊢
K
∈
V
∧
W
∈
H
∧
F
∈
T
∧
X
∈
B
∧
Y
∈
B
→
X
C
Y
↔
F
⁡
X
C
F
⁡
Y