Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Norm Megill
Construction of a vector space from a Hilbert lattice
cdleme31fv1s
Next ⟩
cdleme31fv2
Metamath Proof Explorer
Ascii
Unicode
Theorem
cdleme31fv1s
Description:
Part of proof of Lemma E in
Crawley
p. 113.
(Contributed by
NM
, 25-Feb-2013)
Ref
Expression
Hypotheses
cdleme31.o
⊢
O
=
ι
z
∈
B
|
∀
s
∈
A
¬
s
≤
˙
W
∧
s
∨
˙
x
∧
˙
W
=
x
→
z
=
N
∨
˙
x
∧
˙
W
cdleme31.f
⊢
F
=
x
∈
B
⟼
if
P
≠
Q
∧
¬
x
≤
˙
W
O
x
Assertion
cdleme31fv1s
⊢
X
∈
B
∧
P
≠
Q
∧
¬
X
≤
˙
W
→
F
⁡
X
=
⦋
X
/
x
⦌
O
Proof
Step
Hyp
Ref
Expression
1
cdleme31.o
⊢
O
=
ι
z
∈
B
|
∀
s
∈
A
¬
s
≤
˙
W
∧
s
∨
˙
x
∧
˙
W
=
x
→
z
=
N
∨
˙
x
∧
˙
W
2
cdleme31.f
⊢
F
=
x
∈
B
⟼
if
P
≠
Q
∧
¬
x
≤
˙
W
O
x
3
eqid
⊢
ι
z
∈
B
|
∀
s
∈
A
¬
s
≤
˙
W
∧
s
∨
˙
X
∧
˙
W
=
X
→
z
=
N
∨
˙
X
∧
˙
W
=
ι
z
∈
B
|
∀
s
∈
A
¬
s
≤
˙
W
∧
s
∨
˙
X
∧
˙
W
=
X
→
z
=
N
∨
˙
X
∧
˙
W
4
1
2
3
cdleme31fv1
⊢
X
∈
B
∧
P
≠
Q
∧
¬
X
≤
˙
W
→
F
⁡
X
=
ι
z
∈
B
|
∀
s
∈
A
¬
s
≤
˙
W
∧
s
∨
˙
X
∧
˙
W
=
X
→
z
=
N
∨
˙
X
∧
˙
W
5
1
3
cdleme31so
⊢
X
∈
B
→
⦋
X
/
x
⦌
O
=
ι
z
∈
B
|
∀
s
∈
A
¬
s
≤
˙
W
∧
s
∨
˙
X
∧
˙
W
=
X
→
z
=
N
∨
˙
X
∧
˙
W
6
5
adantr
⊢
X
∈
B
∧
P
≠
Q
∧
¬
X
≤
˙
W
→
⦋
X
/
x
⦌
O
=
ι
z
∈
B
|
∀
s
∈
A
¬
s
≤
˙
W
∧
s
∨
˙
X
∧
˙
W
=
X
→
z
=
N
∨
˙
X
∧
˙
W
7
4
6
eqtr4d
⊢
X
∈
B
∧
P
≠
Q
∧
¬
X
≤
˙
W
→
F
⁡
X
=
⦋
X
/
x
⦌
O