Metamath Proof Explorer


Theorem prjspnn0

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

Ref Expression
Hypotheses prjspnssbas.p 𝑃 = ( 𝑁 ℙ𝕣𝕠𝕛n 𝐾 )
prjspnssbas.w 𝑊 = ( 𝐾 freeLMod ( 0 ... 𝑁 ) )
prjspnssbas.b 𝐵 = ( ( Base ‘ 𝑊 ) ∖ { ( 0g𝑊 ) } )
prjspnssbas.n ( 𝜑𝑁 ∈ ℕ0 )
prjspnssbas.k ( 𝜑𝐾 ∈ DivRing )
prjspnn0.a ( 𝜑𝐴𝑃 )
Assertion prjspnn0 ( 𝜑𝐴 ≠ ∅ )

Proof

Step Hyp Ref Expression
1 prjspnssbas.p 𝑃 = ( 𝑁 ℙ𝕣𝕠𝕛n 𝐾 )
2 prjspnssbas.w 𝑊 = ( 𝐾 freeLMod ( 0 ... 𝑁 ) )
3 prjspnssbas.b 𝐵 = ( ( Base ‘ 𝑊 ) ∖ { ( 0g𝑊 ) } )
4 prjspnssbas.n ( 𝜑𝑁 ∈ ℕ0 )
5 prjspnssbas.k ( 𝜑𝐾 ∈ DivRing )
6 prjspnn0.a ( 𝜑𝐴𝑃 )
7 eqid { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥𝐵𝑦𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ 𝐾 ) 𝑥 = ( 𝑙 ( ·𝑠𝑊 ) 𝑦 ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥𝐵𝑦𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ 𝐾 ) 𝑥 = ( 𝑙 ( ·𝑠𝑊 ) 𝑦 ) ) }
8 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
9 eqid ( ·𝑠𝑊 ) = ( ·𝑠𝑊 )
10 7 2 3 8 9 5 prjspner ( 𝜑 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥𝐵𝑦𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ 𝐾 ) 𝑥 = ( 𝑙 ( ·𝑠𝑊 ) 𝑦 ) ) } Er 𝐵 )
11 erdm ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥𝐵𝑦𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ 𝐾 ) 𝑥 = ( 𝑙 ( ·𝑠𝑊 ) 𝑦 ) ) } Er 𝐵 → dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥𝐵𝑦𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ 𝐾 ) 𝑥 = ( 𝑙 ( ·𝑠𝑊 ) 𝑦 ) ) } = 𝐵 )
12 10 11 syl ( 𝜑 → dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥𝐵𝑦𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ 𝐾 ) 𝑥 = ( 𝑙 ( ·𝑠𝑊 ) 𝑦 ) ) } = 𝐵 )
13 7 2 3 8 9 prjspnval2 ( ( 𝑁 ∈ ℕ0𝐾 ∈ DivRing ) → ( 𝑁 ℙ𝕣𝕠𝕛n 𝐾 ) = ( 𝐵 / { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥𝐵𝑦𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ 𝐾 ) 𝑥 = ( 𝑙 ( ·𝑠𝑊 ) 𝑦 ) ) } ) )
14 4 5 13 syl2anc ( 𝜑 → ( 𝑁 ℙ𝕣𝕠𝕛n 𝐾 ) = ( 𝐵 / { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥𝐵𝑦𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ 𝐾 ) 𝑥 = ( 𝑙 ( ·𝑠𝑊 ) 𝑦 ) ) } ) )
15 1 14 eqtrid ( 𝜑𝑃 = ( 𝐵 / { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥𝐵𝑦𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ 𝐾 ) 𝑥 = ( 𝑙 ( ·𝑠𝑊 ) 𝑦 ) ) } ) )
16 6 15 eleqtrd ( 𝜑𝐴 ∈ ( 𝐵 / { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥𝐵𝑦𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ 𝐾 ) 𝑥 = ( 𝑙 ( ·𝑠𝑊 ) 𝑦 ) ) } ) )
17 elqsn0 ( ( dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥𝐵𝑦𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ 𝐾 ) 𝑥 = ( 𝑙 ( ·𝑠𝑊 ) 𝑦 ) ) } = 𝐵𝐴 ∈ ( 𝐵 / { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥𝐵𝑦𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ 𝐾 ) 𝑥 = ( 𝑙 ( ·𝑠𝑊 ) 𝑦 ) ) } ) ) → 𝐴 ≠ ∅ )
18 12 16 17 syl2anc ( 𝜑𝐴 ≠ ∅ )