Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Norm Megill
Construction of a vector space from a Hilbert lattice
4atexlemqtb
Next ⟩
4atexlempns
Metamath Proof Explorer
Ascii
Unicode
Theorem
4atexlemqtb
Description:
Lemma for
4atexlem7
.
(Contributed by
NM
, 24-Nov-2012)
Ref
Expression
Hypotheses
4thatlem.ph
⊢
φ
↔
K
∈
HL
∧
W
∈
H
∧
P
∈
A
∧
¬
P
≤
˙
W
∧
Q
∈
A
∧
¬
Q
≤
˙
W
∧
S
∈
A
∧
R
∈
A
∧
¬
R
≤
˙
W
∧
P
∨
˙
R
=
Q
∨
˙
R
∧
T
∈
A
∧
U
∨
˙
T
=
V
∨
˙
T
∧
P
≠
Q
∧
¬
S
≤
˙
P
∨
˙
Q
4thatlempqb.j
⊢
∨
˙
=
join
⁡
K
4thatlempqb.a
⊢
A
=
Atoms
⁡
K
Assertion
4atexlemqtb
⊢
φ
→
Q
∨
˙
T
∈
Base
K
Proof
Step
Hyp
Ref
Expression
1
4thatlem.ph
⊢
φ
↔
K
∈
HL
∧
W
∈
H
∧
P
∈
A
∧
¬
P
≤
˙
W
∧
Q
∈
A
∧
¬
Q
≤
˙
W
∧
S
∈
A
∧
R
∈
A
∧
¬
R
≤
˙
W
∧
P
∨
˙
R
=
Q
∨
˙
R
∧
T
∈
A
∧
U
∨
˙
T
=
V
∨
˙
T
∧
P
≠
Q
∧
¬
S
≤
˙
P
∨
˙
Q
2
4thatlempqb.j
⊢
∨
˙
=
join
⁡
K
3
4thatlempqb.a
⊢
A
=
Atoms
⁡
K
4
1
4atexlemk
⊢
φ
→
K
∈
HL
5
1
4atexlemq
⊢
φ
→
Q
∈
A
6
1
4atexlemt
⊢
φ
→
T
∈
A
7
eqid
⊢
Base
K
=
Base
K
8
7
2
3
hlatjcl
⊢
K
∈
HL
∧
Q
∈
A
∧
T
∈
A
→
Q
∨
˙
T
∈
Base
K
9
4
5
6
8
syl3anc
⊢
φ
→
Q
∨
˙
T
∈
Base
K