Theorem prjspnssbas

Description: A projective point spans a subset of the (nonzero) affine points. (Contributed by SN, 17-Jan-2025)

	Ref	Expression
Hypotheses	prjspnssbas.p	|- P = ( N PrjSpn K )
	prjspnssbas.w	|- W = ( K freeLMod ( 0 ... N ) )
	prjspnssbas.b	|- B = ( ( Base ` W ) \ { ( 0g ` W ) } )
	prjspnssbas.n	|- ( ph -> N e. NN0 )
	prjspnssbas.k	|- ( ph -> K e. DivRing )
Assertion	prjspnssbas	|- ( ph -> P C_ ~P B )

Proof

Step	Hyp	Ref	Expression
1		prjspnssbas.p	|- P = ( N PrjSpn K )
2		prjspnssbas.w	|- W = ( K freeLMod ( 0 ... N ) )
3		prjspnssbas.b	|- B = ( ( Base ` W ) \ { ( 0g ` W ) } )
4		prjspnssbas.n	|- ( ph -> N e. NN0 )
5		prjspnssbas.k	|- ( ph -> K e. DivRing )
6		eqid	|- { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` K ) x = ( l ( .s ` W ) y ) ) } = { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` K ) x = ( l ( .s ` W ) y ) ) }
7		eqid	|- ( Base ` K ) = ( Base ` K )
8		eqid	|- ( .s ` W ) = ( .s ` W )
9	6 2 3 7 8	prjspnval2	|- ( ( N e. NN0 /\ K e. DivRing ) -> ( N PrjSpn K ) = ( B /. { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` K ) x = ( l ( .s ` W ) y ) ) } ) )
10	4 5 9	syl2anc	|- ( ph -> ( N PrjSpn K ) = ( B /. { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` K ) x = ( l ( .s ` W ) y ) ) } ) )
11	1 10	eqtrid	|- ( ph -> P = ( B /. { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` K ) x = ( l ( .s ` W ) y ) ) } ) )
12	6 2 3 7 8 5	prjspner	|- ( ph -> { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` K ) x = ( l ( .s ` W ) y ) ) } Er B )
13	12	qsss	|- ( ph -> ( B /. { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` K ) x = ( l ( .s ` W ) y ) ) } ) C_ ~P B )
14	11 13	eqsstrd	|- ( ph -> P C_ ~P B )