Theorem prjspnval

Description: Value of the n-dimensional projective space function. (Contributed by Steven Nguyen, 1-May-2023)

	Ref	Expression
Assertion	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)$$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$$⊢n=N\to \left(0\dots n\right)=\left(0\dots N\right)$$
2	1	oveq2d	$$⊢n=N\to k\mathrm{freeLMod}\left(0\dots n\right)=k\mathrm{freeLMod}\left(0\dots N\right)$$
3	2	fveq2d	$$⊢n=N\to \mathrm{\mathbb{P}𝕣𝕠𝕛}\left(k\mathrm{freeLMod}\left(0\dots n\right)\right)=\mathrm{\mathbb{P}𝕣𝕠𝕛}\left(k\mathrm{freeLMod}\left(0\dots N\right)\right)$$
4		fvoveq1	$$⊢k=K\to \mathrm{\mathbb{P}𝕣𝕠𝕛}\left(k\mathrm{freeLMod}\left(0\dots N\right)\right)=\mathrm{\mathbb{P}𝕣𝕠𝕛}\left(K\mathrm{freeLMod}\left(0\dots N\right)\right)$$
5		df-prjspn	$$⊢{\mathrm{\mathbb{P}𝕣𝕠𝕛}}_n=\left(n\in {\mathbb{N}}_0,k\in \mathrm{DivRing}⟼\mathrm{\mathbb{P}𝕣𝕠𝕛}\left(k\mathrm{freeLMod}\left(0\dots n\right)\right)\right)$$
6		fvex	$$⊢\mathrm{\mathbb{P}𝕣𝕠𝕛}\left(K\mathrm{freeLMod}\left(0\dots N\right)\right)\in \mathrm{V}$$
7	3 4 5 6	ovmpo	$$⊢\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)$$