Metamath Proof Explorer

Theorem prjspnn0

Description: A projective point is nonempty. (Contributed by SN, 17-Jan-2025)

Ref Expression
Hypotheses prjspnssbas.p 
|- P = ( N PrjSpn K )
prjspnssbas.w 
|- W = ( K freeLMod ( 0 ... N ) )
prjspnssbas.b 
|- B = ( ( Base ` W ) \ { ( 0g ` W ) } )
prjspnssbas.n 
|- ( ph -> N e. NN0 )
prjspnssbas.k 
|- ( ph -> K e. DivRing )
prjspnn0.a 
|- ( ph -> A e. P )
Assertion prjspnn0 
|- ( ph -> A =/= (/) )

Proof

Step Hyp Ref Expression
1 prjspnssbas.p 
 |-  P = ( N PrjSpn K )
2 prjspnssbas.w 
 |-  W = ( K freeLMod ( 0 ... N ) )
3 prjspnssbas.b 
 |-  B = ( ( Base ` W ) \ { ( 0g ` W ) } )
4 prjspnssbas.n 
 |-  ( ph -> N e. NN0 )
5 prjspnssbas.k 
 |-  ( ph -> K e. DivRing )
6 prjspnn0.a 
 |-  ( ph -> A e. P )
7 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 ) ) }
8 eqid 
 |-  ( Base ` K ) = ( Base ` K )
9 eqid 
 |-  ( .s ` W ) = ( .s ` W )
10 7 2 3 8 9 5 prjspner 
 |-  ( ph -> { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` K ) x = ( l ( .s ` W ) y ) ) } Er B )
11 erdm 
 |-  ( { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` K ) x = ( l ( .s ` W ) y ) ) } Er B -> dom { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` K ) x = ( l ( .s ` W ) y ) ) } = B )
12 10 11 syl 
 |-  ( ph -> dom { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` K ) x = ( l ( .s ` W ) y ) ) } = B )
13 7 2 3 8 9 prjspnval2 
 |-  ( ( N e. NN0 /\ K e. DivRing ) -> ( N PrjSpn K ) = ( B /. { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` K ) x = ( l ( .s ` W ) y ) ) } ) )
14 4 5 13 syl2anc 
 |-  ( ph -> ( N PrjSpn K ) = ( B /. { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` K ) x = ( l ( .s ` W ) y ) ) } ) )
15 1 14 eqtrid 
 |-  ( ph -> P = ( B /. { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` K ) x = ( l ( .s ` W ) y ) ) } ) )
16 6 15 eleqtrd 
 |-  ( ph -> A e. ( B /. { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` K ) x = ( l ( .s ` W ) y ) ) } ) )
17 elqsn0 
 |-  ( ( dom { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` K ) x = ( l ( .s ` W ) y ) ) } = B /\ A e. ( B /. { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` K ) x = ( l ( .s ` W ) y ) ) } ) ) -> A =/= (/) )
18 12 16 17 syl2anc 
 |-  ( ph -> A =/= (/) )