Theorem elprjspnss

Description: A point of a projective space is a subset of the corresponding free module (an equivalence class of nonzero vectors of that module). (Contributed by SN, 23-Sep-2026)

	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 )
	elprjspnss.a	|- ( ph -> A e. P )
Assertion	elprjspnss	|- ( ph -> A C_ 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		elprjspnss.a	|- ( ph -> A e. P )
7	1 2 3 4 5	prjspnssbas	|- ( ph -> P C_ ~P B )
8	7 6	sseldd	|- ( ph -> A e. ~P B )
9	8	elpwid	|- ( ph -> A C_ B )