Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Norm Megill
Construction of a vector space from a Hilbert lattice
dalawlem14
Next ⟩
dalawlem15
Metamath Proof Explorer
Ascii
Unicode
Theorem
dalawlem14
Description:
Lemma for
dalaw
. Combine
dalawlem10
and
dalawlem13
.
(Contributed by
NM
, 6-Oct-2012)
Ref
Expression
Hypotheses
dalawlem.l
⊢
≤
˙
=
≤
K
dalawlem.j
⊢
∨
˙
=
join
⁡
K
dalawlem.m
⊢
∧
˙
=
meet
⁡
K
dalawlem.a
⊢
A
=
Atoms
⁡
K
dalawlem2.o
⊢
O
=
LPlanes
⁡
K
Assertion
dalawlem14
⊢
K
∈
HL
∧
¬
P
∨
˙
Q
∨
˙
R
∈
O
∧
¬
P
∨
˙
S
∧
˙
Q
∨
˙
T
≤
˙
P
∨
˙
Q
∧
¬
P
∨
˙
S
∧
˙
Q
∨
˙
T
≤
˙
Q
∨
˙
R
∧
¬
P
∨
˙
S
∧
˙
Q
∨
˙
T
≤
˙
R
∨
˙
P
∧
P
∨
˙
S
∧
˙
Q
∨
˙
T
≤
˙
R
∨
˙
U
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
→
P
∨
˙
Q
∧
˙
S
∨
˙
T
≤
˙
Q
∨
˙
R
∧
˙
T
∨
˙
U
∨
˙
R
∨
˙
P
∧
˙
U
∨
˙
S
Proof
Step
Hyp
Ref
Expression
1
dalawlem.l
⊢
≤
˙
=
≤
K
2
dalawlem.j
⊢
∨
˙
=
join
⁡
K
3
dalawlem.m
⊢
∧
˙
=
meet
⁡
K
4
dalawlem.a
⊢
A
=
Atoms
⁡
K
5
dalawlem2.o
⊢
O
=
LPlanes
⁡
K
6
ianor
⊢
¬
P
∨
˙
Q
∨
˙
R
∈
O
∧
¬
P
∨
˙
S
∧
˙
Q
∨
˙
T
≤
˙
P
∨
˙
Q
∧
¬
P
∨
˙
S
∧
˙
Q
∨
˙
T
≤
˙
Q
∨
˙
R
∧
¬
P
∨
˙
S
∧
˙
Q
∨
˙
T
≤
˙
R
∨
˙
P
↔
¬
P
∨
˙
Q
∨
˙
R
∈
O
∨
¬
¬
P
∨
˙
S
∧
˙
Q
∨
˙
T
≤
˙
P
∨
˙
Q
∧
¬
P
∨
˙
S
∧
˙
Q
∨
˙
T
≤
˙
Q
∨
˙
R
∧
¬
P
∨
˙
S
∧
˙
Q
∨
˙
T
≤
˙
R
∨
˙
P
7
1
2
3
4
5
dalawlem13
⊢
K
∈
HL
∧
¬
P
∨
˙
Q
∨
˙
R
∈
O
∧
P
∨
˙
S
∧
˙
Q
∨
˙
T
≤
˙
R
∨
˙
U
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
→
P
∨
˙
Q
∧
˙
S
∨
˙
T
≤
˙
Q
∨
˙
R
∧
˙
T
∨
˙
U
∨
˙
R
∨
˙
P
∧
˙
U
∨
˙
S
8
7
3expib
⊢
K
∈
HL
∧
¬
P
∨
˙
Q
∨
˙
R
∈
O
∧
P
∨
˙
S
∧
˙
Q
∨
˙
T
≤
˙
R
∨
˙
U
→
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
→
P
∨
˙
Q
∧
˙
S
∨
˙
T
≤
˙
Q
∨
˙
R
∧
˙
T
∨
˙
U
∨
˙
R
∨
˙
P
∧
˙
U
∨
˙
S
9
8
3exp
⊢
K
∈
HL
→
¬
P
∨
˙
Q
∨
˙
R
∈
O
→
P
∨
˙
S
∧
˙
Q
∨
˙
T
≤
˙
R
∨
˙
U
→
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
→
P
∨
˙
Q
∧
˙
S
∨
˙
T
≤
˙
Q
∨
˙
R
∧
˙
T
∨
˙
U
∨
˙
R
∨
˙
P
∧
˙
U
∨
˙
S
10
1
2
3
4
dalawlem10
⊢
K
∈
HL
∧
¬
¬
P
∨
˙
S
∧
˙
Q
∨
˙
T
≤
˙
P
∨
˙
Q
∧
¬
P
∨
˙
S
∧
˙
Q
∨
˙
T
≤
˙
Q
∨
˙
R
∧
¬
P
∨
˙
S
∧
˙
Q
∨
˙
T
≤
˙
R
∨
˙
P
∧
P
∨
˙
S
∧
˙
Q
∨
˙
T
≤
˙
R
∨
˙
U
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
→
P
∨
˙
Q
∧
˙
S
∨
˙
T
≤
˙
Q
∨
˙
R
∧
˙
T
∨
˙
U
∨
˙
R
∨
˙
P
∧
˙
U
∨
˙
S
11
10
3expib
⊢
K
∈
HL
∧
¬
¬
P
∨
˙
S
∧
˙
Q
∨
˙
T
≤
˙
P
∨
˙
Q
∧
¬
P
∨
˙
S
∧
˙
Q
∨
˙
T
≤
˙
Q
∨
˙
R
∧
¬
P
∨
˙
S
∧
˙
Q
∨
˙
T
≤
˙
R
∨
˙
P
∧
P
∨
˙
S
∧
˙
Q
∨
˙
T
≤
˙
R
∨
˙
U
→
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
→
P
∨
˙
Q
∧
˙
S
∨
˙
T
≤
˙
Q
∨
˙
R
∧
˙
T
∨
˙
U
∨
˙
R
∨
˙
P
∧
˙
U
∨
˙
S
12
11
3exp
⊢
K
∈
HL
→
¬
¬
P
∨
˙
S
∧
˙
Q
∨
˙
T
≤
˙
P
∨
˙
Q
∧
¬
P
∨
˙
S
∧
˙
Q
∨
˙
T
≤
˙
Q
∨
˙
R
∧
¬
P
∨
˙
S
∧
˙
Q
∨
˙
T
≤
˙
R
∨
˙
P
→
P
∨
˙
S
∧
˙
Q
∨
˙
T
≤
˙
R
∨
˙
U
→
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
→
P
∨
˙
Q
∧
˙
S
∨
˙
T
≤
˙
Q
∨
˙
R
∧
˙
T
∨
˙
U
∨
˙
R
∨
˙
P
∧
˙
U
∨
˙
S
13
9
12
jaod
⊢
K
∈
HL
→
¬
P
∨
˙
Q
∨
˙
R
∈
O
∨
¬
¬
P
∨
˙
S
∧
˙
Q
∨
˙
T
≤
˙
P
∨
˙
Q
∧
¬
P
∨
˙
S
∧
˙
Q
∨
˙
T
≤
˙
Q
∨
˙
R
∧
¬
P
∨
˙
S
∧
˙
Q
∨
˙
T
≤
˙
R
∨
˙
P
→
P
∨
˙
S
∧
˙
Q
∨
˙
T
≤
˙
R
∨
˙
U
→
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
→
P
∨
˙
Q
∧
˙
S
∨
˙
T
≤
˙
Q
∨
˙
R
∧
˙
T
∨
˙
U
∨
˙
R
∨
˙
P
∧
˙
U
∨
˙
S
14
6
13
syl5bi
⊢
K
∈
HL
→
¬
P
∨
˙
Q
∨
˙
R
∈
O
∧
¬
P
∨
˙
S
∧
˙
Q
∨
˙
T
≤
˙
P
∨
˙
Q
∧
¬
P
∨
˙
S
∧
˙
Q
∨
˙
T
≤
˙
Q
∨
˙
R
∧
¬
P
∨
˙
S
∧
˙
Q
∨
˙
T
≤
˙
R
∨
˙
P
→
P
∨
˙
S
∧
˙
Q
∨
˙
T
≤
˙
R
∨
˙
U
→
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
→
P
∨
˙
Q
∧
˙
S
∨
˙
T
≤
˙
Q
∨
˙
R
∧
˙
T
∨
˙
U
∨
˙
R
∨
˙
P
∧
˙
U
∨
˙
S
15
14
3imp
⊢
K
∈
HL
∧
¬
P
∨
˙
Q
∨
˙
R
∈
O
∧
¬
P
∨
˙
S
∧
˙
Q
∨
˙
T
≤
˙
P
∨
˙
Q
∧
¬
P
∨
˙
S
∧
˙
Q
∨
˙
T
≤
˙
Q
∨
˙
R
∧
¬
P
∨
˙
S
∧
˙
Q
∨
˙
T
≤
˙
R
∨
˙
P
∧
P
∨
˙
S
∧
˙
Q
∨
˙
T
≤
˙
R
∨
˙
U
→
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
→
P
∨
˙
Q
∧
˙
S
∨
˙
T
≤
˙
Q
∨
˙
R
∧
˙
T
∨
˙
U
∨
˙
R
∨
˙
P
∧
˙
U
∨
˙
S
16
15
3impib
⊢
K
∈
HL
∧
¬
P
∨
˙
Q
∨
˙
R
∈
O
∧
¬
P
∨
˙
S
∧
˙
Q
∨
˙
T
≤
˙
P
∨
˙
Q
∧
¬
P
∨
˙
S
∧
˙
Q
∨
˙
T
≤
˙
Q
∨
˙
R
∧
¬
P
∨
˙
S
∧
˙
Q
∨
˙
T
≤
˙
R
∨
˙
P
∧
P
∨
˙
S
∧
˙
Q
∨
˙
T
≤
˙
R
∨
˙
U
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
→
P
∨
˙
Q
∧
˙
S
∨
˙
T
≤
˙
Q
∨
˙
R
∧
˙
T
∨
˙
U
∨
˙
R
∨
˙
P
∧
˙
U
∨
˙
S