prjspnval2

Description: Value of the n-dimensional projective space function, expanded. (Contributed by SN, 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 )
	prjspnval2.n	\|- ( ph -> N e. NN0 )
	prjspnval2.k	\|- ( ph -> K e. DivRing )
Assertion	prjspnval2	\|- ( ph -> ( 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		prjspnval2.n	\|- ( ph -> N e. NN0 )
7		prjspnval2.k	\|- ( ph -> K e. DivRing )
8		prjspnval	\|- ( ( N e. NN0 /\ K e. DivRing ) -> ( N PrjSpn K ) = ( PrjSp ` ( K freeLMod ( 0 ... N ) ) ) )
9	6 7 8	syl2anc	\|- ( ph -> ( N PrjSpn K ) = ( PrjSp ` ( K freeLMod ( 0 ... N ) ) ) )
10	2	fveq2i	\|- ( PrjSp ` W ) = ( PrjSp ` ( K freeLMod ( 0 ... N ) ) )
11		ovex	\|- ( 0 ... N ) e. _V
12	2	frlmlvec	\|- ( ( K e. DivRing /\ ( 0 ... N ) e. _V ) -> W e. LVec )
13	11 12	mpan2	\|- ( K e. DivRing -> W e. LVec )
14		eqid	\|- ( Scalar ` W ) = ( Scalar ` W )
15		eqid	\|- ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
16	3 5 14 15	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 ) ) } ) )
17	13 16	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 ) ) } ) )
18	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 ) ) } )
19	18	qseq2d	\|- ( K e. DivRing -> ( B /. .~ ) = ( B /. { <. x , y >. \| ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` ( Scalar ` W ) ) x = ( l .x. y ) ) } ) )
20	17 19	eqtr4d	\|- ( K e. DivRing -> ( PrjSp ` W ) = ( B /. .~ ) )
21	7 20	syl	\|- ( ph -> ( PrjSp ` W ) = ( B /. .~ ) )
22	10 21	eqtr3id	\|- ( ph -> ( PrjSp ` ( K freeLMod ( 0 ... N ) ) ) = ( B /. .~ ) )
23	9 22	eqtrd	\|- ( ph -> ( N PrjSpn K ) = ( B /. .~ ) )

Metamath Proof Explorer

Theorem prjspnval2

Proof