Metamath Proof Explorer

Theorem 0prjspn

Description: A zero-dimensional projective space has only 1 point. (Contributed by Steven Nguyen, 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 0nn0 ⊢ 0 ∈ ℕ 0
4 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
5 eqid ⊢ Base K = Base K
6 eqid ⊢ ⋅ W = ⋅ W
7 4 1 2 5 6 prjspnval2 ⊢ 0 ∈ ℕ 0 ∧ K ∈ DivRing → 0 ℙ𝕣𝕠𝕛 n K = B / x y | x ∈ B ∧ y ∈ B ∧ ∃ l ∈ Base K x = l ⋅ W y
8 3 7 mpan ⊢ K ∈ DivRing → 0 ℙ𝕣𝕠𝕛 n K = B / x y | x ∈ B ∧ y ∈ B ∧ ∃ l ∈ Base K x = l ⋅ W y
9 ovex ⊢ 0 … 0 ∈ V
10 1 frlmsca ⊢ K ∈ DivRing ∧ 0 … 0 ∈ V → K = Scalar ⁡ W
11 9 10 mpan2 ⊢ K ∈ DivRing → K = Scalar ⁡ W
12 11 fveq2d ⊢ K ∈ DivRing → Base K = Base Scalar ⁡ W
13 12 rexeqdv ⊢ K ∈ DivRing → ∃ l ∈ Base K x = l ⋅ W y ↔ ∃ l ∈ Base Scalar ⁡ W x = l ⋅ W y
14 13 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
15 14 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
16 15 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
17 1 frlmlvec ⊢ K ∈ DivRing ∧ 0 … 0 ∈ V → W ∈ LVec
18 9 17 mpan2 ⊢ K ∈ DivRing → W ∈ LVec
19 lveclmod ⊢ W ∈ LVec → W ∈ LMod
20 18 19 syl ⊢ K ∈ DivRing → W ∈ LMod
21 20 adantr ⊢ K ∈ DivRing ∧ a ∈ B ∧ b ∈ B → W ∈ LMod
22 15 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 4 2 6 5 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 15 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 4 2 6 5 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 6 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 18 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 6 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 6 32 prjsper ⊢ W ∈ LVec → x y | x ∈ B ∧ y ∈ B ∧ ∃ l ∈ Base Scalar ⁡ W x = l ⋅ W y Er B
39 18 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 8 16 41 3eqtrd ⊢ K ∈ DivRing → 0 ℙ𝕣𝕠𝕛 n K = B