Metamath Proof Explorer

Theorem 0prjspn

Description: A zero-dimensional projective space has only 1 point. (Contributed by Steven Nguyen, 9-Jun-2023)

Ref Expression
Hypotheses 0prjspn.w 
|- W = ( K freeLMod ( 0 ... 0 ) )
0prjspn.b 
|- B = ( ( Base ` W ) \ { ( 0g ` W ) } )
Assertion 0prjspn 
|- ( K e. DivRing -> ( 0 PrjSpn K ) = { B } )

Proof

Step Hyp Ref Expression
1 0prjspn.w 
 |-  W = ( K freeLMod ( 0 ... 0 ) )
2 0prjspn.b 
 |-  B = ( ( Base ` W ) \ { ( 0g ` W ) } )
3 0nn0 
 |-  0 e. NN0
4 eqid 
 |-  { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` K ) x = ( l ( .s ` W ) y ) ) } = { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` K ) x = ( l ( .s ` W ) y ) ) }
5 eqid 
 |-  ( Base ` K ) = ( Base ` K )
6 eqid 
 |-  ( .s ` W ) = ( .s ` W )
7 4 1 2 5 6 prjspnval2 
 |-  ( ( 0 e. NN0 /\ K e. DivRing ) -> ( 0 PrjSpn K ) = ( B /. { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` K ) x = ( l ( .s ` W ) y ) ) } ) )
8 3 7 mpan 
 |-  ( K e. DivRing -> ( 0 PrjSpn K ) = ( B /. { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` K ) x = ( l ( .s ` W ) y ) ) } ) )
9 ovex 
 |-  ( 0 ... 0 ) e. _V
10 1 frlmsca 
 |-  ( ( K e. DivRing /\ ( 0 ... 0 ) e. _V ) -> K = ( Scalar ` W ) )
11 9 10 mpan2 
 |-  ( K e. DivRing -> K = ( Scalar ` W ) )
12 11 fveq2d 
 |-  ( K e. DivRing -> ( Base ` K ) = ( Base ` ( Scalar ` W ) ) )
13 12 rexeqdv 
 |-  ( K e. DivRing -> ( E. l e. ( Base ` K ) x = ( l ( .s ` W ) y ) <-> E. l e. ( Base ` ( Scalar ` W ) ) x = ( l ( .s ` W ) y ) ) )
14 13 anbi2d 
 |-  ( K e. DivRing -> ( ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` K ) x = ( l ( .s ` W ) y ) ) <-> ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` ( Scalar ` W ) ) x = ( l ( .s ` W ) y ) ) ) )
15 14 opabbidv 
 |-  ( K e. DivRing -> { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` K ) x = ( l ( .s ` W ) y ) ) } = { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` ( Scalar ` W ) ) x = ( l ( .s ` W ) y ) ) } )
16 15 qseq2d 
 |-  ( K e. DivRing -> ( B /. { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` K ) x = ( l ( .s ` W ) y ) ) } ) = ( B /. { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` ( Scalar ` W ) ) x = ( l ( .s ` W ) y ) ) } ) )
17 1 frlmlvec 
 |-  ( ( K e. DivRing /\ ( 0 ... 0 ) e. _V ) -> W e. LVec )
18 9 17 mpan2 
 |-  ( K e. DivRing -> W e. LVec )
19 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
20 18 19 syl 
 |-  ( K e. DivRing -> W e. LMod )
21 20 adantr 
 |-  ( ( K e. DivRing /\ ( a e. B /\ b e. B ) ) -> W e. LMod )
22 15 adantr 
 |-  ( ( K e. DivRing /\ a e. B ) -> { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` K ) x = ( l ( .s ` W ) y ) ) } = { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` ( Scalar ` W ) ) x = ( l ( .s ` W ) y ) ) } )
23 eqid 
 |-  ( ( K unitVec ( 0 ... 0 ) ) ` 0 ) = ( ( K unitVec ( 0 ... 0 ) ) ` 0 )
