Theorem pcl0bN

Description: The projective subspace closure of the empty subspace. (Contributed by NM, 13-Sep-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pcl0b.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	pcl0b.c	$$⊢U=\mathrm{PCl}\left(K\right)$$
Assertion	pcl0bN	$$⊢\left(K\in \mathrm{HL}\wedge P\subseteq A\right)\to \left(U\left(P\right)=\varnothing \leftrightarrow P=\varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		pcl0b.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
2		pcl0b.c	$$⊢U=\mathrm{PCl}\left(K\right)$$
3	1 2	pclssidN	$$⊢\left(K\in \mathrm{HL}\wedge P\subseteq A\right)\to P\subseteq U\left(P\right)$$
4		eqimss	$$⊢U\left(P\right)=\varnothing \to U\left(P\right)\subseteq \varnothing$$
5	3 4	sylan9ss	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\subseteq A\right)\wedge U\left(P\right)=\varnothing \right)\to P\subseteq \varnothing$$
6		ss0	$$⊢P\subseteq \varnothing \to P=\varnothing$$
7	5 6	syl	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\subseteq A\right)\wedge U\left(P\right)=\varnothing \right)\to P=\varnothing$$
8		fveq2	$$⊢P=\varnothing \to U\left(P\right)=U\left(\varnothing \right)$$
9	2	pcl0N	$$⊢K\in \mathrm{HL}\to U\left(\varnothing \right)=\varnothing$$
10	8 9	sylan9eqr	$$⊢\left(K\in \mathrm{HL}\wedge P=\varnothing \right)\to U\left(P\right)=\varnothing$$
11	10	adantlr	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\subseteq A\right)\wedge P=\varnothing \right)\to U\left(P\right)=\varnothing$$
12	7 11	impbida	$$⊢\left(K\in \mathrm{HL}\wedge P\subseteq A\right)\to \left(U\left(P\right)=\varnothing \leftrightarrow P=\varnothing \right)$$