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 ⊢ 𝑊 = ( 𝐾 freeLMod ( 0 ... 0 ) )
0prjspn.b ⊢ 𝐵 = ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } )
Assertion 0prjspn ( 𝐾 ∈ DivRing → ( 0 ℙ𝕣𝕠𝕛n 𝐾 ) = { 𝐵 } )

Proof

Step Hyp Ref Expression
1 0prjspn.w ⊢ 𝑊 = ( 𝐾 freeLMod ( 0 ... 0 ) )
2 0prjspn.b ⊢ 𝐵 = ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } )
3 0nn0 ⊢ 0 ∈ ℕ0
4 eqid ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ 𝐾 ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ 𝐾 ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) }
5 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
6 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
7 4 1 2 5 6 prjspnval2 ⊢ ( ( 0 ∈ ℕ0 ∧ 𝐾 ∈ DivRing ) → ( 0 ℙ𝕣𝕠𝕛n 𝐾 ) = ( 𝐵 / { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ 𝐾 ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) } ) )
8 3 7 mpan ⊢ ( 𝐾 ∈ DivRing → ( 0 ℙ𝕣𝕠𝕛n 𝐾 ) = ( 𝐵 / { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ 𝐾 ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) } ) )
9 ovex ⊢ ( 0 ... 0 ) ∈ V
10 1 frlmsca ⊢ ( ( 𝐾 ∈ DivRing ∧ ( 0 ... 0 ) ∈ V ) → 𝐾 = ( Scalar ‘ 𝑊 ) )
11 9 10 mpan2 ⊢ ( 𝐾 ∈ DivRing → 𝐾 = ( Scalar ‘ 𝑊 ) )
12 11 fveq2d ⊢ ( 𝐾 ∈ DivRing → ( Base ‘ 𝐾 ) = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
13 12 rexeqdv ⊢ ( 𝐾 ∈ DivRing → ( ∃ 𝑙 ∈ ( Base ‘ 𝐾 ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ↔ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) )
14 13 anbi2d ⊢ ( 𝐾 ∈ DivRing → ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ 𝐾 ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) ) )
15 14 opabbidv ⊢ ( 𝐾 ∈ DivRing → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ 𝐾 ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) } )
16 15 qseq2d ⊢ ( 𝐾 ∈ DivRing → ( 𝐵 / { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ 𝐾 ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) } ) = ( 𝐵 / { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) } ) )
17 1 frlmlvec ⊢ ( ( 𝐾 ∈ DivRing ∧ ( 0 ... 0 ) ∈ V ) → 𝑊 ∈ LVec )
18 9 17 mpan2 ⊢ ( 𝐾 ∈ DivRing → 𝑊 ∈ LVec )
19 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
20 18 19 syl ⊢ ( 𝐾 ∈ DivRing → 𝑊 ∈ LMod )
21 20 adantr ⊢ ( ( 𝐾 ∈ DivRing ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑊 ∈ LMod )
22 15 adantr ⊢ ( ( 𝐾 ∈ DivRing ∧ 𝑎 ∈ 𝐵 ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ 𝐾 ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) } )
23 eqid ⊢ ( ( 𝐾 unitVec ( 0 ... 0 ) ) ‘ 0 ) = ( ( 𝐾 unitVec ( 0 ... 0 ) ) ‘ 0 )
24 4 2 6 5 1 23 0prjspnrel ⊢ ( ( 𝐾 ∈ DivRing ∧ 𝑎 ∈ 𝐵 ) → 𝑎 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ 𝐾 ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) } ( ( 𝐾 unitVec ( 0 ... 0 ) ) ‘ 0 ) )
25 22 24 breqdi ⊢ ( ( 𝐾 ∈ DivRing ∧ 𝑎 ∈ 𝐵 ) → 𝑎 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) } ( ( 𝐾 unitVec ( 0 ... 0 ) ) ‘ 0 ) )
26 25 adantrr ⊢ ( ( 𝐾 ∈ DivRing ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑎 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) } ( ( 𝐾 unitVec ( 0 ... 0 ) ) ‘ 0 ) )
27 15 adantr ⊢ ( ( 𝐾 ∈ DivRing ∧ 𝑏 ∈ 𝐵 ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ 𝐾 ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) } )
28 4 2 6 5 1 23 0prjspnrel ⊢ ( ( 𝐾 ∈ DivRing ∧ 𝑏 ∈ 𝐵 ) → 𝑏 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ 𝐾 ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) } ( ( 𝐾 unitVec ( 0 ... 0 ) ) ‘ 0 ) )
29 27 28 breqdi ⊢ ( ( 𝐾 ∈ DivRing ∧ 𝑏 ∈ 𝐵 ) → 𝑏 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) } ( ( 𝐾 unitVec ( 0 ... 0 ) ) ‘ 0 ) )
30 eqid ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) }
31 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
32 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
33 30 2 31 6 32 prjspersym ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑏 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) } ( ( 𝐾 unitVec ( 0 ... 0 ) ) ‘ 0 ) ) → ( ( 𝐾 unitVec ( 0 ... 0 ) ) ‘ 0 ) { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) } 𝑏 )
34 18 29 33 syl2an2r ⊢ ( ( 𝐾 ∈ DivRing ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝐾 unitVec ( 0 ... 0 ) ) ‘ 0 ) { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) } 𝑏 )
35 34 adantrl ⊢ ( ( 𝐾 ∈ DivRing ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝐾 unitVec ( 0 ... 0 ) ) ‘ 0 ) { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) } 𝑏 )
36 30 2 31 6 32 prjspertr ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑎 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) } ( ( 𝐾 unitVec ( 0 ... 0 ) ) ‘ 0 ) ∧ ( ( 𝐾 unitVec ( 0 ... 0 ) ) ‘ 0 ) { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) } 𝑏 ) ) → 𝑎 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) } 𝑏 )
37 21 26 35 36 syl12anc ⊢ ( ( 𝐾 ∈ DivRing ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑎 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) } 𝑏 )
38 30 2 31 6 32 prjsper ⊢ ( 𝑊 ∈ LVec → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) } Er 𝐵 )
39 18 38 syl ⊢ ( 𝐾 ∈ DivRing → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) } Er 𝐵 )
40 2 1 23 0prjspnlem ⊢ ( 𝐾 ∈ DivRing → ( ( 𝐾 unitVec ( 0 ... 0 ) ) ‘ 0 ) ∈ 𝐵 )
41 37 39 40 qsalrel ⊢ ( 𝐾 ∈ DivRing → ( 𝐵 / { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) } ) = { 𝐵 } )
42 8 16 41 3eqtrd ⊢ ( 𝐾 ∈ DivRing → ( 0 ℙ𝕣𝕠𝕛n 𝐾 ) = { 𝐵 } )