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	⊢ ( 𝜑 → 𝐴 ≠ ∅ )