Metamath Proof Explorer

Theorem 0prjspn

Description: A zero-dimensional projective space has only 1 point. (Contributed by SN, 9-Jun-2023)

Ref Expression
Hypotheses 0prjspn.w ⊢ W = K freeLMod 0 … 0
0prjspn.b ⊢ B = Base W ∖ 0 W
Assertion 0prjspn ⊢ K ∈ DivRing → 0 ℙ𝕣𝕠𝕛 n K = B

Proof

Step Hyp Ref Expression
1 0prjspn.w ⊢ W = K freeLMod 0 … 0
2 0prjspn.b ⊢ B = Base W ∖ 0 W
3 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
4 eqid ⊢ Base K = Base K
5 eqid ⊢ ⋅ W = ⋅ W
6 0nn0 ⊢ 0 ∈ ℕ 0
7 6 a1i ⊢ K ∈ DivRing → 0 ∈ ℕ 0
8 id ⊢ K ∈ DivRing → K ∈ DivRing
9 3 1 2 4 5 7 8 prjspnval2 ⊢ K ∈ DivRing → 0 ℙ𝕣𝕠𝕛 n K = B / x y | x ∈ B ∧ y ∈ B ∧ ∃ l ∈ Base K x = l ⋅ W y
10 ovex ⊢ 0 … 0 ∈ V
11 1 frlmsca ⊢ K ∈ DivRing ∧ 0 … 0 ∈ V → K = Scalar ⁡ W
12 10 11 mpan2 ⊢ K ∈ DivRing → K = Scalar ⁡ W
13 12 fveq2d ⊢ K ∈ DivRing → Base K = Base Scalar ⁡ W
14 13 rexeqdv ⊢ K ∈ DivRing → ∃ l ∈ Base K x = l ⋅ W y ↔ ∃ l ∈ Base Scalar ⁡ W x = l ⋅ W y
15 14 anbi2d ⊢ K ∈ DivRing → x ∈ B ∧ y ∈ B ∧ ∃ l ∈ Base K x = l ⋅ W y ↔ x ∈ B ∧ y ∈ B ∧ ∃ l ∈ Base Scalar ⁡ W x = l ⋅ W y
16 15 opabbidv ⊢ K ∈ DivRing → x y | x ∈ B ∧ y ∈ B ∧ ∃ l ∈ Base K x = l ⋅ W y = x y | x ∈ B ∧ y ∈ B ∧ ∃ l ∈ Base Scalar ⁡ W x = l ⋅ W y
17 16 qseq2d ⊢ K ∈ DivRing → B / x y | x ∈ B ∧ y ∈ B ∧ ∃ l ∈ Base K x = l ⋅ W y = B / x y | x ∈ B ∧ y ∈ B ∧ ∃ l ∈ Base Scalar ⁡ W x = l ⋅ W y
18 1 frlmlvec ⊢ K ∈ DivRing ∧ 0 … 0 ∈ V → W ∈ LVec
19 10 18 mpan2 ⊢ K ∈ DivRing → W ∈ LVec
20 19 lveclmodd ⊢ K ∈ DivRing → W ∈ LMod
21 20 adantr ⊢ K ∈ DivRing ∧ a ∈ B ∧ b ∈ B → W ∈ LMod
22 16 adantr ⊢ K ∈ DivRing ∧ a ∈ B → x y | x ∈ B ∧ y ∈ B ∧ ∃ l ∈ Base K x = l ⋅ W y = x y | x ∈ B ∧ y ∈ B ∧ ∃ l ∈ Base Scalar ⁡ W x = l ⋅ W y
23 eqid ⊢ K unitVec 0 … 0 ⁡ 0 = K unitVec 0 … 0 ⁡ 0
24 3 2 5 4 1 23 0prjspnrel ⊢ K ∈ DivRing ∧ a ∈ B → a x y | x ∈ B ∧ y ∈ B ∧ ∃ l ∈ Base K x = l ⋅ W y K unitVec 0 … 0 ⁡ 0
25 22 24 breqdi ⊢ K ∈ DivRing ∧ a ∈ B → a x y | x ∈ B ∧ y ∈ B ∧ ∃ l ∈ Base Scalar ⁡ W x = l ⋅ W y K unitVec 0 … 0 ⁡ 0
26 25 adantrr ⊢ K ∈ DivRing ∧ a ∈ B ∧ b ∈ B → a x y | x ∈ B ∧ y ∈ B ∧ ∃ l ∈ Base Scalar ⁡ W x = l ⋅ W y K unitVec 0 … 0 ⁡ 0
27 16 adantr ⊢ K ∈ DivRing ∧ b ∈ B → x y | x ∈ B ∧ y ∈ B ∧ ∃ l ∈ Base K x = l ⋅ W y = x y | x ∈ B ∧ y ∈ B ∧ ∃ l ∈ Base Scalar ⁡ W x = l ⋅ W y
28 3 2 5 4 1 23 0prjspnrel ⊢ K ∈ DivRing ∧ b ∈ B → b x y | x ∈ B ∧ y ∈ B ∧ ∃ l ∈ Base K x = l ⋅ W y K unitVec 0 … 0 ⁡ 0
29 27 28 breqdi ⊢ K ∈ DivRing ∧ b ∈ B → b x y | x ∈ B ∧ y ∈ B ∧ ∃ l ∈ Base Scalar ⁡ W x = l ⋅ W y K unitVec 0 … 0 ⁡ 0
30 eqid ⊢ x y | x ∈ B ∧ y ∈ B ∧ ∃ l ∈ Base Scalar ⁡ W x = l ⋅ W y = x y | x ∈ B ∧ y ∈ B ∧ ∃ l ∈ Base Scalar ⁡ W x = l ⋅ W y
31 eqid ⊢ Scalar ⁡ W = Scalar ⁡ W
32 eqid ⊢ Base Scalar ⁡ W = Base Scalar ⁡ W
33 30 2 31 5 32 prjspersym ⊢ W ∈ LVec ∧ b x y | x ∈ B ∧ y ∈ B ∧ ∃ l ∈ Base Scalar ⁡ W x = l ⋅ W y K unitVec 0 … 0 ⁡ 0 → K unitVec 0 … 0 ⁡ 0 x y | x ∈ B ∧ y ∈ B ∧ ∃ l ∈ Base Scalar ⁡ W x = l ⋅ W y b
34 19 29 33 syl2an2r ⊢ K ∈ DivRing ∧ b ∈ B → K unitVec 0 … 0 ⁡ 0 x y | x ∈ B ∧ y ∈ B ∧ ∃ l ∈ Base Scalar ⁡ W x = l ⋅ W y b
35 34 adantrl ⊢ K ∈ DivRing ∧ a ∈ B ∧ b ∈ B → K unitVec 0 … 0 ⁡ 0 x y | x ∈ B ∧ y ∈ B ∧ ∃ l ∈ Base Scalar ⁡ W x = l ⋅ W y b
36 30 2 31 5 32 prjspertr ⊢ W ∈ LMod ∧ a x y | x ∈ B ∧ y ∈ B ∧ ∃ l ∈ Base Scalar ⁡ W x = l ⋅ W y K unitVec 0 … 0 ⁡ 0 ∧ K unitVec 0 … 0 ⁡ 0 x y | x ∈ B ∧ y ∈ B ∧ ∃ l ∈ Base Scalar ⁡ W x = l ⋅ W y b → a x y | x ∈ B ∧ y ∈ B ∧ ∃ l ∈ Base Scalar ⁡ W x = l ⋅ W y b
37 21 26 35 36 syl12anc ⊢ K ∈ DivRing ∧ a ∈ B ∧ b ∈ B → a x y | x ∈ B ∧ y ∈ B ∧ ∃ l ∈ Base Scalar ⁡ W x = l ⋅ W y b
38 30 2 31 5 32 prjsper ⊢ W ∈ LVec → x y | x ∈ B ∧ y ∈ B ∧ ∃ l ∈ Base Scalar ⁡ W x = l ⋅ W y Er B
39 19 38 syl ⊢ K ∈ DivRing → x y | x ∈ B ∧ y ∈ B ∧ ∃ l ∈ Base Scalar ⁡ W x = l ⋅ W y Er B
40 2 1 23 0prjspnlem ⊢ K ∈ DivRing → K unitVec 0 … 0 ⁡ 0 ∈ B
41 37 39 40 qsalrel ⊢ K ∈ DivRing → B / x y | x ∈ B ∧ y ∈ B ∧ ∃ l ∈ Base Scalar ⁡ W x = l ⋅ W y = B
42 9 17 41 3eqtrd ⊢ K ∈ DivRing → 0 ℙ𝕣𝕠𝕛 n K = B