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