Metamath Proof Explorer


Theorem prjspnn0

Description: A projective point is nonempty. (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
prjspnn0.a φ A P
Assertion prjspnn0 φ A

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 prjspnn0.a φ A P
7 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
8 eqid Base K = Base K
9 eqid W = W
10 7 2 3 8 9 5 prjspner φ x y | x B y B l Base K x = l W y Er B
11 erdm x y | x B y B l Base K x = l W y Er B dom x y | x B y B l Base K x = l W y = B
12 10 11 syl φ dom x y | x B y B l Base K x = l W y = B
13 7 2 3 8 9 prjspnval2 N 0 K DivRing N ℙ𝕣𝕠𝕛 n K = B / x y | x B y B l Base K x = l W y
14 4 5 13 syl2anc φ N ℙ𝕣𝕠𝕛 n K = B / x y | x B y B l Base K x = l W y
15 1 14 eqtrid φ P = B / x y | x B y B l Base K x = l W y
16 6 15 eleqtrd φ A B / x y | x B y B l Base K x = l W y
17 elqsn0 dom x y | x B y B l Base K x = l W y = B A B / x y | x B y B l Base K x = l W y A
18 12 16 17 syl2anc φ A