Metamath Proof Explorer

Theorem prjspnn0

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

		Ref	Expression
	Hypotheses	prjspnn0.p	$⊢ P = N {ℙ𝕣𝕠𝕛}_{n} K$
		prjspnn0.n	$⊢ φ \to N \in ℕ_{0}$
		prjspnn0.k	$⊢ φ \to K \in DivRing$
		prjspnn0.a	$⊢ φ \to A \in P$
	Assertion	prjspnn0	$⊢ φ \to A \neq \emptyset$

Proof

Step	Hyp	Ref	Expression
1		prjspnn0.p	$⊢ P = N {ℙ𝕣𝕠𝕛}_{n} K$
2		prjspnn0.n	$⊢ φ \to N \in ℕ_{0}$
3		prjspnn0.k	$⊢ φ \to K \in DivRing$
4		prjspnn0.a	$⊢ φ \to A \in P$
5		eqid	$⊢ \{⟨x, y⟩ \| ((x \in ({Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\}) \land y \in ({Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\})) \land \exists l \in {Base}_{K} x = l \cdot_{(K freeLMod (0 \dots N))} y)\} = \{⟨x, y⟩ \| ((x \in ({Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\}) \land y \in ({Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\})) \land \exists l \in {Base}_{K} x = l \cdot_{(K freeLMod (0 \dots N))} y)\}$
6		eqid	$⊢ K freeLMod (0 \dots N) = K freeLMod (0 \dots N)$
7		eqid	$⊢ {Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\} = {Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\}$
8		eqid	$⊢ {Base}_{K} = {Base}_{K}$
9		eqid	$⊢ \cdot_{(K freeLMod (0 \dots N))} = \cdot_{(K freeLMod (0 \dots N))}$
10	5 6 7 8 9 3	prjspner	$⊢ φ \to \{⟨x, y⟩ \| ((x \in ({Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\}) \land y \in ({Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\})) \land \exists l \in {Base}_{K} x = l \cdot_{(K freeLMod (0 \dots N))} y)\} Er ({Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\})$
11		erdm	$⊢ \{⟨x, y⟩ \| ((x \in ({Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\}) \land y \in ({Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\})) \land \exists l \in {Base}_{K} x = l \cdot_{(K freeLMod (0 \dots N))} y)\} Er ({Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\}) \to dom \{⟨x, y⟩ \| ((x \in ({Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\}) \land y \in ({Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\})) \land \exists l \in {Base}_{K} x = l \cdot_{(K freeLMod (0 \dots N))} y)\} = {Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\}$
12	10 11	syl	$⊢ φ \to dom \{⟨x, y⟩ \| ((x \in ({Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\}) \land y \in ({Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\})) \land \exists l \in {Base}_{K} x = l \cdot_{(K freeLMod (0 \dots N))} y)\} = {Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\}$
13	5 6 7 8 9 2 3	prjspnval2	$⊢ φ \to N {ℙ𝕣𝕠𝕛}_{n} K = ({Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\}) / \{⟨x, y⟩ \| ((x \in ({Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\}) \land y \in ({Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\})) \land \exists l \in {Base}_{K} x = l \cdot_{(K freeLMod (0 \dots N))} y)\}$
14	1 13	eqtrid	$⊢ φ \to P = ({Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\}) / \{⟨x, y⟩ \| ((x \in ({Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\}) \land y \in ({Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\})) \land \exists l \in {Base}_{K} x = l \cdot_{(K freeLMod (0 \dots N))} y)\}$
15	4 14	eleqtrd	$⊢ φ \to A \in (({Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\}) / \{⟨x, y⟩ \| ((x \in ({Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\}) \land y \in ({Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\})) \land \exists l \in {Base}_{K} x = l \cdot_{(K freeLMod (0 \dots N))} y)\})$
16		elqsn0	$⊢ (dom \{⟨x, y⟩ \| ((x \in ({Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\}) \land y \in ({Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\})) \land \exists l \in {Base}_{K} x = l \cdot_{(K freeLMod (0 \dots N))} y)\} = {Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\} \land A \in (({Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\}) / \{⟨x, y⟩ \| ((x \in ({Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\}) \land y \in ({Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\})) \land \exists l \in {Base}_{K} x = l \cdot_{(K freeLMod (0 \dots N))} y)\})) \to A \neq \emptyset$
17	12 15 16	syl2anc	$⊢ φ \to A \neq \emptyset$