psubclsubN

Description: A closed projective subspace is a projective subspace. (Contributed by NM, 23-Jan-2012) (New usage is discouraged.)

Step	Hyp	Ref	Expression
1		psubclsub.s	$⊢ S = PSubSp (K)$
2		psubclsub.c	$⊢ C = PSubCl (K)$
3		eqid	$⊢ ⊥_{𝑃} (K) = ⊥_{𝑃} (K)$
4	3 2	psubcli2N	$⊢ (K \in HL \land X \in C) \to ⊥_{𝑃} (K) (⊥_{𝑃} (K) (X)) = X$
5		eqid	$⊢ Atoms (K) = Atoms (K)$
6	5 3 2	psubcliN	$⊢ (K \in HL \land X \in C) \to (X \subseteq Atoms (K) \land ⊥_{𝑃} (K) (⊥_{𝑃} (K) (X)) = X)$
7	6	simpld	$⊢ (K \in HL \land X \in C) \to X \subseteq Atoms (K)$
8	5 1 3	polsubN	$⊢ (K \in HL \land X \subseteq Atoms (K)) \to ⊥_{𝑃} (K) (X) \in S$
9	7 8	syldan	$⊢ (K \in HL \land X \in C) \to ⊥_{𝑃} (K) (X) \in S$
10	5 1	psubssat	$⊢ (K \in HL \land ⊥_{𝑃} (K) (X) \in S) \to ⊥_{𝑃} (K) (X) \subseteq Atoms (K)$
11	9 10	syldan	$⊢ (K \in HL \land X \in C) \to ⊥_{𝑃} (K) (X) \subseteq Atoms (K)$
12	5 1 3	polsubN	$⊢ (K \in HL \land ⊥_{𝑃} (K) (X) \subseteq Atoms (K)) \to ⊥_{𝑃} (K) (⊥_{𝑃} (K) (X)) \in S$
13	11 12	syldan	$⊢ (K \in HL \land X \in C) \to ⊥_{𝑃} (K) (⊥_{𝑃} (K) (X)) \in S$
14	4 13	eqeltrrd	$⊢ (K \in HL \land X \in C) \to X \in S$

Metamath Proof Explorer