Metamath Proof Explorer

Definition df-lplanes

Description: Define the set of all "lattice planes" (lattice elements which cover a line) in a Hilbert lattice k , in other words all elements of height 3 (or lattice dimension 3 or projective dimension 2). (Contributed by NM, 16-Jun-2012)

Ref Expression
Assertion df-lplanes ${⊢}\mathrm{LPlanes}=\left({k}\in \mathrm{V}⟼\left\{{x}\in {\mathrm{Base}}_{{k}}|\exists {p}\in \mathrm{LLines}\left({k}\right)\phantom{\rule{.4em}{0ex}}{p}{⋖}_{{k}}{x}\right\}\right)$

Detailed syntax breakdown

Step Hyp Ref Expression
0 clpl ${class}\mathrm{LPlanes}$
1 vk ${setvar}{k}$
2 cvv ${class}\mathrm{V}$
3 vx ${setvar}{x}$
4 cbs ${class}\mathrm{Base}$
5 1 cv ${setvar}{k}$
6 5 4 cfv ${class}{\mathrm{Base}}_{{k}}$
7 vp ${setvar}{p}$
8 clln ${class}\mathrm{LLines}$
9 5 8 cfv ${class}\mathrm{LLines}\left({k}\right)$
10 7 cv ${setvar}{p}$
11 ccvr ${class}⋖$
12 5 11 cfv ${class}{⋖}_{{k}}$
13 3 cv ${setvar}{x}$
14 10 13 12 wbr ${wff}{p}{⋖}_{{k}}{x}$
15 14 7 9 wrex ${wff}\exists {p}\in \mathrm{LLines}\left({k}\right)\phantom{\rule{.4em}{0ex}}{p}{⋖}_{{k}}{x}$
16 15 3 6 crab ${class}\left\{{x}\in {\mathrm{Base}}_{{k}}|\exists {p}\in \mathrm{LLines}\left({k}\right)\phantom{\rule{.4em}{0ex}}{p}{⋖}_{{k}}{x}\right\}$
17 1 2 16 cmpt ${class}\left({k}\in \mathrm{V}⟼\left\{{x}\in {\mathrm{Base}}_{{k}}|\exists {p}\in \mathrm{LLines}\left({k}\right)\phantom{\rule{.4em}{0ex}}{p}{⋖}_{{k}}{x}\right\}\right)$
18 0 17 wceq ${wff}\mathrm{LPlanes}=\left({k}\in \mathrm{V}⟼\left\{{x}\in {\mathrm{Base}}_{{k}}|\exists {p}\in \mathrm{LLines}\left({k}\right)\phantom{\rule{.4em}{0ex}}{p}{⋖}_{{k}}{x}\right\}\right)$