This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pointpsubN

Description: A point (singleton of an atom) is a projective subspace. Remark below Definition 15.1 of MaedaMaeda p. 61. (Contributed by NM, 13-Oct-2011) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	pointpsub.p	$⊢ P = Points (K)$
		pointpsub.s	$⊢ S = PSubSp (K)$
	Assertion	pointpsubN	$⊢ (K \in AtLat \land X \in P) \to X \in S$

Proof

Step	Hyp	Ref	Expression
1		pointpsub.p	$⊢ P = Points (K)$
2		pointpsub.s	$⊢ S = PSubSp (K)$
3		eqid	$⊢ Atoms (K) = Atoms (K)$
4	3 1	ispointN	$⊢ K \in AtLat \to (X \in P \leftrightarrow \exists q \in Atoms (K) X = \{q\})$
5	3 2	snatpsubN	$⊢ (K \in AtLat \land q \in Atoms (K)) \to \{q\} \in S$
6	5	ex	$⊢ K \in AtLat \to (q \in Atoms (K) \to \{q\} \in S)$
7		eleq1a	$⊢ \{q\} \in S \to (X = \{q\} \to X \in S)$
8	6 7	syl6	$⊢ K \in AtLat \to (q \in Atoms (K) \to (X = \{q\} \to X \in S))$
9	8	rexlimdv	$⊢ K \in AtLat \to (\exists q \in Atoms (K) X = \{q\} \to X \in S)$
10	4 9	sylbid	$⊢ K \in AtLat \to (X \in P \to X \in S)$
11	10	imp	$⊢ (K \in AtLat \land X \in P) \to X \in S$