Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Norm Megill
Construction of a vector space from a Hilbert lattice
dihmeetlem5
Next ⟩
dihmeetlem6
Metamath Proof Explorer
Ascii
Unicode
Theorem
dihmeetlem5
Description:
Part of proof that isomorphism H is order-preserving .
(Contributed by
NM
, 6-Apr-2014)
Ref
Expression
Hypotheses
dihmeetlem5.b
⊢
B
=
Base
K
dihmeetlem5.l
⊢
≤
˙
=
≤
K
dihmeetlem5.j
⊢
∨
˙
=
join
⁡
K
dihmeetlem5.m
⊢
∧
˙
=
meet
⁡
K
dihmeetlem5.a
⊢
A
=
Atoms
⁡
K
Assertion
dihmeetlem5
⊢
K
∈
HL
∧
X
∈
B
∧
Y
∈
B
∧
Q
∈
A
∧
Q
≤
˙
X
→
X
∧
˙
Y
∨
˙
Q
=
X
∧
˙
Y
∨
˙
Q
Proof
Step
Hyp
Ref
Expression
1
dihmeetlem5.b
⊢
B
=
Base
K
2
dihmeetlem5.l
⊢
≤
˙
=
≤
K
3
dihmeetlem5.j
⊢
∨
˙
=
join
⁡
K
4
dihmeetlem5.m
⊢
∧
˙
=
meet
⁡
K
5
dihmeetlem5.a
⊢
A
=
Atoms
⁡
K
6
simpl1
⊢
K
∈
HL
∧
X
∈
B
∧
Y
∈
B
∧
Q
∈
A
∧
Q
≤
˙
X
→
K
∈
HL
7
simprl
⊢
K
∈
HL
∧
X
∈
B
∧
Y
∈
B
∧
Q
∈
A
∧
Q
≤
˙
X
→
Q
∈
A
8
simpl2
⊢
K
∈
HL
∧
X
∈
B
∧
Y
∈
B
∧
Q
∈
A
∧
Q
≤
˙
X
→
X
∈
B
9
simpl3
⊢
K
∈
HL
∧
X
∈
B
∧
Y
∈
B
∧
Q
∈
A
∧
Q
≤
˙
X
→
Y
∈
B
10
simprr
⊢
K
∈
HL
∧
X
∈
B
∧
Y
∈
B
∧
Q
∈
A
∧
Q
≤
˙
X
→
Q
≤
˙
X
11
1
2
3
4
5
atmod2i1
⊢
K
∈
HL
∧
Q
∈
A
∧
X
∈
B
∧
Y
∈
B
∧
Q
≤
˙
X
→
X
∧
˙
Y
∨
˙
Q
=
X
∧
˙
Y
∨
˙
Q
12
6
7
8
9
10
11
syl131anc
⊢
K
∈
HL
∧
X
∈
B
∧
Y
∈
B
∧
Q
∈
A
∧
Q
≤
˙
X
→
X
∧
˙
Y
∨
˙
Q
=
X
∧
˙
Y
∨
˙
Q
13
12
eqcomd
⊢
K
∈
HL
∧
X
∈
B
∧
Y
∈
B
∧
Q
∈
A
∧
Q
≤
˙
X
→
X
∧
˙
Y
∨
˙
Q
=
X
∧
˙
Y
∨
˙
Q