Theorem pol0N

Description: The polarity of the empty projective subspace is the whole space. (Contributed by NM, 29-Oct-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	polssat.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	polssat.p	$$⊢\underset{\dot{}}{\perp }={\perp }_{𝑃}\left(K\right)$$
Assertion	pol0N	$$⊢K\in B\to \underset{\dot{}}{\perp }\left(\varnothing \right)=A$$

Proof

Step	Hyp	Ref	Expression
1		polssat.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
2		polssat.p	$$⊢\underset{\dot{}}{\perp }={\perp }_{𝑃}\left(K\right)$$
3		0ss	$$⊢\varnothing \subseteq A$$
4		eqid	$$⊢\mathrm{oc}\left(K\right)=\mathrm{oc}\left(K\right)$$
5		eqid	$$⊢\mathrm{pmap}\left(K\right)=\mathrm{pmap}\left(K\right)$$
6	4 1 5 2	polvalN	$$⊢\left(K\in B\wedge \varnothing \subseteq A\right)\to \underset{\dot{}}{\perp }\left(\varnothing \right)=A\cap \bigcap _{p\in \varnothing }\mathrm{pmap}\left(K\right)\left(\mathrm{oc}\left(K\right)\left(p\right)\right)$$
7	3 6	mpan2	$$⊢K\in B\to \underset{\dot{}}{\perp }\left(\varnothing \right)=A\cap \bigcap _{p\in \varnothing }\mathrm{pmap}\left(K\right)\left(\mathrm{oc}\left(K\right)\left(p\right)\right)$$
8		0iin	$$⊢\bigcap _{p\in \varnothing }\mathrm{pmap}\left(K\right)\left(\mathrm{oc}\left(K\right)\left(p\right)\right)=\mathrm{V}$$
9	8	ineq2i	$$⊢A\cap \bigcap _{p\in \varnothing }\mathrm{pmap}\left(K\right)\left(\mathrm{oc}\left(K\right)\left(p\right)\right)=A\cap \mathrm{V}$$
10		inv1	$$⊢A\cap \mathrm{V}=A$$
11	9 10	eqtri	$$⊢A\cap \bigcap _{p\in \varnothing }\mathrm{pmap}\left(K\right)\left(\mathrm{oc}\left(K\right)\left(p\right)\right)=A$$
12	7 11	syl6eq	$$⊢K\in B\to \underset{\dot{}}{\perp }\left(\varnothing \right)=A$$