Theorem prjspnssbas

Description: A projective point spans a subset of the (nonzero) affine points. (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	prjspnval2	$$⊢\left(N\in {\mathbb{N}}_0\wedge K\in \mathrm{DivRing}\right)\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	4 5 9	syl2anc	$$⊢\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\}$$
11	1 10	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\}$$
12	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$$
13	12	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$$
14	11 13	eqsstrd	$$⊢\phi \to P\subseteq 𝒫B$$