Theorem psubssat

Description: A projective subspace consists of atoms. (Contributed by NM, 4-Nov-2011)

	Ref	Expression
Hypotheses	atpsub.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	atpsub.s	$$⊢S=\mathrm{PSubSp}\left(K\right)$$
Assertion	psubssat	$$⊢\left(K\in B\wedge X\in S\right)\to X\subseteq A$$

Proof

Step	Hyp	Ref	Expression
1		atpsub.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
2		atpsub.s	$$⊢S=\mathrm{PSubSp}\left(K\right)$$
3		eqid	$$⊢{\le }_K={\le }_K$$
4		eqid	$$⊢\mathrm{join}\left(K\right)=\mathrm{join}\left(K\right)$$
5	3 4 1 2	ispsubsp	$$⊢K\in B\to \left(X\in S\leftrightarrow \left(X\subseteq A\wedge \forall p\in X\forall q\in X\forall r\in A\left(r{\le }_K\left(p\mathrm{join}\left(K\right)q\right)\to r\in X\right)\right)\right)$$
6	5	simprbda	$$⊢\left(K\in B\wedge X\in S\right)\to X\subseteq A$$