Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Norm Megill
Construction of a vector space from a Hilbert lattice
cdleme31se
Next ⟩
cdleme31se2
Metamath Proof Explorer
Ascii
Unicode
Theorem
cdleme31se
Description:
Part of proof of Lemma D in
Crawley
p. 113.
(Contributed by
NM
, 26-Feb-2013)
Ref
Expression
Hypotheses
cdleme31se.e
⊢
E
=
P
∨
˙
Q
∧
˙
D
∨
˙
s
∨
˙
T
∧
˙
W
cdleme31se.y
⊢
Y
=
P
∨
˙
Q
∧
˙
D
∨
˙
R
∨
˙
T
∧
˙
W
Assertion
cdleme31se
⊢
R
∈
A
→
⦋
R
/
s
⦌
E
=
Y
Proof
Step
Hyp
Ref
Expression
1
cdleme31se.e
⊢
E
=
P
∨
˙
Q
∧
˙
D
∨
˙
s
∨
˙
T
∧
˙
W
2
cdleme31se.y
⊢
Y
=
P
∨
˙
Q
∧
˙
D
∨
˙
R
∨
˙
T
∧
˙
W
3
nfcvd
⊢
R
∈
A
→
Ⅎ
_
s
P
∨
˙
Q
∧
˙
D
∨
˙
R
∨
˙
T
∧
˙
W
4
oveq1
⊢
s
=
R
→
s
∨
˙
T
=
R
∨
˙
T
5
4
oveq1d
⊢
s
=
R
→
s
∨
˙
T
∧
˙
W
=
R
∨
˙
T
∧
˙
W
6
5
oveq2d
⊢
s
=
R
→
D
∨
˙
s
∨
˙
T
∧
˙
W
=
D
∨
˙
R
∨
˙
T
∧
˙
W
7
6
oveq2d
⊢
s
=
R
→
P
∨
˙
Q
∧
˙
D
∨
˙
s
∨
˙
T
∧
˙
W
=
P
∨
˙
Q
∧
˙
D
∨
˙
R
∨
˙
T
∧
˙
W
8
3
7
csbiegf
⊢
R
∈
A
→
⦋
R
/
s
⦌
P
∨
˙
Q
∧
˙
D
∨
˙
s
∨
˙
T
∧
˙
W
=
P
∨
˙
Q
∧
˙
D
∨
˙
R
∨
˙
T
∧
˙
W
9
1
csbeq2i
⊢
⦋
R
/
s
⦌
E
=
⦋
R
/
s
⦌
P
∨
˙
Q
∧
˙
D
∨
˙
s
∨
˙
T
∧
˙
W
10
8
9
2
3eqtr4g
⊢
R
∈
A
→
⦋
R
/
s
⦌
E
=
Y