Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Norm Megill
Construction of a vector space from a Hilbert lattice
4atexlemnslpq
Next ⟩
4atexlemkl
Metamath Proof Explorer
Ascii
Unicode
Theorem
4atexlemnslpq
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
4atexlemnslpq
⊢
φ
→
¬
S
≤
˙
P
∨
˙
Q
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
simp3r
⊢
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
→
¬
S
≤
˙
P
∨
˙
Q
3
1
2
sylbi
⊢
φ
→
¬
S
≤
˙
P
∨
˙
Q