Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Norm Megill
Construction of a vector space from a Hilbert lattice
cdleme50ex
Next ⟩
cdleme
Metamath Proof Explorer
Ascii
Unicode
Theorem
cdleme50ex
Description:
Part of Lemma E in
Crawley
p. 113. TODO: fix comment.
(Contributed by
NM
, 11-Apr-2013)
Ref
Expression
Hypotheses
cdleme.l
⊢
≤
˙
=
≤
K
cdleme.a
⊢
A
=
Atoms
⁡
K
cdleme.h
⊢
H
=
LHyp
⁡
K
cdleme.t
⊢
T
=
LTrn
⁡
K
⁡
W
Assertion
cdleme50ex
⊢
K
∈
HL
∧
W
∈
H
∧
P
∈
A
∧
¬
P
≤
˙
W
∧
Q
∈
A
∧
¬
Q
≤
˙
W
→
∃
f
∈
T
f
⁡
P
=
Q
Proof
Step
Hyp
Ref
Expression
1
cdleme.l
⊢
≤
˙
=
≤
K
2
cdleme.a
⊢
A
=
Atoms
⁡
K
3
cdleme.h
⊢
H
=
LHyp
⁡
K
4
cdleme.t
⊢
T
=
LTrn
⁡
K
⁡
W
5
eqid
⊢
Base
K
=
Base
K
6
eqid
⊢
join
⁡
K
=
join
⁡
K
7
eqid
⊢
meet
⁡
K
=
meet
⁡
K
8
eqid
⊢
P
join
⁡
K
Q
meet
⁡
K
W
=
P
join
⁡
K
Q
meet
⁡
K
W
9
eqid
⊢
t
join
⁡
K
P
join
⁡
K
Q
meet
⁡
K
W
meet
⁡
K
Q
join
⁡
K
P
join
⁡
K
t
meet
⁡
K
W
=
t
join
⁡
K
P
join
⁡
K
Q
meet
⁡
K
W
meet
⁡
K
Q
join
⁡
K
P
join
⁡
K
t
meet
⁡
K
W
10
eqid
⊢
P
join
⁡
K
Q
meet
⁡
K
t
join
⁡
K
P
join
⁡
K
Q
meet
⁡
K
W
meet
⁡
K
Q
join
⁡
K
P
join
⁡
K
t
meet
⁡
K
W
join
⁡
K
s
join
⁡
K
t
meet
⁡
K
W
=
P
join
⁡
K
Q
meet
⁡
K
t
join
⁡
K
P
join
⁡
K
Q
meet
⁡
K
W
meet
⁡
K
Q
join
⁡
K
P
join
⁡
K
t
meet
⁡
K
W
join
⁡
K
s
join
⁡
K
t
meet
⁡
K
W
11
eqid
⊢
x
∈
Base
K
⟼
if
P
≠
Q
∧
¬
x
≤
˙
W
ι
z
∈
Base
K
|
∀
s
∈
A
¬
s
≤
˙
W
∧
s
join
⁡
K
x
meet
⁡
K
W
=
x
→
z
=
if
s
≤
˙
P
join
⁡
K
Q
ι
y
∈
Base
K
|
∀
t
∈
A
¬
t
≤
˙
W
∧
¬
t
≤
˙
P
join
⁡
K
Q
→
y
=
P
join
⁡
K
Q
meet
⁡
K
t
join
⁡
K
P
join
⁡
K
Q
meet
⁡
K
W
meet
⁡
K
Q
join
⁡
K
P
join
⁡
K
t
meet
⁡
K
W
join
⁡
K
s
join
⁡
K
t
meet
⁡
K
W
⦋
s
/
t
⦌
t
join
⁡
K
P
join
⁡
K
Q
meet
⁡
K
W
meet
⁡
K
Q
join
⁡
K
P
join
⁡
K
t
meet
⁡
K
W
join
⁡
K
x
meet
⁡
K
W
x
=
x
∈
Base
K
⟼
if
P
≠
Q
∧
¬
x
≤
˙
W
ι
z
∈
Base
K
|
∀
s
∈
A
¬
s
≤
˙
W
∧
s
join
⁡
K
x
meet
⁡
K
W
=
x
→
z
=
if
s
≤
˙
P
join
⁡
K
Q
ι
y
∈
Base
K
|
∀
t
∈
A
¬
t
≤
˙
W
∧
¬
t
≤
˙
P
join
⁡
K
Q
→
y
=
P
join
⁡
K
Q
meet
⁡
K
t
join
⁡
K
P
join
⁡
K
Q
meet
⁡
K
W
meet
⁡
K
Q
join
⁡
K
P
join
⁡
K
t
meet
⁡
K
W
join
⁡
K
s
join
⁡
K
t
meet
⁡
K
W
⦋
s
/
t
⦌
t
join
⁡
K
P
join
⁡
K
Q
meet
⁡
K
W
meet
⁡
K
Q
join
⁡
K
P
join
⁡
K
t
meet
⁡
K
W
join
⁡
K
x
meet
⁡
K
W
x
12
5
1
6
7
2
3
8
9
10
11
4
cdleme50ltrn
⊢
K
∈
HL
∧
W
∈
H
∧
P
∈
A
∧
¬
P
≤
˙
W
∧
Q
∈
A
∧
¬
Q
≤
˙
W
→
x
∈
Base
K
⟼
if
P
≠
Q
∧
¬
x
≤
˙
W
ι
z
∈
Base
K
|
∀
s
∈
A
¬
s
≤
˙
W
∧
s
join
⁡
K
x
meet
⁡
K
W
=
x
→
z
=
if
s
≤
˙
P
join
⁡
K
Q
ι
y
∈
Base
K
|
∀
t
∈
A
¬
t
≤
˙
W
∧
¬
t
≤
˙
P
join
⁡
K
Q
→
y
=
P
join
⁡
K
Q
meet
⁡
K
t
join
⁡
K
P
join
⁡
K
Q
meet
⁡
K
W
meet
⁡
K
Q
join
⁡
K
P
join
⁡
K
t
meet
⁡
K
W
join
⁡
K
s
join
⁡
K
t
meet
⁡
K
W
⦋
s
/
t
⦌
t
join
⁡
K
P
join
⁡
K
Q
meet
⁡
K
W
meet
⁡
K
Q
join
⁡
K
P
join
⁡
K
t
meet
⁡
K
W
join
⁡
K
x
meet
⁡
K
W
x
∈
T
13
5
1
6
7
2
3
8
9
10
11
cdleme17d
⊢
K
∈
HL
∧
W
∈
H
∧
P
∈
A
∧
¬
P
≤
˙
W
∧
Q
∈
A
∧
¬
Q
≤
˙
W
→
x
∈
Base
K
⟼
if
P
≠
Q
∧
¬
x
≤
˙
W
ι
z
∈
Base
K
|
∀
s
∈
A
¬
s
≤
˙
W
∧
s
join
⁡
K
x
meet
⁡
K
W
=
x
→
z
=
if
s
≤
˙
P
join
⁡
K
Q
ι
y
∈
Base
K
|
∀
t
∈
A
¬
t
≤
˙
W
∧
¬
t
≤
˙
P
join
⁡
K
Q
→
y
=
P
join
⁡
K
Q
meet
⁡
K
t
join
⁡
K
P
join
⁡
K
Q
meet
⁡
K
W
meet
⁡
K
Q
join
⁡
K
P
join
⁡
K
t
meet
⁡
K
W
join
⁡
K
s
join
⁡
K
t
meet
⁡
K
W
⦋
s
/
t
⦌
t
join
⁡
K
P
join
⁡
K
Q
meet
⁡
K
W
meet
⁡
K
Q
join
⁡
K
P
join
⁡
K
t
meet
⁡
K
W
join
⁡
K
x
meet
⁡
K
W
x
⁡
P
=
Q
14
fveq1
⊢
f
=
x
∈
Base
K
⟼
if
P
≠
Q
∧
¬
x
≤
˙
W
ι
z
∈
Base
K
|
∀
s
∈
A
¬
s
≤
˙
W
∧
s
join
⁡
K
x
meet
⁡
K
W
=
x
→
z
=
if
s
≤
˙
P
join
⁡
K
Q
ι
y
∈
Base
K
|
∀
t
∈
A
¬
t
≤
˙
W
∧
¬
t
≤
˙
P
join
⁡
K
Q
→
y
=
P
join
⁡
K
Q
meet
⁡
K
t
join
⁡
K
P
join
⁡
K
Q
meet
⁡
K
W
meet
⁡
K
Q
join
⁡
K
P
join
⁡
K
t
meet
⁡
K
W
join
⁡
K
s
join
⁡
K
t
meet
⁡
K
W
⦋
s
/
t
⦌
t
join
⁡
K
P
join
⁡
K
Q
meet
⁡
K
W
meet
⁡
K
Q
join
⁡
K
P
join
⁡
K
t
meet
⁡
K
W
join
⁡
K
x
meet
⁡
K
W
x
→
f
⁡
P
=
x
∈
Base
K
⟼
if
P
≠
Q
∧
¬
x
≤
˙
W
ι
z
∈
Base
K
|
∀
s
∈
A
¬
s
≤
˙
W
∧
s
join
⁡
K
x
meet
⁡
K
W
=
x
→
z
=
if
s
≤
˙
P
join
⁡
K
Q
ι
y
∈
Base
K
|
∀
t
∈
A
¬
t
≤
˙
W
∧
¬
t
≤
˙
P
join
⁡
K
Q
→
y
=
P
join
⁡
K
Q
meet
⁡
K
t
join
⁡
K
P
join
⁡
K
Q
meet
⁡
K
W
meet
⁡
K
Q
join
⁡
K
P
join
⁡
K
t
meet
⁡
K
W
join
⁡
K
s
join
⁡
K
t
meet
⁡
K
W
⦋
s
/
t
⦌
t
join
⁡
K
P
join
⁡
K
Q
meet
⁡
K
W
meet
⁡
K
Q
join
⁡
K
P
join
⁡
K
t
meet
⁡
K
W
join
⁡
K
x
meet
⁡
K
W
x
⁡
P
15
14
eqeq1d
⊢
f
=
x
∈
Base
K
⟼
if
P
≠
Q
∧
¬
x
≤
˙
W
ι
z
∈
Base
K
|
∀
s
∈
A
¬
s
≤
˙
W
∧
s
join
⁡
K
x
meet
⁡
K
W
=
x
→
z
=
if
s
≤
˙
P
join
⁡
K
Q
ι
y
∈
Base
K
|
∀
t
∈
A
¬
t
≤
˙
W
∧
¬
t
≤
˙
P
join
⁡
K
Q
→
y
=
P
join
⁡
K
Q
meet
⁡
K
t
join
⁡
K
P
join
⁡
K
Q
meet
⁡
K
W
meet
⁡
K
Q
join
⁡
K
P
join
⁡
K
t
meet
⁡
K
W
join
⁡
K
s
join
⁡
K
t
meet
⁡
K
W
⦋
s
/
t
⦌
t
join
⁡
K
P
join
⁡
K
Q
meet
⁡
K
W
meet
⁡
K
Q
join
⁡
K
P
join
⁡
K
t
meet
⁡
K
W
join
⁡
K
x
meet
⁡
K
W
x
→
f
⁡
P
=
Q
↔
x
∈
Base
K
⟼
if
P
≠
Q
∧
¬
x
≤
˙
W
ι
z
∈
Base
K
|
∀
s
∈
A
¬
s
≤
˙
W
∧
s
join
⁡
K
x
meet
⁡
K
W
=
x
→
z
=
if
s
≤
˙
P
join
⁡
K
Q
ι
y
∈
Base
K
|
∀
t
∈
A
¬
t
≤
˙
W
∧
¬
t
≤
˙
P
join
⁡
K
Q
→
y
=
P
join
⁡
K
Q
meet
⁡
K
t
join
⁡
K
P
join
⁡
K
Q
meet
⁡
K
W
meet
⁡
K
Q
join
⁡
K
P
join
⁡
K
t
meet
⁡
K
W
join
⁡
K
s
join
⁡
K
t
meet
⁡
K
W
⦋
s
/
t
⦌
t
join
⁡
K
P
join
⁡
K
Q
meet
⁡
K
W
meet
⁡
K
Q
join
⁡
K
P
join
⁡
K
t
meet
⁡
K
W
join
⁡
K
x
meet
⁡
K
W
x
⁡
P
=
Q
16
15
rspcev
⊢
x
∈
Base
K
⟼
if
P
≠
Q
∧
¬
x
≤
˙
W
ι
z
∈
Base
K
|
∀
s
∈
A
¬
s
≤
˙
W
∧
s
join
⁡
K
x
meet
⁡
K
W
=
x
→
z
=
if
s
≤
˙
P
join
⁡
K
Q
ι
y
∈
Base
K
|
∀
t
∈
A
¬
t
≤
˙
W
∧
¬
t
≤
˙
P
join
⁡
K
Q
→
y
=
P
join
⁡
K
Q
meet
⁡
K
t
join
⁡
K
P
join
⁡
K
Q
meet
⁡
K
W
meet
⁡
K
Q
join
⁡
K
P
join
⁡
K
t
meet
⁡
K
W
join
⁡
K
s
join
⁡
K
t
meet
⁡
K
W
⦋
s
/
t
⦌
t
join
⁡
K
P
join
⁡
K
Q
meet
⁡
K
W
meet
⁡
K
Q
join
⁡
K
P
join
⁡
K
t
meet
⁡
K
W
join
⁡
K
x
meet
⁡
K
W
x
∈
T
∧
x
∈
Base
K
⟼
if
P
≠
Q
∧
¬
x
≤
˙
W
ι
z
∈
Base
K
|
∀
s
∈
A
¬
s
≤
˙
W
∧
s
join
⁡
K
x
meet
⁡
K
W
=
x
→
z
=
if
s
≤
˙
P
join
⁡
K
Q
ι
y
∈
Base
K
|
∀
t
∈
A
¬
t
≤
˙
W
∧
¬
t
≤
˙
P
join
⁡
K
Q
→
y
=
P
join
⁡
K
Q
meet
⁡
K
t
join
⁡
K
P
join
⁡
K
Q
meet
⁡
K
W
meet
⁡
K
Q
join
⁡
K
P
join
⁡
K
t
meet
⁡
K
W
join
⁡
K
s
join
⁡
K
t
meet
⁡
K
W
⦋
s
/
t
⦌
t
join
⁡
K
P
join
⁡
K
Q
meet
⁡
K
W
meet
⁡
K
Q
join
⁡
K
P
join
⁡
K
t
meet
⁡
K
W
join
⁡
K
x
meet
⁡
K
W
x
⁡
P
=
Q
→
∃
f
∈
T
f
⁡
P
=
Q
17
12
13
16
syl2anc
⊢
K
∈
HL
∧
W
∈
H
∧
P
∈
A
∧
¬
P
≤
˙
W
∧
Q
∈
A
∧
¬
Q
≤
˙
W
→
∃
f
∈
T
f
⁡
P
=
Q