Theorem prjspnval

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

	Ref	Expression
Assertion	prjspnval	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ DivRing ) → ( 𝑁 ℙ𝕣𝕠𝕛n 𝐾 ) = ( ℙ𝕣𝕠𝕛 ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		oveq2	⊢ ( 𝑛 = 𝑁 → ( 0 ... 𝑛 ) = ( 0 ... 𝑁 ) )
2	1	oveq2d	⊢ ( 𝑛 = 𝑁 → ( 𝑘 freeLMod ( 0 ... 𝑛 ) ) = ( 𝑘 freeLMod ( 0 ... 𝑁 ) ) )
3	2	fveq2d	⊢ ( 𝑛 = 𝑁 → ( ℙ𝕣𝕠𝕛 ‘ ( 𝑘 freeLMod ( 0 ... 𝑛 ) ) ) = ( ℙ𝕣𝕠𝕛 ‘ ( 𝑘 freeLMod ( 0 ... 𝑁 ) ) ) )
4		fvoveq1	⊢ ( 𝑘 = 𝐾 → ( ℙ𝕣𝕠𝕛 ‘ ( 𝑘 freeLMod ( 0 ... 𝑁 ) ) ) = ( ℙ𝕣𝕠𝕛 ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) )
5		df-prjspn	⊢ ℙ𝕣𝕠𝕛n = ( 𝑛 ∈ ℕ0 , 𝑘 ∈ DivRing ↦ ( ℙ𝕣𝕠𝕛 ‘ ( 𝑘 freeLMod ( 0 ... 𝑛 ) ) ) )
6		fvex	⊢ ( ℙ𝕣𝕠𝕛 ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ∈ V
7	3 4 5 6	ovmpo	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ DivRing ) → ( 𝑁 ℙ𝕣𝕠𝕛n 𝐾 ) = ( ℙ𝕣𝕠𝕛 ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) )