Metamath Proof Explorer

Theorem prjspnn0

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

		Ref	Expression
	Hypotheses	prjspnn0.p	⊢ 𝑃 = ( 𝑁 ℙ𝕣𝕠𝕛_n 𝐾 )
		prjspnn0.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ₀ )
		prjspnn0.k	⊢ ( 𝜑 → 𝐾 ∈ DivRing )
		prjspnn0.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
	Assertion	prjspnn0	⊢ ( 𝜑 → 𝐴 ≠ ∅ )

Proof

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