Metamath Proof Explorer

Theorem prjspnn0

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

Ref Expression
Hypotheses prjspnn0.p 
|- P = ( N PrjSpn K )
prjspnn0.n 
|- ( ph -> N e. NN0 )
prjspnn0.k 
|- ( ph -> K e. DivRing )
prjspnn0.a 
|- ( ph -> A e. P )
Assertion prjspnn0 
|- ( ph -> A =/= (/) )

Proof

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