Theorem elprjspnss

Description: A point of a projective space is a subset of the corresponding free module (an equivalence class of nonzero vectors of that module). (Contributed by SN, 23-Sep-2026)

	Ref	Expression
Hypotheses	prjspnssbas.p	$$⊢P=N{\mathrm{\mathbb{P}𝕣𝕠𝕛}}_{n}K$$
	prjspnssbas.w	$$⊢W=K\mathrm{freeLMod}\left(0\dots N\right)$$
	prjspnssbas.b	$$⊢B={\mathrm{Base}}_W\setminus \left\{0_W\right\}$$
	prjspnssbas.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	prjspnssbas.k	$$⊢\phi \to K\in \mathrm{DivRing}$$
	elprjspnss.a	$$⊢\phi \to A\in P$$
Assertion	elprjspnss	$$⊢\phi \to A\subseteq B$$

Proof

Step	Hyp	Ref	Expression
1		prjspnssbas.p	$$⊢P=N{\mathrm{\mathbb{P}𝕣𝕠𝕛}}_{n}K$$
2		prjspnssbas.w	$$⊢W=K\mathrm{freeLMod}\left(0\dots N\right)$$
3		prjspnssbas.b	$$⊢B={\mathrm{Base}}_W\setminus \left\{0_W\right\}$$
4		prjspnssbas.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
5		prjspnssbas.k	$$⊢\phi \to K\in \mathrm{DivRing}$$
6		elprjspnss.a	$$⊢\phi \to A\in P$$
7	1 2 3 4 5	prjspnssbas	$$⊢\phi \to P\subseteq 𝒫B$$
8	7 6	sseldd	$$⊢\phi \to A\in 𝒫B$$
9	8	elpwid	$$⊢\phi \to A\subseteq B$$