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=KfreeLMod0…0
0prjspn.b ⊢B=BaseW∖0W
Assertion 0prjspn ⊢K∈DivRing→0ℙ𝕣𝕠𝕛nK=B

Proof

Step Hyp Ref Expression
1 0prjspn.w ⊢W=KfreeLMod0…0
2 0prjspn.b ⊢B=BaseW∖0W
3 0nn0 ⊢0∈ℕ0
4 eqid ⊢xy|x∈B∧y∈B∧∃l∈BaseKx=l⋅Wy=xy|x∈B∧y∈B∧∃l∈BaseKx=l⋅Wy
5 eqid ⊢BaseK=BaseK
6 eqid ⊢⋅W=⋅W
7 4 1 2 5 6 prjspnval2 ⊢0∈ℕ0∧K∈DivRing→0ℙ𝕣𝕠𝕛nK=B/xy|x∈B∧y∈B∧∃l∈BaseKx=l⋅Wy
8 3 7 mpan ⊢K∈DivRing→0ℙ𝕣𝕠𝕛nK=B/xy|x∈B∧y∈B∧∃l∈BaseKx=l⋅Wy
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→BaseK=BaseScalar⁡W
13 12 rexeqdv ⊢K∈DivRing→∃l∈BaseKx=l⋅Wy↔∃l∈BaseScalar⁡Wx=l⋅Wy
14 13 anbi2d ⊢K∈DivRing→x∈B∧y∈B∧∃l∈BaseKx=l⋅Wy↔x∈B∧y∈B∧∃l∈BaseScalar⁡Wx=l⋅Wy
15 14 opabbidv ⊢K∈DivRing→xy|x∈B∧y∈B∧∃l∈BaseKx=l⋅Wy=xy|x∈B∧y∈B∧∃l∈BaseScalar⁡Wx=l⋅Wy
16 15 qseq2d ⊢K∈DivRing→B/xy|x∈B∧y∈B∧∃l∈BaseKx=l⋅Wy=B/xy|x∈B∧y∈B∧∃l∈BaseScalar⁡Wx=l⋅Wy
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→xy|x∈B∧y∈B∧∃l∈BaseKx=l⋅Wy=xy|x∈B∧y∈B∧∃l∈BaseScalar⁡Wx=l⋅Wy
23 eqid ⊢KunitVec0…0⁡0=KunitVec0…0⁡0
24 4 2 6 5 1 23 0prjspnrel ⊢K∈DivRing∧a∈B→axy|x∈B∧y∈B∧∃l∈BaseKx=l⋅WyKunitVec0…0⁡0
25 22 24 breqdi ⊢K∈DivRing∧a∈B→axy|x∈B∧y∈B∧∃l∈BaseScalar⁡Wx=l⋅WyKunitVec0…0⁡0
26 25 adantrr ⊢K∈DivRing∧a∈B∧b∈B→axy|x∈B∧y∈B∧∃l∈BaseScalar⁡Wx=l⋅WyKunitVec0…0⁡0
27 15 adantr ⊢K∈DivRing∧b∈B→xy|x∈B∧y∈B∧∃l∈BaseKx=l⋅Wy=xy|x∈B∧y∈B∧∃l∈BaseScalar⁡Wx=l⋅Wy
28 4 2 6 5 1 23 0prjspnrel ⊢K∈DivRing∧b∈B→bxy|x∈B∧y∈B∧∃l∈BaseKx=l⋅WyKunitVec0…0⁡0
29 27 28 breqdi ⊢K∈DivRing∧b∈B→bxy|x∈B∧y∈B∧∃l∈BaseScalar⁡Wx=l⋅WyKunitVec0…0⁡0
30 eqid ⊢xy|x∈B∧y∈B∧∃l∈BaseScalar⁡Wx=l⋅Wy=xy|x∈B∧y∈B∧∃l∈BaseScalar⁡Wx=l⋅Wy
31 eqid ⊢Scalar⁡W=Scalar⁡W
32 eqid ⊢BaseScalar⁡W=BaseScalar⁡W
33 30 2 31 6 32 prjspersym ⊢W∈LVec∧bxy|x∈B∧y∈B∧∃l∈BaseScalar⁡Wx=l⋅WyKunitVec0…0⁡0→KunitVec0…0⁡0xy|x∈B∧y∈B∧∃l∈BaseScalar⁡Wx=l⋅Wyb
34 18 29 33 syl2an2r ⊢K∈DivRing∧b∈B→KunitVec0…0⁡0xy|x∈B∧y∈B∧∃l∈BaseScalar⁡Wx=l⋅Wyb
35 34 adantrl ⊢K∈DivRing∧a∈B∧b∈B→KunitVec0…0⁡0xy|x∈B∧y∈B∧∃l∈BaseScalar⁡Wx=l⋅Wyb
36 30 2 31 6 32 prjspertr ⊢W∈LMod∧axy|x∈B∧y∈B∧∃l∈BaseScalar⁡Wx=l⋅WyKunitVec0…0⁡0∧KunitVec0…0⁡0xy|x∈B∧y∈B∧∃l∈BaseScalar⁡Wx=l⋅Wyb→axy|x∈B∧y∈B∧∃l∈BaseScalar⁡Wx=l⋅Wyb
37 21 26 35 36 syl12anc ⊢K∈DivRing∧a∈B∧b∈B→axy|x∈B∧y∈B∧∃l∈BaseScalar⁡Wx=l⋅Wyb
38 30 2 31 6 32 prjsper ⊢W∈LVec→xy|x∈B∧y∈B∧∃l∈BaseScalar⁡Wx=l⋅WyErB
39 18 38 syl ⊢K∈DivRing→xy|x∈B∧y∈B∧∃l∈BaseScalar⁡Wx=l⋅WyErB
40 2 1 23 0prjspnlem ⊢K∈DivRing→KunitVec0…0⁡0∈B
41 37 39 40 qsalrel ⊢K∈DivRing→B/xy|x∈B∧y∈B∧∃l∈BaseScalar⁡Wx=l⋅Wy=B
42 8 16 41 3eqtrd ⊢K∈DivRing→0ℙ𝕣𝕠𝕛nK=B