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 
|- .~ = { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. S x = ( l .x. y ) ) }
0prjspnrel.b 
|- B = ( ( Base ` W ) \ { ( 0g ` W ) } )
0prjspnrel.x 
|- .x. = ( .s ` W )
0prjspnrel.s 
|- S = ( Base ` K )
0prjspnrel.w 
|- W = ( K freeLMod ( 0 ... 0 ) )
0prjspnrel.1 
|- .1. = ( ( K unitVec ( 0 ... 0 ) ) ` 0 )
Assertion 0prjspnrel 
|- ( ( K e. DivRing /\ X e. B ) -> X .~ .1. )

Proof

Step Hyp Ref Expression
1 0prjspnrel.e 
 |-  .~ = { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. S x = ( l .x. y ) ) }
2 0prjspnrel.b 
 |-  B = ( ( Base ` W ) \ { ( 0g ` W ) } )
3 0prjspnrel.x 
 |-  .x. = ( .s ` W )
4 0prjspnrel.s 
 |-  S = ( Base ` K )
5 0prjspnrel.w 
 |-  W = ( K freeLMod ( 0 ... 0 ) )
6 0prjspnrel.1 
 |-  .1. = ( ( K unitVec ( 0 ... 0 ) ) ` 0 )
7 simpr 
 |-  ( ( K e. DivRing /\ X e. B ) -> X e. B )
8 2 5 6 0prjspnlem 
 |-  ( K e. DivRing -> .1. e. B )
9 8 adantr 
 |-  ( ( K e. DivRing /\ X e. B ) -> .1. e. B )
10 ovexd 
 |-  ( ( K e. DivRing /\ X e. B ) -> ( 0 ... 0 ) e. _V )
11 difss 
 |-  ( ( Base ` W ) \ { ( 0g ` W ) } ) C_ ( Base ` W )
12 2 11 eqsstri 
 |-  B C_ ( Base ` W )
13 12 sseli 
 |-  ( X e. B -> X e. ( Base ` W ) )
14 13 adantl 
 |-  ( ( K e. DivRing /\ X e. B ) -> X e. ( Base ` W ) )
15 eqid 
 |-  ( Base ` K ) = ( Base ` K )
16 eqid 
 |-  ( Base ` W ) = ( Base ` W )
