Theorem prjspnval2

Description: Value of the n-dimensional projective space function, expanded. (Contributed by SN, 15-Jul-2023)

	Ref	Expression
Hypotheses	prjspnval2.e	$$⊢\underset{\dot{}}{\sim }=\left\{⟨x,y⟩|\left(\left(x\in B\wedge y\in B\right)\wedge \exists l\in Sx=l\underset{\dot{}}{·}y\right)\right\}$$
	prjspnval2.w	$$⊢W=K\mathrm{freeLMod}\left(0\dots N\right)$$
	prjspnval2.b	$$⊢B={\mathrm{Base}}_W\setminus \left\{0_W\right\}$$
	prjspnval2.s	$$⊢S={\mathrm{Base}}_K$$
	prjspnval2.x	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	prjspnval2.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	prjspnval2.k	$$⊢\phi \to K\in \mathrm{DivRing}$$
Assertion	prjspnval2	$$⊢\phi \to N{\mathrm{\mathbb{P}𝕣𝕠𝕛}}_{n}K=B/\underset{\dot{}}{\sim }$$

Proof

Step	Hyp	Ref	Expression
1		prjspnval2.e	$$⊢\underset{\dot{}}{\sim }=\left\{⟨x,y⟩|\left(\left(x\in B\wedge y\in B\right)\wedge \exists l\in Sx=l\underset{\dot{}}{·}y\right)\right\}$$
2		prjspnval2.w	$$⊢W=K\mathrm{freeLMod}\left(0\dots N\right)$$
3		prjspnval2.b	$$⊢B={\mathrm{Base}}_W\setminus \left\{0_W\right\}$$
4		prjspnval2.s	$$⊢S={\mathrm{Base}}_K$$
5		prjspnval2.x	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
6		prjspnval2.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
7		prjspnval2.k	$$⊢\phi \to K\in \mathrm{DivRing}$$
8		prjspnval	$$⊢\left(N\in {\mathbb{N}}_0\wedge K\in \mathrm{DivRing}\right)\to N{\mathrm{\mathbb{P}𝕣𝕠𝕛}}_{n}K=\mathrm{\mathbb{P}𝕣𝕠𝕛}\left(K\mathrm{freeLMod}\left(0\dots N\right)\right)$$
9	6 7 8	syl2anc	$$⊢\phi \to N{\mathrm{\mathbb{P}𝕣𝕠𝕛}}_{n}K=\mathrm{\mathbb{P}𝕣𝕠𝕛}\left(K\mathrm{freeLMod}\left(0\dots N\right)\right)$$
10	2	fveq2i	$$⊢\mathrm{\mathbb{P}𝕣𝕠𝕛}\left(W\right)=\mathrm{\mathbb{P}𝕣𝕠𝕛}\left(K\mathrm{freeLMod}\left(0\dots N\right)\right)$$
11		ovex	$$⊢\left(0\dots N\right)\in \mathrm{V}$$
12	2	frlmlvec	$$⊢\left(K\in \mathrm{DivRing}\wedge \left(0\dots N\right)\in \mathrm{V}\right)\to W\in \mathrm{LVec}$$
13	11 12	mpan2	$$⊢K\in \mathrm{DivRing}\to W\in \mathrm{LVec}$$
14		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
15		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
16	3 5 14 15	prjspval	$$⊢W\in \mathrm{LVec}\to \mathrm{\mathbb{P}𝕣𝕠𝕛}\left(W\right)=B/\left\{⟨x,y⟩|\left(\left(x\in B\wedge y\in B\right)\wedge \exists l\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}x=l\underset{\dot{}}{·}y\right)\right\}$$
17	13 16	syl	$$⊢K\in \mathrm{DivRing}\to \mathrm{\mathbb{P}𝕣𝕠𝕛}\left(W\right)=B/\left\{⟨x,y⟩|\left(\left(x\in B\wedge y\in B\right)\wedge \exists l\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}x=l\underset{\dot{}}{·}y\right)\right\}$$
18	1 2 3 4 5	prjspnerlem	$$⊢K\in \mathrm{DivRing}\to \underset{\dot{}}{\sim }=\left\{⟨x,y⟩|\left(\left(x\in B\wedge y\in B\right)\wedge \exists l\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}x=l\underset{\dot{}}{·}y\right)\right\}$$
19	18	qseq2d	$$⊢K\in \mathrm{DivRing}\to B/\underset{\dot{}}{\sim }=B/\left\{⟨x,y⟩|\left(\left(x\in B\wedge y\in B\right)\wedge \exists l\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}x=l\underset{\dot{}}{·}y\right)\right\}$$
20	17 19	eqtr4d	$$⊢K\in \mathrm{DivRing}\to \mathrm{\mathbb{P}𝕣𝕠𝕛}\left(W\right)=B/\underset{\dot{}}{\sim }$$
21	7 20	syl	$$⊢\phi \to \mathrm{\mathbb{P}𝕣𝕠𝕛}\left(W\right)=B/\underset{\dot{}}{\sim }$$
22	10 21	eqtr3id	$$⊢\phi \to \mathrm{\mathbb{P}𝕣𝕠𝕛}\left(K\mathrm{freeLMod}\left(0\dots N\right)\right)=B/\underset{\dot{}}{\sim }$$
23	9 22	eqtrd	$$⊢\phi \to N{\mathrm{\mathbb{P}𝕣𝕠𝕛}}_{n}K=B/\underset{\dot{}}{\sim }$$