Theorem pmap0

Description: Value of the projective map of a Hilbert lattice at lattice zero. Part of Theorem 15.5.1 of MaedaMaeda p. 62. (Contributed by NM, 17-Oct-2011)

	Ref	Expression
Hypotheses	pmap0.z	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
	pmap0.m	$$⊢M=\mathrm{pmap}\left(K\right)$$
Assertion	pmap0	$$⊢K\in \mathrm{AtLat}\to M\left(\underset{\dot{}}{0}\right)=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		pmap0.z	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
2		pmap0.m	$$⊢M=\mathrm{pmap}\left(K\right)$$
3		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
4	3 1	atl0cl	$$⊢K\in \mathrm{AtLat}\to \underset{\dot{}}{0}\in {\mathrm{Base}}_K$$
5		eqid	$$⊢{\le }_K={\le }_K$$
6		eqid	$$⊢\mathrm{Atoms}\left(K\right)=\mathrm{Atoms}\left(K\right)$$
7	3 5 6 2	pmapval	$$⊢\left(K\in \mathrm{AtLat}\wedge \underset{\dot{}}{0}\in {\mathrm{Base}}_K\right)\to M\left(\underset{\dot{}}{0}\right)=\left\{a\in \mathrm{Atoms}\left(K\right)|a{\le }_K\underset{\dot{}}{0}\right\}$$
8	4 7	mpdan	$$⊢K\in \mathrm{AtLat}\to M\left(\underset{\dot{}}{0}\right)=\left\{a\in \mathrm{Atoms}\left(K\right)|a{\le }_K\underset{\dot{}}{0}\right\}$$
9	5 1 6	atnle0	$$⊢\left(K\in \mathrm{AtLat}\wedge a\in \mathrm{Atoms}\left(K\right)\right)\to \neg a{\le }_K\underset{\dot{}}{0}$$
10	9	nrexdv	$$⊢K\in \mathrm{AtLat}\to \neg \exists a\in \mathrm{Atoms}\left(K\right)a{\le }_K\underset{\dot{}}{0}$$
11		rabn0	$$⊢\left\{a\in \mathrm{Atoms}\left(K\right)|a{\le }_K\underset{\dot{}}{0}\right\}\ne \varnothing \leftrightarrow \exists a\in \mathrm{Atoms}\left(K\right)a{\le }_K\underset{\dot{}}{0}$$
12	10 11	sylnibr	$$⊢K\in \mathrm{AtLat}\to \neg \left\{a\in \mathrm{Atoms}\left(K\right)|a{\le }_K\underset{\dot{}}{0}\right\}\ne \varnothing$$
13		nne	$$⊢\neg \left\{a\in \mathrm{Atoms}\left(K\right)|a{\le }_K\underset{\dot{}}{0}\right\}\ne \varnothing \leftrightarrow \left\{a\in \mathrm{Atoms}\left(K\right)|a{\le }_K\underset{\dot{}}{0}\right\}=\varnothing$$
14	12 13	sylib	$$⊢K\in \mathrm{AtLat}\to \left\{a\in \mathrm{Atoms}\left(K\right)|a{\le }_K\underset{\dot{}}{0}\right\}=\varnothing$$
15	8 14	eqtrd	$$⊢K\in \mathrm{AtLat}\to M\left(\underset{\dot{}}{0}\right)=\varnothing$$