Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Norm Megill
Construction of a vector space from a Hilbert lattice
watfvalN
Next ⟩
watvalN
Metamath Proof Explorer
Ascii
Unicode
Theorem
watfvalN
Description:
The W atoms function.
(Contributed by
NM
, 26-Jan-2012)
(New usage is discouraged.)
Ref
Expression
Hypotheses
watomfval.a
⊢
A
=
Atoms
⁡
K
watomfval.p
⊢
P
=
⊥
𝑃
⁡
K
watomfval.w
⊢
W
=
WAtoms
⁡
K
Assertion
watfvalN
⊢
K
∈
B
→
W
=
d
∈
A
⟼
A
∖
⊥
𝑃
⁡
K
⁡
d
Proof
Step
Hyp
Ref
Expression
1
watomfval.a
⊢
A
=
Atoms
⁡
K
2
watomfval.p
⊢
P
=
⊥
𝑃
⁡
K
3
watomfval.w
⊢
W
=
WAtoms
⁡
K
4
elex
⊢
K
∈
B
→
K
∈
V
5
fveq2
⊢
k
=
K
→
Atoms
⁡
k
=
Atoms
⁡
K
6
5
1
eqtr4di
⊢
k
=
K
→
Atoms
⁡
k
=
A
7
fveq2
⊢
k
=
K
→
⊥
𝑃
⁡
k
=
⊥
𝑃
⁡
K
8
7
fveq1d
⊢
k
=
K
→
⊥
𝑃
⁡
k
⁡
d
=
⊥
𝑃
⁡
K
⁡
d
9
6
8
difeq12d
⊢
k
=
K
→
Atoms
⁡
k
∖
⊥
𝑃
⁡
k
⁡
d
=
A
∖
⊥
𝑃
⁡
K
⁡
d
10
6
9
mpteq12dv
⊢
k
=
K
→
d
∈
Atoms
⁡
k
⟼
Atoms
⁡
k
∖
⊥
𝑃
⁡
k
⁡
d
=
d
∈
A
⟼
A
∖
⊥
𝑃
⁡
K
⁡
d
11
df-watsN
⊢
WAtoms
=
k
∈
V
⟼
d
∈
Atoms
⁡
k
⟼
Atoms
⁡
k
∖
⊥
𝑃
⁡
k
⁡
d
12
10
11
1
mptfvmpt
⊢
K
∈
V
→
WAtoms
⁡
K
=
d
∈
A
⟼
A
∖
⊥
𝑃
⁡
K
⁡
d
13
3
12
syl5eq
⊢
K
∈
V
→
W
=
d
∈
A
⟼
A
∖
⊥
𝑃
⁡
K
⁡
d
14
4
13
syl
⊢
K
∈
B
→
W
=
d
∈
A
⟼
A
∖
⊥
𝑃
⁡
K
⁡
d