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 ≠ ∅