Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Norm Megill
Projective geometries based on Hilbert lattices
lvoli
Next ⟩
islvol3
Metamath Proof Explorer
Ascii
Unicode
Theorem
lvoli
Description:
Condition implying a 3-dim lattice volume.
(Contributed by
NM
, 1-Jul-2012)
Ref
Expression
Hypotheses
lvolset.b
⊢
B
=
Base
K
lvolset.c
⊢
C
=
⋖
K
lvolset.p
⊢
P
=
LPlanes
⁡
K
lvolset.v
⊢
V
=
LVols
⁡
K
Assertion
lvoli
⊢
K
∈
D
∧
Y
∈
B
∧
X
∈
P
∧
X
C
Y
→
Y
∈
V
Proof
Step
Hyp
Ref
Expression
1
lvolset.b
⊢
B
=
Base
K
2
lvolset.c
⊢
C
=
⋖
K
3
lvolset.p
⊢
P
=
LPlanes
⁡
K
4
lvolset.v
⊢
V
=
LVols
⁡
K
5
simpl2
⊢
K
∈
D
∧
Y
∈
B
∧
X
∈
P
∧
X
C
Y
→
Y
∈
B
6
breq1
⊢
x
=
X
→
x
C
Y
↔
X
C
Y
7
6
rspcev
⊢
X
∈
P
∧
X
C
Y
→
∃
x
∈
P
x
C
Y
8
7
3ad2antl3
⊢
K
∈
D
∧
Y
∈
B
∧
X
∈
P
∧
X
C
Y
→
∃
x
∈
P
x
C
Y
9
simpl1
⊢
K
∈
D
∧
Y
∈
B
∧
X
∈
P
∧
X
C
Y
→
K
∈
D
10
1
2
3
4
islvol
⊢
K
∈
D
→
Y
∈
V
↔
Y
∈
B
∧
∃
x
∈
P
x
C
Y
11
9
10
syl
⊢
K
∈
D
∧
Y
∈
B
∧
X
∈
P
∧
X
C
Y
→
Y
∈
V
↔
Y
∈
B
∧
∃
x
∈
P
x
C
Y
12
5
8
11
mpbir2and
⊢
K
∈
D
∧
Y
∈
B
∧
X
∈
P
∧
X
C
Y
→
Y
∈
V