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 ⊢ P = N ℙ𝕣𝕠𝕛 n K
prjspnssbas.w ⊢ W = K freeLMod 0 … N
prjspnssbas.b ⊢ B = Base W ∖ 0 W
prjspnssbas.n ⊢ φ → N ∈ ℕ 0
prjspnssbas.k ⊢ φ → K ∈ DivRing
Assertion prjspnssbas ⊢ φ → P ⊆ 𝒫 B

Proof

Step Hyp Ref Expression
1 prjspnssbas.p ⊢ P = N ℙ𝕣𝕠𝕛 n K
2 prjspnssbas.w ⊢ W = K freeLMod 0 … N
3 prjspnssbas.b ⊢ B = Base W ∖ 0 W
4 prjspnssbas.n ⊢ φ → N ∈ ℕ 0
5 prjspnssbas.k ⊢ φ → K ∈ DivRing
6 eqid ⊢ x y | x ∈ B ∧ y ∈ B ∧ ∃ l ∈ Base K x = l ⋅ W y = x y | x ∈ B ∧ y ∈ B ∧ ∃ l ∈ Base K x = l ⋅ W y
7 eqid ⊢ Base K = Base K
8 eqid ⊢ ⋅ W = ⋅ W
9 6 2 3 7 8 prjspnval2 ⊢ N ∈ ℕ 0 ∧ K ∈ DivRing → N ℙ𝕣𝕠𝕛 n K = B / x y | x ∈ B ∧ y ∈ B ∧ ∃ l ∈ Base K x = l ⋅ W y
10 4 5 9 syl2anc ⊢ φ → N ℙ𝕣𝕠𝕛 n K = B / x y | x ∈ B ∧ y ∈ B ∧ ∃ l ∈ Base K x = l ⋅ W y
11 1 10 eqtrid ⊢ φ → P = B / x y | x ∈ B ∧ y ∈ B ∧ ∃ l ∈ Base K x = l ⋅ W y
12 6 2 3 7 8 5 prjspner ⊢ φ → x y | x ∈ B ∧ y ∈ B ∧ ∃ l ∈ Base K x = l ⋅ W y Er B
13 12 qsss ⊢ φ → B / x y | x ∈ B ∧ y ∈ B ∧ ∃ l ∈ Base K x = l ⋅ W y ⊆ 𝒫 B
14 11 13 eqsstrd ⊢ φ → P ⊆ 𝒫 B