Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Norm Megill
Projective geometries based on Hilbert lattices
islpln
Next ⟩
islpln4
Metamath Proof Explorer
Ascii
Unicode
Theorem
islpln
Description:
The predicate "is a lattice plane".
(Contributed by
NM
, 16-Jun-2012)
Ref
Expression
Hypotheses
lplnset.b
⊢
B
=
Base
K
lplnset.c
⊢
C
=
⋖
K
lplnset.n
⊢
N
=
LLines
⁡
K
lplnset.p
⊢
P
=
LPlanes
⁡
K
Assertion
islpln
⊢
K
∈
A
→
X
∈
P
↔
X
∈
B
∧
∃
y
∈
N
y
C
X
Proof
Step
Hyp
Ref
Expression
1
lplnset.b
⊢
B
=
Base
K
2
lplnset.c
⊢
C
=
⋖
K
3
lplnset.n
⊢
N
=
LLines
⁡
K
4
lplnset.p
⊢
P
=
LPlanes
⁡
K
5
1
2
3
4
lplnset
⊢
K
∈
A
→
P
=
x
∈
B
|
∃
y
∈
N
y
C
x
6
5
eleq2d
⊢
K
∈
A
→
X
∈
P
↔
X
∈
x
∈
B
|
∃
y
∈
N
y
C
x
7
breq2
⊢
x
=
X
→
y
C
x
↔
y
C
X
8
7
rexbidv
⊢
x
=
X
→
∃
y
∈
N
y
C
x
↔
∃
y
∈
N
y
C
X
9
8
elrab
⊢
X
∈
x
∈
B
|
∃
y
∈
N
y
C
x
↔
X
∈
B
∧
∃
y
∈
N
y
C
X
10
6
9
bitrdi
⊢
K
∈
A
→
X
∈
P
↔
X
∈
B
∧
∃
y
∈
N
y
C
X