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

Proof

Step Hyp Ref Expression
1 0prjspn.w ⊢ 𝑊 = ( 𝐾 freeLMod ( 0 ... 0 ) )
2 0prjspn.b ⊢ 𝐵 = ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } )
3 eqid ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ 𝐾 ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ 𝐾 ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) }
4 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
5 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
6 0nn0 ⊢ 0 ∈ ℕ0
7 6 a1i ⊢ ( 𝐾 ∈ DivRing → 0 ∈ ℕ0 )
8 id ⊢ ( 𝐾 ∈ DivRing → 𝐾 ∈ DivRing )
9 3 1 2 4 5 7 8 prjspnval2 ⊢ ( 𝐾 ∈ DivRing → ( 0 ℙrojn 𝐾 ) = ( 𝐵 / { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ 𝐾 ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) } ) )
10 ovex ⊢ ( 0 ... 0 ) ∈ V
11 1 frlmsca ⊢ ( ( 𝐾 ∈ DivRing ∧ ( 0 ... 0 ) ∈ V ) → 𝐾 = ( Scalar ‘ 𝑊 ) )
12 10 11 mpan2 ⊢ ( 𝐾 ∈ DivRing → 𝐾 = ( Scalar ‘ 𝑊 ) )
13 12 fveq2d ⊢ ( 𝐾 ∈ DivRing → ( Base ‘ 𝐾 ) = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
14 13 rexeqdv ⊢ ( 𝐾 ∈ DivRing → ( ∃ 𝑙 ∈ ( Base ‘ 𝐾 ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ↔ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) )
15 14 anbi2d ⊢ ( 𝐾 ∈ DivRing → ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ 𝐾 ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) ) )
16 15 opabbidv ⊢ ( 𝐾 ∈ DivRing → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ 𝐾 ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) } )
17 16 qseq2d ⊢ ( 𝐾 ∈ DivRing → ( 𝐵 / { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ 𝐾 ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) } ) = ( 𝐵 / { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) } ) )
18 1 frlmlvec ⊢ ( ( 𝐾 ∈ DivRing ∧ ( 0 ... 0 ) ∈ V ) → 𝑊 ∈ LVec )
19 10 18 mpan2 ⊢ ( 𝐾 ∈ DivRing → 𝑊 ∈ LVec )
20 19 lveclmodd ⊢ ( 𝐾 ∈ DivRing → 𝑊 ∈ LMod )
21 20 adantr ⊢ ( ( 𝐾 ∈ DivRing ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑊 ∈ LMod )
22 16 adantr ⊢ ( ( 𝐾 ∈ DivRing ∧ 𝑎 ∈ 𝐵 ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ 𝐾 ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) } )
23 eqid ⊢ ( ( 𝐾 unitVec ( 0 ... 0 ) ) ‘ 0 ) = ( ( 𝐾 unitVec ( 0 ... 0 ) ) ‘ 0 )
24 3 2 5 4 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 16 adantr ⊢ ( ( 𝐾 ∈ DivRing ∧ 𝑏 ∈ 𝐵 ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ 𝐾 ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) } )
28 3 2 5 4 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 5 32 prjspersym ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑏 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) } ( ( 𝐾 unitVec ( 0 ... 0 ) ) ‘ 0 ) ) → ( ( 𝐾 unitVec ( 0 ... 0 ) ) ‘ 0 ) { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) } 𝑏 )
34 19 29 33 syl2an2r ⊢ ( ( 𝐾 ∈ DivRing ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝐾 unitVec ( 0 ... 0 ) ) ‘ 0 ) { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) } 𝑏 )
35 34 adantrl ⊢ ( ( 𝐾 ∈ DivRing ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝐾 unitVec ( 0 ... 0 ) ) ‘ 0 ) { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) } 𝑏 )
36 30 2 31 5 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 5 32 prjsper ⊢ ( 𝑊 ∈ LVec → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) } Er 𝐵 )
39 19 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 9 17 41 3eqtrd ⊢ ( 𝐾 ∈ DivRing → ( 0 ℙrojn 𝐾 ) = { 𝐵 } )