Theorem pclss2polN

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

	Ref	Expression
Hypotheses	pclss2pol.a	|- A = ( Atoms ` K )
	pclss2pol.o	|- ._|_ = ( _|_P ` K )
	pclss2pol.c	|- U = ( PCl ` K )
Assertion	pclss2polN	|- ( ( K e. HL /\ X C_ A ) -> ( U ` X ) C_ ( ._|_ ` ( ._|_ ` X ) ) )

Proof

Step	Hyp	Ref	Expression
1		pclss2pol.a	|- A = ( Atoms ` K )
2		pclss2pol.o	|- ._|_ = ( _|_P ` K )
3		pclss2pol.c	|- U = ( PCl ` K )
4		simpl	|- ( ( K e. HL /\ X C_ A ) -> K e. HL )
5	1 2	2polssN	|- ( ( K e. HL /\ X C_ A ) -> X C_ ( ._|_ ` ( ._|_ ` X ) ) )
6	1 2	polssatN	|- ( ( K e. HL /\ X C_ A ) -> ( ._|_ ` X ) C_ A )
7	1 2	polssatN	|- ( ( K e. HL /\ ( ._|_ ` X ) C_ A ) -> ( ._|_ ` ( ._|_ ` X ) ) C_ A )
8	6 7	syldan	|- ( ( K e. HL /\ X C_ A ) -> ( ._|_ ` ( ._|_ ` X ) ) C_ A )
9	1 3	pclssN	|- ( ( K e. HL /\ X C_ ( ._|_ ` ( ._|_ ` X ) ) /\ ( ._|_ ` ( ._|_ ` X ) ) C_ A ) -> ( U ` X ) C_ ( U ` ( ._|_ ` ( ._|_ ` X ) ) ) )
10	4 5 8 9	syl3anc	|- ( ( K e. HL /\ X C_ A ) -> ( U ` X ) C_ ( U ` ( ._|_ ` ( ._|_ ` X ) ) ) )
11		eqid	|- ( PSubSp ` K ) = ( PSubSp ` K )
12	1 11 2	polsubN	|- ( ( K e. HL /\ ( ._|_ ` X ) C_ A ) -> ( ._|_ ` ( ._|_ ` X ) ) e. ( PSubSp ` K ) )
13	6 12	syldan	|- ( ( K e. HL /\ X C_ A ) -> ( ._|_ ` ( ._|_ ` X ) ) e. ( PSubSp ` K ) )
14	11 3	pclidN	|- ( ( K e. HL /\ ( ._|_ ` ( ._|_ ` X ) ) e. ( PSubSp ` K ) ) -> ( U ` ( ._|_ ` ( ._|_ ` X ) ) ) = ( ._|_ ` ( ._|_ ` X ) ) )
15	13 14	syldan	|- ( ( K e. HL /\ X C_ A ) -> ( U ` ( ._|_ ` ( ._|_ ` X ) ) ) = ( ._|_ ` ( ._|_ ` X ) ) )
16	10 15	sseqtrd	|- ( ( K e. HL /\ X C_ A ) -> ( U ` X ) C_ ( ._|_ ` ( ._|_ ` X ) ) )