Metamath Proof Explorer

Theorem pclbtwnN

Description: A projective subspace sandwiched between a set of atoms and the set's projective subspace closure equals the closure. (Contributed by NM, 8-Sep-2013) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	pclid.s	$⊢ S = PSubSp (K)$
		pclid.c	$⊢ U = PCl (K)$
	Assertion	pclbtwnN	$⊢ ((K \in V \land X \in S) \land (Y \subseteq X \land X \subseteq U (Y))) \to X = U (Y)$

Proof

Step	Hyp	Ref	Expression
1		pclid.s	$⊢ S = PSubSp (K)$
2		pclid.c	$⊢ U = PCl (K)$
3		simprr	$⊢ ((K \in V \land X \in S) \land (Y \subseteq X \land X \subseteq U (Y))) \to X \subseteq U (Y)$
4		simpll	$⊢ ((K \in V \land X \in S) \land (Y \subseteq X \land X \subseteq U (Y))) \to K \in V$
5		simprl	$⊢ ((K \in V \land X \in S) \land (Y \subseteq X \land X \subseteq U (Y))) \to Y \subseteq X$
6		eqid	$⊢ Atoms (K) = Atoms (K)$
7	6 1	psubssat	$⊢ (K \in V \land X \in S) \to X \subseteq Atoms (K)$
8	7	adantr	$⊢ ((K \in V \land X \in S) \land (Y \subseteq X \land X \subseteq U (Y))) \to X \subseteq Atoms (K)$
9	6 2	pclssN	$⊢ (K \in V \land Y \subseteq X \land X \subseteq Atoms (K)) \to U (Y) \subseteq U (X)$
10	4 5 8 9	syl3anc	$⊢ ((K \in V \land X \in S) \land (Y \subseteq X \land X \subseteq U (Y))) \to U (Y) \subseteq U (X)$
11	1 2	pclidN	$⊢ (K \in V \land X \in S) \to U (X) = X$
12	11	adantr	$⊢ ((K \in V \land X \in S) \land (Y \subseteq X \land X \subseteq U (Y))) \to U (X) = X$
13	10 12	sseqtrd	$⊢ ((K \in V \land X \in S) \land (Y \subseteq X \land X \subseteq U (Y))) \to U (Y) \subseteq X$
14	3 13	eqssd	$⊢ ((K \in V \land X \in S) \land (Y \subseteq X \land X \subseteq U (Y))) \to X = U (Y)$