This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )