Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Norm Megill
Construction of a vector space from a Hilbert lattice
4atexlemu
Next ⟩
4atexlemv
Metamath Proof Explorer
Ascii
Unicode
Theorem
4atexlemu
Description:
Lemma for
4atexlem7
.
(Contributed by
NM
, 23-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
4thatlem0.l
⊢
≤
˙
=
≤
K
4thatlem0.j
⊢
∨
˙
=
join
⁡
K
4thatlem0.m
⊢
∧
˙
=
meet
⁡
K
4thatlem0.a
⊢
A
=
Atoms
⁡
K
4thatlem0.h
⊢
H
=
LHyp
⁡
K
4thatlem0.u
⊢
U
=
P
∨
˙
Q
∧
˙
W
Assertion
4atexlemu
⊢
φ
→
U
∈
A
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
4thatlem0.l
⊢
≤
˙
=
≤
K
3
4thatlem0.j
⊢
∨
˙
=
join
⁡
K
4
4thatlem0.m
⊢
∧
˙
=
meet
⁡
K
5
4thatlem0.a
⊢
A
=
Atoms
⁡
K
6
4thatlem0.h
⊢
H
=
LHyp
⁡
K
7
4thatlem0.u
⊢
U
=
P
∨
˙
Q
∧
˙
W
8
1
4atexlemk
⊢
φ
→
K
∈
HL
9
1
4atexlemw
⊢
φ
→
W
∈
H
10
1
4atexlempw
⊢
φ
→
P
∈
A
∧
¬
P
≤
˙
W
11
1
4atexlemq
⊢
φ
→
Q
∈
A
12
1
4atexlempnq
⊢
φ
→
P
≠
Q
13
2
3
4
5
6
7
lhpat2
⊢
K
∈
HL
∧
W
∈
H
∧
P
∈
A
∧
¬
P
≤
˙
W
∧
Q
∈
A
∧
P
≠
Q
→
U
∈
A
14
8
9
10
11
12
13
syl212anc
⊢
φ
→
U
∈
A