Theorem pmap1N

Description: Value of the projective map of a Hilbert lattice at lattice unity. Part of Theorem 15.5.1 of MaedaMaeda p. 62. (Contributed by NM, 22-Oct-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pmap1.u	$$⊢\underset{\dot{}}{1}=\mathrm{1.}\left(K\right)$$
	pmap1.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	pmap1.m	$$⊢M=\mathrm{pmap}\left(K\right)$$
Assertion	pmap1N	$$⊢K\in \mathrm{OP}\to M\left(\underset{\dot{}}{1}\right)=A$$

Proof

Step	Hyp	Ref	Expression
1		pmap1.u	$$⊢\underset{\dot{}}{1}=\mathrm{1.}\left(K\right)$$
2		pmap1.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
3		pmap1.m	$$⊢M=\mathrm{pmap}\left(K\right)$$
4		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
5	4 1	op1cl	$$⊢K\in \mathrm{OP}\to \underset{\dot{}}{1}\in {\mathrm{Base}}_K$$
6		eqid	$$⊢{\le }_K={\le }_K$$
7	4 6 2 3	pmapval	$$⊢\left(K\in \mathrm{OP}\wedge \underset{\dot{}}{1}\in {\mathrm{Base}}_K\right)\to M\left(\underset{\dot{}}{1}\right)=\left\{p\in A|p{\le }_K\underset{\dot{}}{1}\right\}$$
8	5 7	mpdan	$$⊢K\in \mathrm{OP}\to M\left(\underset{\dot{}}{1}\right)=\left\{p\in A|p{\le }_K\underset{\dot{}}{1}\right\}$$
9	4 2	atbase	$$⊢p\in A\to p\in {\mathrm{Base}}_K$$
10	4 6 1	ople1	$$⊢\left(K\in \mathrm{OP}\wedge p\in {\mathrm{Base}}_K\right)\to p{\le }_K\underset{\dot{}}{1}$$
11	9 10	sylan2	$$⊢\left(K\in \mathrm{OP}\wedge p\in A\right)\to p{\le }_K\underset{\dot{}}{1}$$
12	11	ralrimiva	$$⊢K\in \mathrm{OP}\to \forall p\in Ap{\le }_K\underset{\dot{}}{1}$$
13		rabid2	$$⊢A=\left\{p\in A|p{\le }_K\underset{\dot{}}{1}\right\}\leftrightarrow \forall p\in Ap{\le }_K\underset{\dot{}}{1}$$
14	12 13	sylibr	$$⊢K\in \mathrm{OP}\to A=\left\{p\in A|p{\le }_K\underset{\dot{}}{1}\right\}$$
15	8 14	eqtr4d	$$⊢K\in \mathrm{OP}\to M\left(\underset{\dot{}}{1}\right)=A$$