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