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	⊢ 𝑃 = ( 𝑁 ℙ𝕣𝕠𝕛n 𝐾 )
	prjspnssbas.w	⊢ 𝑊 = ( 𝐾 freeLMod ( 0 ... 𝑁 ) )
	prjspnssbas.b	⊢ 𝐵 = ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } )
	prjspnssbas.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
	prjspnssbas.k	⊢ ( 𝜑 → 𝐾 ∈ DivRing )
Assertion	prjspnssbas	⊢ ( 𝜑 → 𝑃 ⊆ 𝒫 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		prjspnssbas.p	⊢ 𝑃 = ( 𝑁 ℙ𝕣𝕠𝕛n 𝐾 )
2		prjspnssbas.w	⊢ 𝑊 = ( 𝐾 freeLMod ( 0 ... 𝑁 ) )
3		prjspnssbas.b	⊢ 𝐵 = ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } )
4		prjspnssbas.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
5		prjspnssbas.k	⊢ ( 𝜑 → 𝐾 ∈ DivRing )
6		eqid	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ 𝐾 ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ 𝐾 ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) }
7		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
8		eqid	⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
9	6 2 3 7 8	prjspnval2	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ DivRing ) → ( 𝑁 ℙ𝕣𝕠𝕛n 𝐾 ) = ( 𝐵 / { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ 𝐾 ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) } ) )
10	4 5 9	syl2anc	⊢ ( 𝜑 → ( 𝑁 ℙ𝕣𝕠𝕛n 𝐾 ) = ( 𝐵 / { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ 𝐾 ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) } ) )
11	1 10	eqtrid	⊢ ( 𝜑 → 𝑃 = ( 𝐵 / { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ 𝐾 ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) } ) )
12	6 2 3 7 8 5	prjspner	⊢ ( 𝜑 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ 𝐾 ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) } Er 𝐵 )
13	12	qsss	⊢ ( 𝜑 → ( 𝐵 / { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ 𝐾 ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) } ) ⊆ 𝒫 𝐵 )
14	11 13	eqsstrd	⊢ ( 𝜑 → 𝑃 ⊆ 𝒫 𝐵 )