Metamath Proof Explorer

Theorem prjspnn0

Description: A projective point is nonempty. (Contributed by SN, 17-Jan-2025)

Ref Expression
Hypotheses prjspnssbas.p ⊢P=Nℙ𝕣𝕠𝕛nK
prjspnssbas.w ⊢W=KfreeLMod0…N
prjspnssbas.b ⊢B=BaseW∖0W
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ℙ𝕣𝕠𝕛nK
2 prjspnssbas.w ⊢W=KfreeLMod0…N
3 prjspnssbas.b ⊢B=BaseW∖0W
4 prjspnssbas.n ⊢φ→N∈ℕ0
5 prjspnssbas.k ⊢φ→K∈DivRing
6 prjspnn0.a ⊢φ→A∈P
7 eqid ⊢xy|x∈B∧y∈B∧∃l∈BaseKx=l⋅Wy=xy|x∈B∧y∈B∧∃l∈BaseKx=l⋅Wy
8 eqid ⊢BaseK=BaseK
9 eqid ⊢⋅W=⋅W
10 7 2 3 8 9 5 prjspner ⊢φ→xy|x∈B∧y∈B∧∃l∈BaseKx=l⋅WyErB
11 erdm ⊢xy|x∈B∧y∈B∧∃l∈BaseKx=l⋅WyErB→dom⁡xy|x∈B∧y∈B∧∃l∈BaseKx=l⋅Wy=B
12 10 11 syl ⊢φ→dom⁡xy|x∈B∧y∈B∧∃l∈BaseKx=l⋅Wy=B
13 7 2 3 8 9 prjspnval2 ⊢N∈ℕ0∧K∈DivRing→Nℙ𝕣𝕠𝕛nK=B/xy|x∈B∧y∈B∧∃l∈BaseKx=l⋅Wy
14 4 5 13 syl2anc ⊢φ→Nℙ𝕣𝕠𝕛nK=B/xy|x∈B∧y∈B∧∃l∈BaseKx=l⋅Wy
15 1 14 eqtrid ⊢φ→P=B/xy|x∈B∧y∈B∧∃l∈BaseKx=l⋅Wy
16 6 15 eleqtrd ⊢φ→A∈B/xy|x∈B∧y∈B∧∃l∈BaseKx=l⋅Wy
17 elqsn0 ⊢dom⁡xy|x∈B∧y∈B∧∃l∈BaseKx=l⋅Wy=B∧A∈B/xy|x∈B∧y∈B∧∃l∈BaseKx=l⋅Wy→A≠∅
18 12 16 17 syl2anc ⊢φ→A≠∅