Theorem prjspnssbas

Description: A projective space is a set of subsets of the corresponding free module (a set of equivalence classes of nonzero vectors of that module). (Contributed by SN, 17-Jan-2025)

	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}$$
Assertion	prjspnssbas	$$⊢\phi \to P\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		eqid	$$⊢\left\{⟨x,y⟩|\left(\left(x\in B\wedge y\in B\right)\wedge \exists l\in {\mathrm{Base}}_{K}x=l{\cdot }_{W}y\right)\right\}=\left\{⟨x,y⟩|\left(\left(x\in B\wedge y\in B\right)\wedge \exists l\in {\mathrm{Base}}_{K}x=l{\cdot }_{W}y\right)\right\}$$
7		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
8		eqid	$$⊢{\cdot }_W={\cdot }_W$$
9	6 2 3 7 8 4 5	prjspnval2	$$⊢\phi \to N{\mathrm{\mathbb{P}𝕣𝕠𝕛}}_{n}K=B/\left\{⟨x,y⟩|\left(\left(x\in B\wedge y\in B\right)\wedge \exists l\in {\mathrm{Base}}_{K}x=l{\cdot }_{W}y\right)\right\}$$
10	1 9	eqtrid	$$⊢\phi \to P=B/\left\{⟨x,y⟩|\left(\left(x\in B\wedge y\in B\right)\wedge \exists l\in {\mathrm{Base}}_{K}x=l{\cdot }_{W}y\right)\right\}$$
11	6 2 3 7 8 5	prjspner	$$⊢\phi \to \left\{⟨x,y⟩|\left(\left(x\in B\wedge y\in B\right)\wedge \exists l\in {\mathrm{Base}}_{K}x=l{\cdot }_{W}y\right)\right\}\mathrm{Er}B$$
12	11	qsss	$$⊢\phi \to B/\left\{⟨x,y⟩|\left(\left(x\in B\wedge y\in B\right)\wedge \exists l\in {\mathrm{Base}}_{K}x=l{\cdot }_{W}y\right)\right\}\subseteq 𝒫B$$
13	10 12	eqsstrd	$$⊢\phi \to P\subseteq 𝒫B$$