Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Norm Megill
Construction of a vector space from a Hilbert lattice
4atexlemp
Next ⟩
4atexlemq
Metamath Proof Explorer
Ascii
Unicode
Theorem
4atexlemp
Description:
Lemma for
4atexlem7
.
(Contributed by
NM
, 23-Nov-2012)
Ref
Expression
Hypothesis
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
Assertion
4atexlemp
⊢
φ
→
P
∈
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
1
4atexlempw
⊢
φ
→
P
∈
A
∧
¬
P
≤
˙
W
3
2
simpld
⊢
φ
→
P
∈
A