pclidN

Description: The projective subspace closure of a projective subspace is itself. (Contributed by NM, 8-Sep-2013) (New usage is discouraged.)

Step	Hyp	Ref	Expression
1		pclid.s	$⊢ S = PSubSp (K)$
2		pclid.c	$⊢ U = PCl (K)$
3		eqid	$⊢ Atoms (K) = Atoms (K)$
4	3 1	psubssat	$⊢ (K \in V \land X \in S) \to X \subseteq Atoms (K)$
5	3 1 2	pclvalN	$⊢ (K \in V \land X \subseteq Atoms (K)) \to U (X) = ⋂ \{y \in S \| X \subseteq y\}$
6	4 5	syldan	$⊢ (K \in V \land X \in S) \to U (X) = ⋂ \{y \in S \| X \subseteq y\}$
7		intmin	$⊢ X \in S \to ⋂ \{y \in S \| X \subseteq y\} = X$
8	7	adantl	$⊢ (K \in V \land X \in S) \to ⋂ \{y \in S \| X \subseteq y\} = X$
9	6 8	eqtrd	$⊢ (K \in V \land X \in S) \to U (X) = X$

Metamath Proof Explorer