Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Norm Megill
Projective geometries based on Hilbert lattices
lplni
Next ⟩
islpln3
Metamath Proof Explorer
Ascii
Unicode
Theorem
lplni
Description:
Condition implying a lattice plane.
(Contributed by
NM
, 20-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
lplni
⊢
K
∈
D
∧
Y
∈
B
∧
X
∈
N
∧
X
C
Y
→
Y
∈
P
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
simpl2
⊢
K
∈
D
∧
Y
∈
B
∧
X
∈
N
∧
X
C
Y
→
Y
∈
B
6
breq1
⊢
x
=
X
→
x
C
Y
↔
X
C
Y
7
6
rspcev
⊢
X
∈
N
∧
X
C
Y
→
∃
x
∈
N
x
C
Y
8
7
3ad2antl3
⊢
K
∈
D
∧
Y
∈
B
∧
X
∈
N
∧
X
C
Y
→
∃
x
∈
N
x
C
Y
9
simpl1
⊢
K
∈
D
∧
Y
∈
B
∧
X
∈
N
∧
X
C
Y
→
K
∈
D
10
1
2
3
4
islpln
⊢
K
∈
D
→
Y
∈
P
↔
Y
∈
B
∧
∃
x
∈
N
x
C
Y
11
9
10
syl
⊢
K
∈
D
∧
Y
∈
B
∧
X
∈
N
∧
X
C
Y
→
Y
∈
P
↔
Y
∈
B
∧
∃
x
∈
N
x
C
Y
12
5
8
11
mpbir2and
⊢
K
∈
D
∧
Y
∈
B
∧
X
∈
N
∧
X
C
Y
→
Y
∈
P