24 4 2 6 5 1 23 0prjspnrel 
 |-  ( ( K e. DivRing /\ a e. B ) -> a { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` K ) x = ( l ( .s ` W ) y ) ) } ( ( K unitVec ( 0 ... 0 ) ) ` 0 ) )
25 22 24 breqdi 
 |-  ( ( K e. DivRing /\ a e. B ) -> a { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` ( Scalar ` W ) ) x = ( l ( .s ` W ) y ) ) } ( ( K unitVec ( 0 ... 0 ) ) ` 0 ) )
26 25 adantrr 
 |-  ( ( K e. DivRing /\ ( a e. B /\ b e. B ) ) -> a { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` ( Scalar ` W ) ) x = ( l ( .s ` W ) y ) ) } ( ( K unitVec ( 0 ... 0 ) ) ` 0 ) )
27 15 adantr 
 |-  ( ( K e. DivRing /\ b e. B ) -> { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` K ) x = ( l ( .s ` W ) y ) ) } = { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` ( Scalar ` W ) ) x = ( l ( .s ` W ) y ) ) } )
28 4 2 6 5 1 23 0prjspnrel 
 |-  ( ( K e. DivRing /\ b e. B ) -> b { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` K ) x = ( l ( .s ` W ) y ) ) } ( ( K unitVec ( 0 ... 0 ) ) ` 0 ) )
29 27 28 breqdi 
 |-  ( ( K e. DivRing /\ b e. B ) -> b { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` ( Scalar ` W ) ) x = ( l ( .s ` W ) y ) ) } ( ( K unitVec ( 0 ... 0 ) ) ` 0 ) )
30 eqid 
 |-  { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` ( Scalar ` W ) ) x = ( l ( .s ` W ) y ) ) } = { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` ( Scalar ` W ) ) x = ( l ( .s ` W ) y ) ) }
31 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
32 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
33 30 2 31 6 32 prjspersym 
 |-  ( ( W e. LVec /\ b { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` ( Scalar ` W ) ) x = ( l ( .s ` W ) y ) ) } ( ( K unitVec ( 0 ... 0 ) ) ` 0 ) ) -> ( ( K unitVec ( 0 ... 0 ) ) ` 0 ) { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` ( Scalar ` W ) ) x = ( l ( .s ` W ) y ) ) } b )
34 18 29 33 syl2an2r 
 |-  ( ( K e. DivRing /\ b e. B ) -> ( ( K unitVec ( 0 ... 0 ) ) ` 0 ) { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` ( Scalar ` W ) ) x = ( l ( .s ` W ) y ) ) } b )
35 34 adantrl 
 |-  ( ( K e. DivRing /\ ( a e. B /\ b e. B ) ) -> ( ( K unitVec ( 0 ... 0 ) ) ` 0 ) { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` ( Scalar ` W ) ) x = ( l ( .s ` W ) y ) ) } b )
36 30 2 31 6 32 prjspertr 
 |-  ( ( W e. LMod /\ ( a { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` ( Scalar ` W ) ) x = ( l ( .s ` W ) y ) ) } ( ( K unitVec ( 0 ... 0 ) ) ` 0 ) /\ ( ( K unitVec ( 0 ... 0 ) ) ` 0 ) { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` ( Scalar ` W ) ) x = ( l ( .s ` W ) y ) ) } b ) ) -> a { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` ( Scalar ` W ) ) x = ( l ( .s ` W ) y ) ) } b )
37 21 26 35 36 syl12anc 
 |-  ( ( K e. DivRing /\ ( a e. B /\ b e. B ) ) -> a { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` ( Scalar ` W ) ) x = ( l ( .s ` W ) y ) ) } b )
38 30 2 31 6 32 prjsper 
 |-  ( W e. LVec -> { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` ( Scalar ` W ) ) x = ( l ( .s ` W ) y ) ) } Er B )
39 18 38 syl 
 |-  ( K e. DivRing -> { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` ( Scalar ` W ) ) x = ( l ( .s ` W ) y ) ) } Er B )
40 2 1 23 0prjspnlem 
 |-  ( K e. DivRing -> ( ( K unitVec ( 0 ... 0 ) ) ` 0 ) e. B )
41 37 39 40 qsalrel 
 |-  ( K e. DivRing -> ( B /. { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` ( Scalar ` W ) ) x = ( l ( .s ` W ) y ) ) } ) = { B } )
42 8 16 41 3eqtrd 
 |-  ( K e. DivRing -> ( 0 PrjSpn K ) = { B } )