Metamath Proof Explorer

Theorem prjspnval2

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

Ref Expression
Hypotheses prjspnval2.e 
|- .~ = { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. S x = ( l .x. y ) ) }
prjspnval2.w 
|- W = ( K freeLMod ( 0 ... N ) )
prjspnval2.b 
|- B = ( ( Base ` W ) \ { ( 0g ` W ) } )
prjspnval2.s 
|- S = ( Base ` K )
prjspnval2.x 
|- .x. = ( .s ` W )
Assertion prjspnval2 
|- ( ( N e. NN0 /\ K e. DivRing ) -> ( N PrjSpn K ) = ( B /. .~ ) )

Proof

Step Hyp Ref Expression
1 prjspnval2.e 
 |-  .~ = { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. S x = ( l .x. y ) ) }
2 prjspnval2.w 
 |-  W = ( K freeLMod ( 0 ... N ) )
3 prjspnval2.b 
 |-  B = ( ( Base ` W ) \ { ( 0g ` W ) } )
4 prjspnval2.s 
 |-  S = ( Base ` K )
5 prjspnval2.x 
 |-  .x. = ( .s ` W )
6 prjspnval 
 |-  ( ( N e. NN0 /\ K e. DivRing ) -> ( N PrjSpn K ) = ( PrjSp ` ( K freeLMod ( 0 ... N ) ) ) )
7 2 fveq2i 
 |-  ( PrjSp ` W ) = ( PrjSp ` ( K freeLMod ( 0 ... N ) ) )
8 ovex 
 |-  ( 0 ... N ) e. _V
9 2 frlmlvec 
 |-  ( ( K e. DivRing /\ ( 0 ... N ) e. _V ) -> W e. LVec )
10 8 9 mpan2 
 |-  ( K e. DivRing -> W e. LVec )
11 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
12 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
13 3 5 11 12 prjspval 
 |-  ( W e. LVec -> ( PrjSp ` W ) = ( B /. { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` ( Scalar ` W ) ) x = ( l .x. y ) ) } ) )
14 10 13 syl 
 |-  ( K e. DivRing -> ( PrjSp ` W ) = ( B /. { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` ( Scalar ` W ) ) x = ( l .x. y ) ) } ) )
15 1 2 3 4 5 prjspnerlem 
 |-  ( K e. DivRing -> .~ = { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` ( Scalar ` W ) ) x = ( l .x. y ) ) } )
16 15 qseq2d 
 |-  ( K e. DivRing -> ( B /. .~ ) = ( B /. { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` ( Scalar ` W ) ) x = ( l .x. y ) ) } ) )
17 14 16 eqtr4d 
 |-  ( K e. DivRing -> ( PrjSp ` W ) = ( B /. .~ ) )
18 7 17 eqtr3id 
 |-  ( K e. DivRing -> ( PrjSp ` ( K freeLMod ( 0 ... N ) ) ) = ( B /. .~ ) )
19 18 adantl 
 |-  ( ( N e. NN0 /\ K e. DivRing ) -> ( PrjSp ` ( K freeLMod ( 0 ... N ) ) ) = ( B /. .~ ) )
20 6 19 eqtrd 
 |-  ( ( N e. NN0 /\ K e. DivRing ) -> ( N PrjSpn K ) = ( B /. .~ ) )