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