Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Norm Megill
Construction of a vector space from a Hilbert lattice
4atexlempns
Next ⟩
4atexlemswapqr
Metamath Proof Explorer
Ascii
Unicode
Theorem
4atexlempns
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
4thatlemslps.l
⊢
≤
˙
=
≤
K
4thatlemslps.j
⊢
∨
˙
=
join
⁡
K
4thatlemslps.a
⊢
A
=
Atoms
⁡
K
Assertion
4atexlempns
⊢
φ
→
P
≠
S
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
4thatlemslps.l
⊢
≤
˙
=
≤
K
3
4thatlemslps.j
⊢
∨
˙
=
join
⁡
K
4
4thatlemslps.a
⊢
A
=
Atoms
⁡
K
5
1
4atexlemk
⊢
φ
→
K
∈
HL
6
1
4atexlemp
⊢
φ
→
P
∈
A
7
1
4atexlemq
⊢
φ
→
Q
∈
A
8
1
4atexlems
⊢
φ
→
S
∈
A
9
1
4atexlemnslpq
⊢
φ
→
¬
S
≤
˙
P
∨
˙
Q
10
2
3
4
4atlem0be
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
S
∈
A
∧
¬
S
≤
˙
P
∨
˙
Q
→
P
≠
S
11
5
6
7
8
9
10
syl131anc
⊢
φ
→
P
≠
S