Metamath Proof Explorer

Theorem prjspnval

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

Ref Expression
Assertion prjspnval 
|- ( ( N e. NN0 /\ K e. DivRing ) -> ( N PrjSpn K ) = ( PrjSp ` ( K freeLMod ( 0 ... N ) ) ) )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( n = N -> ( 0 ... n ) = ( 0 ... N ) )
2 1 oveq2d 
 |-  ( n = N -> ( k freeLMod ( 0 ... n ) ) = ( k freeLMod ( 0 ... N ) ) )
3 2 fveq2d 
 |-  ( n = N -> ( PrjSp ` ( k freeLMod ( 0 ... n ) ) ) = ( PrjSp ` ( k freeLMod ( 0 ... N ) ) ) )
4 fvoveq1 
 |-  ( k = K -> ( PrjSp ` ( k freeLMod ( 0 ... N ) ) ) = ( PrjSp ` ( K freeLMod ( 0 ... N ) ) ) )
5 df-prjspn 
 |-  PrjSpn = ( n e. NN0 , k e. DivRing |-> ( PrjSp ` ( k freeLMod ( 0 ... n ) ) ) )
6 fvex 
 |-  ( PrjSp ` ( K freeLMod ( 0 ... N ) ) ) e. _V
7 3 4 5 6 ovmpo 
 |-  ( ( N e. NN0 /\ K e. DivRing ) -> ( N PrjSpn K ) = ( PrjSp ` ( K freeLMod ( 0 ... N ) ) ) )