Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Norm Megill
Construction of a vector space from a Hilbert lattice
cdlemefr32snb
Next ⟩
cdlemefr29bpre0N
Metamath Proof Explorer
Ascii
Unicode
Theorem
cdlemefr32snb
Description:
Show closure of
[_ R / s ]_ N
.
(Contributed by
NM
, 28-Mar-2013)
Ref
Expression
Hypotheses
cdlemefr27.b
⊢
B
=
Base
K
cdlemefr27.l
⊢
≤
˙
=
≤
K
cdlemefr27.j
⊢
∨
˙
=
join
⁡
K
cdlemefr27.m
⊢
∧
˙
=
meet
⁡
K
cdlemefr27.a
⊢
A
=
Atoms
⁡
K
cdlemefr27.h
⊢
H
=
LHyp
⁡
K
cdlemefr27.u
⊢
U
=
P
∨
˙
Q
∧
˙
W
cdlemefr27.c
⊢
C
=
s
∨
˙
U
∧
˙
Q
∨
˙
P
∨
˙
s
∧
˙
W
cdlemefr27.n
⊢
N
=
if
s
≤
˙
P
∨
˙
Q
I
C
Assertion
cdlemefr32snb
⊢
K
∈
HL
∧
W
∈
H
∧
P
∈
A
∧
¬
P
≤
˙
W
∧
Q
∈
A
∧
¬
Q
≤
˙
W
∧
P
≠
Q
∧
R
∈
A
∧
¬
R
≤
˙
W
∧
¬
R
≤
˙
P
∨
˙
Q
→
⦋
R
/
s
⦌
N
∈
B
Proof
Step
Hyp
Ref
Expression
1
cdlemefr27.b
⊢
B
=
Base
K
2
cdlemefr27.l
⊢
≤
˙
=
≤
K
3
cdlemefr27.j
⊢
∨
˙
=
join
⁡
K
4
cdlemefr27.m
⊢
∧
˙
=
meet
⁡
K
5
cdlemefr27.a
⊢
A
=
Atoms
⁡
K
6
cdlemefr27.h
⊢
H
=
LHyp
⁡
K
7
cdlemefr27.u
⊢
U
=
P
∨
˙
Q
∧
˙
W
8
cdlemefr27.c
⊢
C
=
s
∨
˙
U
∧
˙
Q
∨
˙
P
∨
˙
s
∧
˙
W
9
cdlemefr27.n
⊢
N
=
if
s
≤
˙
P
∨
˙
Q
I
C
10
1
2
3
4
5
6
7
8
9
cdlemefr32sn2aw
⊢
K
∈
HL
∧
W
∈
H
∧
P
∈
A
∧
¬
P
≤
˙
W
∧
Q
∈
A
∧
¬
Q
≤
˙
W
∧
P
≠
Q
∧
R
∈
A
∧
¬
R
≤
˙
W
∧
¬
R
≤
˙
P
∨
˙
Q
→
⦋
R
/
s
⦌
N
∈
A
∧
¬
⦋
R
/
s
⦌
N
≤
˙
W
11
10
simpld
⊢
K
∈
HL
∧
W
∈
H
∧
P
∈
A
∧
¬
P
≤
˙
W
∧
Q
∈
A
∧
¬
Q
≤
˙
W
∧
P
≠
Q
∧
R
∈
A
∧
¬
R
≤
˙
W
∧
¬
R
≤
˙
P
∨
˙
Q
→
⦋
R
/
s
⦌
N
∈
A
12
1
5
atbase
⊢
⦋
R
/
s
⦌
N
∈
A
→
⦋
R
/
s
⦌
N
∈
B
13
11
12
syl
⊢
K
∈
HL
∧
W
∈
H
∧
P
∈
A
∧
¬
P
≤
˙
W
∧
Q
∈
A
∧
¬
Q
≤
˙
W
∧
P
≠
Q
∧
R
∈
A
∧
¬
R
≤
˙
W
∧
¬
R
≤
˙
P
∨
˙
Q
→
⦋
R
/
s
⦌
N
∈
B