Metamath Proof Explorer

Theorem 0prjspnrel

Description: In the zero-dimensional projective space, all vectors are equivalent to the unit vector. (Contributed by Steven Nguyen, 7-Jun-2023)

Ref Expression
Hypotheses 0prjspnrel.e ⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝑆 𝑥 = ( 𝑙 · 𝑦 ) ) }
0prjspnrel.b ⊢ 𝐵 = ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } )
0prjspnrel.x ⊢ · = ( ·𝑠 ‘ 𝑊 )
0prjspnrel.s ⊢ 𝑆 = ( Base ‘ 𝐾 )
0prjspnrel.w ⊢ 𝑊 = ( 𝐾 freeLMod ( 0 ... 0 ) )
0prjspnrel.1 ⊢ 1 = ( ( 𝐾 unitVec ( 0 ... 0 ) ) ‘ 0 )
Assertion 0prjspnrel ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∼ 1 )

Proof

Step Hyp Ref Expression
1 0prjspnrel.e ⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝑆 𝑥 = ( 𝑙 · 𝑦 ) ) }
2 0prjspnrel.b ⊢ 𝐵 = ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } )
3 0prjspnrel.x ⊢ · = ( ·𝑠 ‘ 𝑊 )
4 0prjspnrel.s ⊢ 𝑆 = ( Base ‘ 𝐾 )
5 0prjspnrel.w ⊢ 𝑊 = ( 𝐾 freeLMod ( 0 ... 0 ) )
6 0prjspnrel.1 ⊢ 1 = ( ( 𝐾 unitVec ( 0 ... 0 ) ) ‘ 0 )
7 simpr ⊢ ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
8 2 5 6 0prjspnlem ⊢ ( 𝐾 ∈ DivRing → 1 ∈ 𝐵 )
9 8 adantr ⊢ ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) → 1 ∈ 𝐵 )
10 sneq ⊢ ( 𝑛 = ( 𝑋 ‘ 0 ) → { 𝑛 } = { ( 𝑋 ‘ 0 ) } )
11 10 xpeq2d ⊢ ( 𝑛 = ( 𝑋 ‘ 0 ) → ( ( 0 ... 0 ) × { 𝑛 } ) = ( ( 0 ... 0 ) × { ( 𝑋 ‘ 0 ) } ) )
12 11 eqeq2d ⊢ ( 𝑛 = ( 𝑋 ‘ 0 ) → ( 𝑋 = ( ( 0 ... 0 ) × { 𝑛 } ) ↔ 𝑋 = ( ( 0 ... 0 ) × { ( 𝑋 ‘ 0 ) } ) ) )
13 ovexd ⊢ ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) → ( 0 ... 0 ) ∈ V )
14 difss ⊢ ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } ) ⊆ ( Base ‘ 𝑊 )
15 2 14 eqsstri ⊢ 𝐵 ⊆ ( Base ‘ 𝑊 )
16 15 sseli ⊢ ( 𝑋 ∈ 𝐵 → 𝑋 ∈ ( Base ‘ 𝑊 ) )
17 16 adantl ⊢ ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ ( Base ‘ 𝑊 ) )
18 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
19 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
20 5 18 19 frlmbasf ⊢ ( ( ( 0 ... 0 ) ∈ V ∧ 𝑋 ∈ ( Base ‘ 𝑊 ) ) → 𝑋 : ( 0 ... 0 ) ⟶ ( Base ‘ 𝐾 ) )
21 13 17 20 syl2anc ⊢ ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) → 𝑋 : ( 0 ... 0 ) ⟶ ( Base ‘ 𝐾 ) )
22 c0ex ⊢ 0 ∈ V
23 22 snid ⊢ 0 ∈ { 0 }
24 fz0sn ⊢ ( 0 ... 0 ) = { 0 }
25 23 24 eleqtrri ⊢ 0 ∈ ( 0 ... 0 )
26 25 a1i ⊢ ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) → 0 ∈ ( 0 ... 0 ) )
27 21 26 ffvelcdmd ⊢ ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ‘ 0 ) ∈ ( Base ‘ 𝐾 ) )
28 5 18 19 frlmbasmap ⊢ ( ( ( 0 ... 0 ) ∈ V ∧ 𝑋 ∈ ( Base ‘ 𝑊 ) ) → 𝑋 ∈ ( ( Base ‘ 𝐾 ) ↑m ( 0 ... 0 ) ) )
29 13 17 28 syl2anc ⊢ ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ ( ( Base ‘ 𝐾 ) ↑m ( 0 ... 0 ) ) )
30 fvex ⊢ ( Base ‘ 𝐾 ) ∈ V
31 24 30 22 mapsnconst ⊢ ( 𝑋 ∈ ( ( Base ‘ 𝐾 ) ↑m ( 0 ... 0 ) ) → 𝑋 = ( ( 0 ... 0 ) × { ( 𝑋 ‘ 0 ) } ) )
32 29 31 syl ⊢ ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) → 𝑋 = ( ( 0 ... 0 ) × { ( 𝑋 ‘ 0 ) } ) )
33 12 27 32 rspcedvdw ⊢ ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) → ∃ 𝑛 ∈ ( Base ‘ 𝐾 ) 𝑋 = ( ( 0 ... 0 ) × { 𝑛 } ) )
34 oveq1 ⊢ ( 𝑚 = 𝑛 → ( 𝑚 · 1 ) = ( 𝑛 · 1 ) )
35 34 eqeq2d ⊢ ( 𝑚 = 𝑛 → ( 𝑋 = ( 𝑚 · 1 ) ↔ 𝑋 = ( 𝑛 · 1 ) ) )
36 simprl ⊢ ( ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑛 ∈ ( Base ‘ 𝐾 ) ∧ 𝑋 = ( ( 0 ... 0 ) × { 𝑛 } ) ) ) → 𝑛 ∈ ( Base ‘ 𝐾 ) )
37 36 4 eleqtrrdi ⊢ ( ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑛 ∈ ( Base ‘ 𝐾 ) ∧ 𝑋 = ( ( 0 ... 0 ) × { 𝑛 } ) ) ) → 𝑛 ∈ 𝑆 )
38 ovexd ⊢ ( ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ( Base ‘ 𝐾 ) ) → ( 0 ... 0 ) ∈ V )
39 simpr ⊢ ( ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ( Base ‘ 𝐾 ) ) → 𝑛 ∈ ( Base ‘ 𝐾 ) )
40 8 ad2antrr ⊢ ( ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ( Base ‘ 𝐾 ) ) → 1 ∈ 𝐵 )
41 15 40 sselid ⊢ ( ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ( Base ‘ 𝐾 ) ) → 1 ∈ ( Base ‘ 𝑊 ) )
42 eqid ⊢ ( .r ‘ 𝐾 ) = ( .r ‘ 𝐾 )
43 5 19 18 38 39 41 3 42 frlmvscafval ⊢ ( ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑛 · 1 ) = ( ( ( 0 ... 0 ) × { 𝑛 } ) ∘f ( .r ‘ 𝐾 ) 1 ) )
44 5 18 19 frlmbasf ⊢ ( ( ( 0 ... 0 ) ∈ V ∧ 1 ∈ ( Base ‘ 𝑊 ) ) → 1 : ( 0 ... 0 ) ⟶ ( Base ‘ 𝐾 ) )
45 38 41 44 syl2anc ⊢ ( ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ( Base ‘ 𝐾 ) ) → 1 : ( 0 ... 0 ) ⟶ ( Base ‘ 𝐾 ) )
46 drngring ⊢ ( 𝐾 ∈ DivRing → 𝐾 ∈ Ring )
47 eqid ⊢ ( 1r ‘ 𝐾 ) = ( 1r ‘ 𝐾 )
48 18 47 ringidcl ⊢ ( 𝐾 ∈ Ring → ( 1r ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) )
49 46 48 syl ⊢ ( 𝐾 ∈ DivRing → ( 1r ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) )
50 49 ad2antrr ⊢ ( ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ( Base ‘ 𝐾 ) ) → ( 1r ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) )
51 50 snssd ⊢ ( ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ( Base ‘ 𝐾 ) ) → { ( 1r ‘ 𝐾 ) } ⊆ ( Base ‘ 𝐾 ) )
52 6 a1i ⊢ ( 𝑑 ∈ ( 0 ... 0 ) → 1 = ( ( 𝐾 unitVec ( 0 ... 0 ) ) ‘ 0 ) )
53 elfz1eq ⊢ ( 𝑑 ∈ ( 0 ... 0 ) → 𝑑 = 0 )
54 52 53 fveq12d ⊢ ( 𝑑 ∈ ( 0 ... 0 ) → ( 1 ‘ 𝑑 ) = ( ( ( 𝐾 unitVec ( 0 ... 0 ) ) ‘ 0 ) ‘ 0 ) )
55 54 adantl ⊢ ( ( ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑑 ∈ ( 0 ... 0 ) ) → ( 1 ‘ 𝑑 ) = ( ( ( 𝐾 unitVec ( 0 ... 0 ) ) ‘ 0 ) ‘ 0 ) )
56 eqid ⊢ ( 𝐾 unitVec ( 0 ... 0 ) ) = ( 𝐾 unitVec ( 0 ... 0 ) )
57 simplll ⊢ ( ( ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑑 ∈ ( 0 ... 0 ) ) → 𝐾 ∈ DivRing )
58 ovexd ⊢ ( ( ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑑 ∈ ( 0 ... 0 ) ) → ( 0 ... 0 ) ∈ V )
59 25 a1i ⊢ ( ( ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑑 ∈ ( 0 ... 0 ) ) → 0 ∈ ( 0 ... 0 ) )
60 56 57 58 59 47 uvcvv1 ⊢ ( ( ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑑 ∈ ( 0 ... 0 ) ) → ( ( ( 𝐾 unitVec ( 0 ... 0 ) ) ‘ 0 ) ‘ 0 ) = ( 1r ‘ 𝐾 ) )
61 fvex ⊢ ( ( ( 𝐾 unitVec ( 0 ... 0 ) ) ‘ 0 ) ‘ 0 ) ∈ V
62 61 elsn ⊢ ( ( ( ( 𝐾 unitVec ( 0 ... 0 ) ) ‘ 0 ) ‘ 0 ) ∈ { ( 1r ‘ 𝐾 ) } ↔ ( ( ( 𝐾 unitVec ( 0 ... 0 ) ) ‘ 0 ) ‘ 0 ) = ( 1r ‘ 𝐾 ) )
63 60 62 sylibr ⊢ ( ( ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑑 ∈ ( 0 ... 0 ) ) → ( ( ( 𝐾 unitVec ( 0 ... 0 ) ) ‘ 0 ) ‘ 0 ) ∈ { ( 1r ‘ 𝐾 ) } )
64 55 63 eqeltrd ⊢ ( ( ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑑 ∈ ( 0 ... 0 ) ) → ( 1 ‘ 𝑑 ) ∈ { ( 1r ‘ 𝐾 ) } )
65 64 ralrimiva ⊢ ( ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ( Base ‘ 𝐾 ) ) → ∀ 𝑑 ∈ ( 0 ... 0 ) ( 1 ‘ 𝑑 ) ∈ { ( 1r ‘ 𝐾 ) } )
66 fcdmssb ⊢ ( ( { ( 1r ‘ 𝐾 ) } ⊆ ( Base ‘ 𝐾 ) ∧ ∀ 𝑑 ∈ ( 0 ... 0 ) ( 1 ‘ 𝑑 ) ∈ { ( 1r ‘ 𝐾 ) } ) → ( 1 : ( 0 ... 0 ) ⟶ ( Base ‘ 𝐾 ) ↔ 1 : ( 0 ... 0 ) ⟶ { ( 1r ‘ 𝐾 ) } ) )
67 51 65 66 syl2anc ⊢ ( ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ( Base ‘ 𝐾 ) ) → ( 1 : ( 0 ... 0 ) ⟶ ( Base ‘ 𝐾 ) ↔ 1 : ( 0 ... 0 ) ⟶ { ( 1r ‘ 𝐾 ) } ) )
68 45 67 mpbid ⊢ ( ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ( Base ‘ 𝐾 ) ) → 1 : ( 0 ... 0 ) ⟶ { ( 1r ‘ 𝐾 ) } )
69 vex ⊢ 𝑛 ∈ V
70 69 a1i ⊢ ( ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ( Base ‘ 𝐾 ) ) → 𝑛 ∈ V )
71 elsni ⊢ ( 𝑐 ∈ { ( 1r ‘ 𝐾 ) } → 𝑐 = ( 1r ‘ 𝐾 ) )
72 71 oveq2d ⊢ ( 𝑐 ∈ { ( 1r ‘ 𝐾 ) } → ( 𝑛 ( .r ‘ 𝐾 ) 𝑐 ) = ( 𝑛 ( .r ‘ 𝐾 ) ( 1r ‘ 𝐾 ) ) )
73 46 ad2antrr ⊢ ( ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ( Base ‘ 𝐾 ) ) → 𝐾 ∈ Ring )
74 18 42 47 73 39 ringridmd ⊢ ( ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑛 ( .r ‘ 𝐾 ) ( 1r ‘ 𝐾 ) ) = 𝑛 )
75 72 74 sylan9eqr ⊢ ( ( ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑐 ∈ { ( 1r ‘ 𝐾 ) } ) → ( 𝑛 ( .r ‘ 𝐾 ) 𝑐 ) = 𝑛 )
76 38 68 70 70 75 caofid2 ⊢ ( ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ( Base ‘ 𝐾 ) ) → ( ( ( 0 ... 0 ) × { 𝑛 } ) ∘f ( .r ‘ 𝐾 ) 1 ) = ( ( 0 ... 0 ) × { 𝑛 } ) )
77 43 76 eqtrd ⊢ ( ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑛 · 1 ) = ( ( 0 ... 0 ) × { 𝑛 } ) )
78 77 eqeq2d ⊢ ( ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑋 = ( 𝑛 · 1 ) ↔ 𝑋 = ( ( 0 ... 0 ) × { 𝑛 } ) ) )
79 78 biimprd ⊢ ( ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑋 = ( ( 0 ... 0 ) × { 𝑛 } ) → 𝑋 = ( 𝑛 · 1 ) ) )
80 79 impr ⊢ ( ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑛 ∈ ( Base ‘ 𝐾 ) ∧ 𝑋 = ( ( 0 ... 0 ) × { 𝑛 } ) ) ) → 𝑋 = ( 𝑛 · 1 ) )
81 35 37 80 rspcedvdw ⊢ ( ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑛 ∈ ( Base ‘ 𝐾 ) ∧ 𝑋 = ( ( 0 ... 0 ) × { 𝑛 } ) ) ) → ∃ 𝑚 ∈ 𝑆 𝑋 = ( 𝑚 · 1 ) )
82 33 81 rexlimddv ⊢ ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) → ∃ 𝑚 ∈ 𝑆 𝑋 = ( 𝑚 · 1 ) )
83 1 prjsprel ⊢ ( 𝑋 ∼ 1 ↔ ( ( 𝑋 ∈ 𝐵 ∧ 1 ∈ 𝐵 ) ∧ ∃ 𝑚 ∈ 𝑆 𝑋 = ( 𝑚 · 1 ) ) )
84 7 9 82 83 syl21anbrc ⊢ ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∼ 1 )