Theorem pmapidclN

Description: Projective map of the LUB of a closed subspace. (Contributed by NM, 3-Feb-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pmapidcl.u	$$⊢U=\mathrm{lub}\left(K\right)$$
	pmapidcl.m	$$⊢M=\mathrm{pmap}\left(K\right)$$
	pmapidcl.c	$$⊢C=\mathrm{PSubCl}\left(K\right)$$
Assertion	pmapidclN	$$⊢\left(K\in \mathrm{HL}\wedge X\in C\right)\to M\left(U\left(X\right)\right)=X$$

Proof

Step	Hyp	Ref	Expression
1		pmapidcl.u	$$⊢U=\mathrm{lub}\left(K\right)$$
2		pmapidcl.m	$$⊢M=\mathrm{pmap}\left(K\right)$$
3		pmapidcl.c	$$⊢C=\mathrm{PSubCl}\left(K\right)$$
4		eqid	$$⊢\mathrm{Atoms}\left(K\right)=\mathrm{Atoms}\left(K\right)$$
5	4 3	psubclssatN	$$⊢\left(K\in \mathrm{HL}\wedge X\in C\right)\to X\subseteq \mathrm{Atoms}\left(K\right)$$
6		eqid	$$⊢{\perp }_{𝑃}\left(K\right)={\perp }_{𝑃}\left(K\right)$$
7	1 4 2 6	2polvalN	$$⊢\left(K\in \mathrm{HL}\wedge X\subseteq \mathrm{Atoms}\left(K\right)\right)\to {\perp }_{𝑃}\left(K\right)\left({\perp }_{𝑃}\left(K\right)\left(X\right)\right)=M\left(U\left(X\right)\right)$$
8	5 7	syldan	$$⊢\left(K\in \mathrm{HL}\wedge X\in C\right)\to {\perp }_{𝑃}\left(K\right)\left({\perp }_{𝑃}\left(K\right)\left(X\right)\right)=M\left(U\left(X\right)\right)$$
9	6 3	psubcli2N	$$⊢\left(K\in \mathrm{HL}\wedge X\in C\right)\to {\perp }_{𝑃}\left(K\right)\left({\perp }_{𝑃}\left(K\right)\left(X\right)\right)=X$$
10	8 9	eqtr3d	$$⊢\left(K\in \mathrm{HL}\wedge X\in C\right)\to M\left(U\left(X\right)\right)=X$$