Theorem 0psubN

Description: The empty set is a projective subspace. Remark below Definition 15.1 of MaedaMaeda p. 61. (Contributed by NM, 13-Oct-2011) (New usage is discouraged.)

	Ref	Expression
Hypothesis	0psub.s	$$⊢S=\mathrm{PSubSp}\left(K\right)$$
Assertion	0psubN	$$⊢K\in V\to \varnothing \in S$$

Proof

Step	Hyp	Ref	Expression
1		0psub.s	$$⊢S=\mathrm{PSubSp}\left(K\right)$$
2		0ss	$$⊢\varnothing \subseteq \mathrm{Atoms}\left(K\right)$$
3		ral0	$$⊢\forall p\in \varnothing \forall q\in \varnothing \forall r\in \mathrm{Atoms}\left(K\right)\left(r{\le }_K\left(p\mathrm{join}\left(K\right)q\right)\to r\in \varnothing \right)$$
4	2 3	pm3.2i	$$⊢\left(\varnothing \subseteq \mathrm{Atoms}\left(K\right)\wedge \forall p\in \varnothing \forall q\in \varnothing \forall r\in \mathrm{Atoms}\left(K\right)\left(r{\le }_K\left(p\mathrm{join}\left(K\right)q\right)\to r\in \varnothing \right)\right)$$
5		eqid	$$⊢{\le }_K={\le }_K$$
6		eqid	$$⊢\mathrm{join}\left(K\right)=\mathrm{join}\left(K\right)$$
7		eqid	$$⊢\mathrm{Atoms}\left(K\right)=\mathrm{Atoms}\left(K\right)$$
8	5 6 7 1	ispsubsp	$$⊢K\in V\to \left(\varnothing \in S\leftrightarrow \left(\varnothing \subseteq \mathrm{Atoms}\left(K\right)\wedge \forall p\in \varnothing \forall q\in \varnothing \forall r\in \mathrm{Atoms}\left(K\right)\left(r{\le }_K\left(p\mathrm{join}\left(K\right)q\right)\to r\in \varnothing \right)\right)\right)$$
9	4 8	mpbiri	$$⊢K\in V\to \varnothing \in S$$