17 5 15 16 frlmbasf 
 |-  ( ( ( 0 ... 0 ) e. _V /\ X e. ( Base ` W ) ) -> X : ( 0 ... 0 ) --> ( Base ` K ) )
18 10 14 17 syl2anc 
 |-  ( ( K e. DivRing /\ X e. B ) -> X : ( 0 ... 0 ) --> ( Base ` K ) )
19 c0ex 
 |-  0 e. _V
20 19 snid 
 |-  0 e. { 0 }
21 fz0sn 
 |-  ( 0 ... 0 ) = { 0 }
22 20 21 eleqtrri 
 |-  0 e. ( 0 ... 0 )
23 22 a1i 
 |-  ( ( K e. DivRing /\ X e. B ) -> 0 e. ( 0 ... 0 ) )
24 18 23 ffvelrnd 
 |-  ( ( K e. DivRing /\ X e. B ) -> ( X ` 0 ) e. ( Base ` K ) )
25 sneq 
 |-  ( n = ( X ` 0 ) -> { n } = { ( X ` 0 ) } )
26 25 xpeq2d 
 |-  ( n = ( X ` 0 ) -> ( ( 0 ... 0 ) X. { n } ) = ( ( 0 ... 0 ) X. { ( X ` 0 ) } ) )
27 26 eqeq2d 
 |-  ( n = ( X ` 0 ) -> ( X = ( ( 0 ... 0 ) X. { n } ) <-> X = ( ( 0 ... 0 ) X. { ( X ` 0 ) } ) ) )
28 27 adantl 
 |-  ( ( ( K e. DivRing /\ X e. B ) /\ n = ( X ` 0 ) ) -> ( X = ( ( 0 ... 0 ) X. { n } ) <-> X = ( ( 0 ... 0 ) X. { ( X ` 0 ) } ) ) )
29 5 15 16 frlmbasmap 
 |-  ( ( ( 0 ... 0 ) e. _V /\ X e. ( Base ` W ) ) -> X e. ( ( Base ` K ) ^m ( 0 ... 0 ) ) )
30 10 14 29 syl2anc 
 |-  ( ( K e. DivRing /\ X e. B ) -> X e. ( ( Base ` K ) ^m ( 0 ... 0 ) ) )
31 fvex 
 |-  ( Base ` K ) e. _V
32 21 31 19 mapsnconst 
 |-  ( X e. ( ( Base ` K ) ^m ( 0 ... 0 ) ) -> X = ( ( 0 ... 0 ) X. { ( X ` 0 ) } ) )
33 30 32 syl 
 |-  ( ( K e. DivRing /\ X e. B ) -> X = ( ( 0 ... 0 ) X. { ( X ` 0 ) } ) )
34 24 28 33 rspcedvd 
 |-  ( ( K e. DivRing /\ X e. B ) -> E. n e. ( Base ` K ) X = ( ( 0 ... 0 ) X. { n } ) )
35 simprl 
 |-  ( ( ( K e. DivRing /\ X e. B ) /\ ( n e. ( Base ` K ) /\ X = ( ( 0 ... 0 ) X. { n } ) ) ) -> n e. ( Base ` K ) )
36 35 4 eleqtrrdi 
 |-  ( ( ( K e. DivRing /\ X e. B ) /\ ( n e. ( Base ` K ) /\ X = ( ( 0 ... 0 ) X. { n } ) ) ) -> n e. S )
37 oveq1 
 |-  ( m = n -> ( m .x. .1. ) = ( n .x. .1. ) )
38 37 eqeq2d 
 |-  ( m = n -> ( X = ( m .x. .1. ) <-> X = ( n .x. .1. ) ) )
39 38 adantl 
 |-  ( ( ( ( K e. DivRing /\ X e. B ) /\ ( n e. ( Base ` K ) /\ X = ( ( 0 ... 0 ) X. { n } ) ) ) /\ m = n ) -> ( X = ( m .x. .1. ) <-> X = ( n .x. .1. ) ) )
40 ovexd 
 |-  ( ( ( K e. DivRing /\ X e. B ) /\ n e. ( Base ` K ) ) -> ( 0 ... 0 ) e. _V )
41 simpr 
 |-  ( ( ( K e. DivRing /\ X e. B ) /\ n e. ( Base ` K ) ) -> n e. ( Base ` K ) )
42 8 ad2antrr 
 |-  ( ( ( K e. DivRing /\ X e. B ) /\ n e. ( Base ` K ) ) -> .1. e. B )
43 12 42 sseldi 
 |-  ( ( ( K e. DivRing /\ X e. B ) /\ n e. ( Base ` K ) ) -> .1. e. ( Base ` W ) )
44 eqid 
 |-  ( .r ` K ) = ( .r ` K )
45 5 16 15 40 41 43 3 44 frlmvscafval 
 |-  ( ( ( K e. DivRing /\ X e. B ) /\ n e. ( Base ` K ) ) -> ( n .x. .1. ) = ( ( ( 0 ... 0 ) X. { n } ) oF ( .r ` K ) .1. ) )
46 5 15 16 frlmbasf 
 |-  ( ( ( 0 ... 0 ) e. _V /\ .1. e. ( Base ` W ) ) -> .1. : ( 0 ... 0 ) --> ( Base ` K ) )
47 40 43 46 syl2anc 
 |-  ( ( ( K e. DivRing /\ X e. B ) /\ n e. ( Base ` K ) ) -> .1. : ( 0 ... 0 ) --> ( Base ` K ) )
48 drngring 
 |-  ( K e. DivRing -> K e. Ring )
49 eqid 
 |-  ( 1r ` K ) = ( 1r ` K )
50 15 49 ringidcl 
 |-  ( K e. Ring -> ( 1r ` K ) e. ( Base ` K ) )
51 48 50 syl 
 |-  ( K e. DivRing -> ( 1r ` K ) e. ( Base ` K ) )
52 51 ad2antrr 
 |-  ( ( ( K e. DivRing /\ X e. B ) /\ n e. ( Base ` K ) ) -> ( 1r ` K ) e. ( Base ` K ) )
53 52 snssd 
 |-  ( ( ( K e. DivRing /\ X e. B ) /\ n e. ( Base ` K ) ) -> { ( 1r ` K ) } C_ ( Base ` K ) )
54 6 a1i 
 |-  ( d e. ( 0 ... 0 ) -> .1. = ( ( K unitVec ( 0 ... 0 ) ) ` 0 ) )
55 elfz1eq 
 |-  ( d e. ( 0 ... 0 ) -> d = 0 )
56 54 55 fveq12d 
 |-  ( d e. ( 0 ... 0 ) -> ( .1. ` d ) = ( ( ( K unitVec ( 0 ... 0 ) ) ` 0 ) ` 0 ) )
57 56 adantl 
 |-  ( ( ( ( K e. DivRing /\ X e. B ) /\ n e. ( Base ` K ) ) /\ d e. ( 0 ... 0 ) ) -> ( .1. ` d ) = ( ( ( K unitVec ( 0 ... 0 ) ) ` 0 ) ` 0 ) )
58 eqid 
 |-  ( K unitVec ( 0 ... 0 ) ) = ( K unitVec ( 0 ... 0 ) )
59 simplll 
 |-  ( ( ( ( K e. DivRing /\ X e. B ) /\ n e. ( Base ` K ) ) /\ d e. ( 0 ... 0 ) ) -> K e. DivRing )
