Metamath Proof Explorer

Theorem 0prjspn

Description: A zero-dimensional projective space has only 1 point. (Contributed by SN, 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 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 ) ) }
4 eqid 
 |-  ( Base ` K ) = ( Base ` K )
5 eqid 
 |-  ( .s ` W ) = ( .s ` W )
6 0nn0 
 |-  0 e. NN0
7 6 a1i 
 |-  ( K e. DivRing -> 0 e. NN0 )
8 id 
 |-  ( K e. DivRing -> K e. DivRing )
9 3 1 2 4 5 7 8 prjspnval2 
 |-  ( 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 ) ) } ) )
10 ovex 
 |-  ( 0 ... 0 ) e. _V
11 1 frlmsca 
 |-  ( ( K e. DivRing /\ ( 0 ... 0 ) e. _V ) -> K = ( Scalar ` W ) )
12 10 11 mpan2 
 |-  ( K e. DivRing -> K = ( Scalar ` W ) )
13 12 fveq2d 
 |-  ( K e. DivRing -> ( Base ` K ) = ( Base ` ( Scalar ` W ) ) )
14 13 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 ) ) )
15 14 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 ) ) ) )
16 15 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 ) ) } )
17 16 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 ) ) } ) )
18 1 frlmlvec 
 |-  ( ( K e. DivRing /\ ( 0 ... 0 ) e. _V ) -> W e. LVec )
19 10 18 mpan2 
 |-  ( K e. DivRing -> W e. LVec )
20 19 lveclmodd 
 |-  ( K e. DivRing -> W e. LMod )
21 20 adantr 
 |-  ( ( K e. DivRing /\ ( a e. B /\ b e. B ) ) -> W e. LMod )
22 16 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 3 2 5 4 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 16 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 3 2 5 4 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 5 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 19 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 5 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 5 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 19 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 9 17 41 3eqtrd 
 |-  ( K e. DivRing -> ( 0 PrjSpn K ) = { B } )