Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Norm Megill
Projective geometries based on Hilbert lattices
islvol
Next ⟩
islvol4
Metamath Proof Explorer
Ascii
Unicode
Theorem
islvol
Description:
The predicate "is 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
islvol
⊢
K
∈
A
→
X
∈
V
↔
X
∈
B
∧
∃
y
∈
P
y
C
X
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
1
2
3
4
lvolset
⊢
K
∈
A
→
V
=
x
∈
B
|
∃
y
∈
P
y
C
x
6
5
eleq2d
⊢
K
∈
A
→
X
∈
V
↔
X
∈
x
∈
B
|
∃
y
∈
P
y
C
x
7
breq2
⊢
x
=
X
→
y
C
x
↔
y
C
X
8
7
rexbidv
⊢
x
=
X
→
∃
y
∈
P
y
C
x
↔
∃
y
∈
P
y
C
X
9
8
elrab
⊢
X
∈
x
∈
B
|
∃
y
∈
P
y
C
x
↔
X
∈
B
∧
∃
y
∈
P
y
C
X
10
6
9
syl6bb
⊢
K
∈
A
→
X
∈
V
↔
X
∈
B
∧
∃
y
∈
P
y
C
X