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 sseldi ( ( ( 𝐾 ∈ 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 )