60 ovexd 
 |-  ( ( ( ( K e. DivRing /\ X e. B ) /\ n e. ( Base ` K ) ) /\ d e. ( 0 ... 0 ) ) -> ( 0 ... 0 ) e. _V )
61 22 a1i 
 |-  ( ( ( ( K e. DivRing /\ X e. B ) /\ n e. ( Base ` K ) ) /\ d e. ( 0 ... 0 ) ) -> 0 e. ( 0 ... 0 ) )
62 58 59 60 61 49 uvcvv1 
 |-  ( ( ( ( K e. DivRing /\ X e. B ) /\ n e. ( Base ` K ) ) /\ d e. ( 0 ... 0 ) ) -> ( ( ( K unitVec ( 0 ... 0 ) ) ` 0 ) ` 0 ) = ( 1r ` K ) )
63 fvex 
 |-  ( ( ( K unitVec ( 0 ... 0 ) ) ` 0 ) ` 0 ) e. _V
64 63 elsn 
 |-  ( ( ( ( K unitVec ( 0 ... 0 ) ) ` 0 ) ` 0 ) e. { ( 1r ` K ) } <-> ( ( ( K unitVec ( 0 ... 0 ) ) ` 0 ) ` 0 ) = ( 1r ` K ) )
65 62 64 sylibr 
 |-  ( ( ( ( K e. DivRing /\ X e. B ) /\ n e. ( Base ` K ) ) /\ d e. ( 0 ... 0 ) ) -> ( ( ( K unitVec ( 0 ... 0 ) ) ` 0 ) ` 0 ) e. { ( 1r ` K ) } )
66 57 65 eqeltrd 
 |-  ( ( ( ( K e. DivRing /\ X e. B ) /\ n e. ( Base ` K ) ) /\ d e. ( 0 ... 0 ) ) -> ( .1. ` d ) e. { ( 1r ` K ) } )
67 66 ralrimiva 
 |-  ( ( ( K e. DivRing /\ X e. B ) /\ n e. ( Base ` K ) ) -> A. d e. ( 0 ... 0 ) ( .1. ` d ) e. { ( 1r ` K ) } )
68 frnssb 
 |-  ( ( { ( 1r ` K ) } C_ ( Base ` K ) /\ A. d e. ( 0 ... 0 ) ( .1. ` d ) e. { ( 1r ` K ) } ) -> ( .1. : ( 0 ... 0 ) --> ( Base ` K ) <-> .1. : ( 0 ... 0 ) --> { ( 1r ` K ) } ) )
69 53 67 68 syl2anc 
 |-  ( ( ( K e. DivRing /\ X e. B ) /\ n e. ( Base ` K ) ) -> ( .1. : ( 0 ... 0 ) --> ( Base ` K ) <-> .1. : ( 0 ... 0 ) --> { ( 1r ` K ) } ) )
70 47 69 mpbid 
 |-  ( ( ( K e. DivRing /\ X e. B ) /\ n e. ( Base ` K ) ) -> .1. : ( 0 ... 0 ) --> { ( 1r ` K ) } )
71 vex 
 |-  n e. _V
72 71 a1i 
 |-  ( ( ( K e. DivRing /\ X e. B ) /\ n e. ( Base ` K ) ) -> n e. _V )
73 elsni 
 |-  ( c e. { ( 1r ` K ) } -> c = ( 1r ` K ) )
74 73 oveq2d 
 |-  ( c e. { ( 1r ` K ) } -> ( n ( .r ` K ) c ) = ( n ( .r ` K ) ( 1r ` K ) ) )
75 48 ad2antrr 
 |-  ( ( ( K e. DivRing /\ X e. B ) /\ n e. ( Base ` K ) ) -> K e. Ring )
76 15 44 49 ringridm 
 |-  ( ( K e. Ring /\ n e. ( Base ` K ) ) -> ( n ( .r ` K ) ( 1r ` K ) ) = n )
77 75 41 76 syl2anc 
 |-  ( ( ( K e. DivRing /\ X e. B ) /\ n e. ( Base ` K ) ) -> ( n ( .r ` K ) ( 1r ` K ) ) = n )
78 74 77 sylan9eqr 
 |-  ( ( ( ( K e. DivRing /\ X e. B ) /\ n e. ( Base ` K ) ) /\ c e. { ( 1r ` K ) } ) -> ( n ( .r ` K ) c ) = n )
79 40 70 72 72 78 caofid2 
 |-  ( ( ( K e. DivRing /\ X e. B ) /\ n e. ( Base ` K ) ) -> ( ( ( 0 ... 0 ) X. { n } ) oF ( .r ` K ) .1. ) = ( ( 0 ... 0 ) X. { n } ) )
80 45 79 eqtrd 
 |-  ( ( ( K e. DivRing /\ X e. B ) /\ n e. ( Base ` K ) ) -> ( n .x. .1. ) = ( ( 0 ... 0 ) X. { n } ) )
81 80 eqeq2d 
 |-  ( ( ( K e. DivRing /\ X e. B ) /\ n e. ( Base ` K ) ) -> ( X = ( n .x. .1. ) <-> X = ( ( 0 ... 0 ) X. { n } ) ) )
82 81 biimprd 
 |-  ( ( ( K e. DivRing /\ X e. B ) /\ n e. ( Base ` K ) ) -> ( X = ( ( 0 ... 0 ) X. { n } ) -> X = ( n .x. .1. ) ) )
83 82 impr 
 |-  ( ( ( K e. DivRing /\ X e. B ) /\ ( n e. ( Base ` K ) /\ X = ( ( 0 ... 0 ) X. { n } ) ) ) -> X = ( n .x. .1. ) )
84 36 39 83 rspcedvd 
 |-  ( ( ( K e. DivRing /\ X e. B ) /\ ( n e. ( Base ` K ) /\ X = ( ( 0 ... 0 ) X. { n } ) ) ) -> E. m e. S X = ( m .x. .1. ) )
85 34 84 rexlimddv 
 |-  ( ( K e. DivRing /\ X e. B ) -> E. m e. S X = ( m .x. .1. ) )
86 1 prjsprel 
 |-  ( X .~ .1. <-> ( ( X e. B /\ .1. e. B ) /\ E. m e. S X = ( m .x. .1. ) ) )
87 7 9 85 86 syl21anbrc 
 |-  ( ( K e. DivRing /\ X e. B ) -> X .~ .1. )