Metamath Proof Explorer


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 ( 𝜑𝑃 ⊆ 𝒫 𝐵 )