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 e. V /\ X e. S ) /\ ( Y C_ X /\ X C_ ( U ` Y ) ) ) -> X = ( U ` Y ) )

Proof

Step	Hyp	Ref	Expression
1		pclid.s	|- S = ( PSubSp ` K )
2		pclid.c	|- U = ( PCl ` K )
3		simprr	|- ( ( ( K e. V /\ X e. S ) /\ ( Y C_ X /\ X C_ ( U ` Y ) ) ) -> X C_ ( U ` Y ) )
4		simpll	|- ( ( ( K e. V /\ X e. S ) /\ ( Y C_ X /\ X C_ ( U ` Y ) ) ) -> K e. V )
5		simprl	|- ( ( ( K e. V /\ X e. S ) /\ ( Y C_ X /\ X C_ ( U ` Y ) ) ) -> Y C_ X )
6		eqid	|- ( Atoms ` K ) = ( Atoms ` K )
7	6 1	psubssat	|- ( ( K e. V /\ X e. S ) -> X C_ ( Atoms ` K ) )
8	7	adantr	|- ( ( ( K e. V /\ X e. S ) /\ ( Y C_ X /\ X C_ ( U ` Y ) ) ) -> X C_ ( Atoms ` K ) )
9	6 2	pclssN	|- ( ( K e. V /\ Y C_ X /\ X C_ ( Atoms ` K ) ) -> ( U ` Y ) C_ ( U ` X ) )
10	4 5 8 9	syl3anc	|- ( ( ( K e. V /\ X e. S ) /\ ( Y C_ X /\ X C_ ( U ` Y ) ) ) -> ( U ` Y ) C_ ( U ` X ) )
11	1 2	pclidN	|- ( ( K e. V /\ X e. S ) -> ( U ` X ) = X )
12	11	adantr	|- ( ( ( K e. V /\ X e. S ) /\ ( Y C_ X /\ X C_ ( U ` Y ) ) ) -> ( U ` X ) = X )
13	10 12	sseqtrd	|- ( ( ( K e. V /\ X e. S ) /\ ( Y C_ X /\ X C_ ( U ` Y ) ) ) -> ( U ` Y ) C_ X )
14	3 13	eqssd	|- ( ( ( K e. V /\ X e. S ) /\ ( Y C_ X /\ X C_ ( U ` Y ) ) ) -> X = ( U ` Y ) )