Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Norm Megill
Projective geometries based on Hilbert lattices
elpmap
Next ⟩
pmapssat
Metamath Proof Explorer
Ascii
Unicode
Theorem
elpmap
Description:
Member of a projective map.
(Contributed by
NM
, 27-Jan-2012)
Ref
Expression
Hypotheses
pmapfval.b
⊢
B
=
Base
K
pmapfval.l
⊢
≤
˙
=
≤
K
pmapfval.a
⊢
A
=
Atoms
⁡
K
pmapfval.m
⊢
M
=
pmap
⁡
K
Assertion
elpmap
⊢
K
∈
C
∧
X
∈
B
→
P
∈
M
⁡
X
↔
P
∈
A
∧
P
≤
˙
X
Proof
Step
Hyp
Ref
Expression
1
pmapfval.b
⊢
B
=
Base
K
2
pmapfval.l
⊢
≤
˙
=
≤
K
3
pmapfval.a
⊢
A
=
Atoms
⁡
K
4
pmapfval.m
⊢
M
=
pmap
⁡
K
5
1
2
3
4
pmapval
⊢
K
∈
C
∧
X
∈
B
→
M
⁡
X
=
x
∈
A
|
x
≤
˙
X
6
5
eleq2d
⊢
K
∈
C
∧
X
∈
B
→
P
∈
M
⁡
X
↔
P
∈
x
∈
A
|
x
≤
˙
X
7
breq1
⊢
x
=
P
→
x
≤
˙
X
↔
P
≤
˙
X
8
7
elrab
⊢
P
∈
x
∈
A
|
x
≤
˙
X
↔
P
∈
A
∧
P
≤
˙
X
9
6
8
bitrdi
⊢
K
∈
C
∧
X
∈
B
→
P
∈
M
⁡
X
↔
P
∈
A
∧
P
≤
˙
X