Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Norm Megill
Construction of a vector space from a Hilbert lattice
cdleme31snd
Next ⟩
cdleme31sdnN
Metamath Proof Explorer
Ascii
Unicode
Theorem
cdleme31snd
Description:
Part of proof of Lemma D in
Crawley
p. 113.
(Contributed by
NM
, 1-Apr-2013)
Ref
Expression
Hypotheses
cdleme31snd.d
⊢
D
=
t
∨
˙
U
∧
˙
Q
∨
˙
P
∨
˙
t
∧
˙
W
cdleme31snd.n
⊢
N
=
v
∨
˙
V
∧
˙
P
∨
˙
Q
∨
˙
v
∧
˙
W
cdleme31snd.e
⊢
E
=
O
∨
˙
U
∧
˙
Q
∨
˙
P
∨
˙
O
∧
˙
W
cdleme31snd.o
⊢
O
=
S
∨
˙
V
∧
˙
P
∨
˙
Q
∨
˙
S
∧
˙
W
Assertion
cdleme31snd
⊢
S
∈
A
→
⦋
S
/
v
⦌
⦋
N
/
t
⦌
D
=
E
Proof
Step
Hyp
Ref
Expression
1
cdleme31snd.d
⊢
D
=
t
∨
˙
U
∧
˙
Q
∨
˙
P
∨
˙
t
∧
˙
W
2
cdleme31snd.n
⊢
N
=
v
∨
˙
V
∧
˙
P
∨
˙
Q
∨
˙
v
∧
˙
W
3
cdleme31snd.e
⊢
E
=
O
∨
˙
U
∧
˙
Q
∨
˙
P
∨
˙
O
∧
˙
W
4
cdleme31snd.o
⊢
O
=
S
∨
˙
V
∧
˙
P
∨
˙
Q
∨
˙
S
∧
˙
W
5
csbnestgw
⊢
S
∈
A
→
⦋
S
/
v
⦌
⦋
N
/
t
⦌
D
=
⦋
⦋
S
/
v
⦌
N
/
t
⦌
D
6
2
4
cdleme31sc
⊢
S
∈
A
→
⦋
S
/
v
⦌
N
=
O
7
6
csbeq1d
⊢
S
∈
A
→
⦋
⦋
S
/
v
⦌
N
/
t
⦌
D
=
⦋
O
/
t
⦌
D
8
4
ovexi
⊢
O
∈
V
9
1
3
cdleme31sc
⊢
O
∈
V
→
⦋
O
/
t
⦌
D
=
E
10
8
9
ax-mp
⊢
⦋
O
/
t
⦌
D
=
E
11
7
10
eqtrdi
⊢
S
∈
A
→
⦋
⦋
S
/
v
⦌
N
/
t
⦌
D
=
E
12
5
11
eqtrd
⊢
S
∈
A
→
⦋
S
/
v
⦌
⦋
N
/
t
⦌
D
=
E