Theorem pjcss

Description: A projection subspace is an (algebraically) closed subspace. (Contributed by Mario Carneiro, 16-Oct-2015)

	Ref	Expression
Hypotheses	pjcss.k	|- K = ( proj ` W )
	pjcss.c	|- C = ( ClSubSp ` W )
Assertion	pjcss	|- ( W e. PreHil -> dom K C_ C )

Proof

Step	Hyp	Ref	Expression
1		pjcss.k	|- K = ( proj ` W )
2		pjcss.c	|- C = ( ClSubSp ` W )
3		eqid	|- ( Base ` W ) = ( Base ` W )
4		eqid	|- ( ocv ` W ) = ( ocv ` W )
5		eqid	|- ( LSSum ` W ) = ( LSSum ` W )
6		simpl	|- ( ( W e. PreHil /\ x e. dom K ) -> W e. PreHil )
7		eqid	|- ( LSubSp ` W ) = ( LSubSp ` W )
8	3 7 4 5 1	pjdm2	|- ( W e. PreHil -> ( x e. dom K <-> ( x e. ( LSubSp ` W ) /\ ( x ( LSSum ` W ) ( ( ocv ` W ) ` x ) ) = ( Base ` W ) ) ) )
9	8	simprbda	|- ( ( W e. PreHil /\ x e. dom K ) -> x e. ( LSubSp ` W ) )
10	3 7	lssss	|- ( x e. ( LSubSp ` W ) -> x C_ ( Base ` W ) )
11	9 10	syl	|- ( ( W e. PreHil /\ x e. dom K ) -> x C_ ( Base ` W ) )
12	3 4	ocvss	|- ( ( ocv ` W ) ` ( ( ocv ` W ) ` x ) ) C_ ( Base ` W )
13	8	simplbda	|- ( ( W e. PreHil /\ x e. dom K ) -> ( x ( LSSum ` W ) ( ( ocv ` W ) ` x ) ) = ( Base ` W ) )
14	12 13	sseqtrrid	|- ( ( W e. PreHil /\ x e. dom K ) -> ( ( ocv ` W ) ` ( ( ocv ` W ) ` x ) ) C_ ( x ( LSSum ` W ) ( ( ocv ` W ) ` x ) ) )
15	2 3 4 5 6 11 14	lsmcss	|- ( ( W e. PreHil /\ x e. dom K ) -> x e. C )
16	15	ex	|- ( W e. PreHil -> ( x e. dom K -> x e. C ) )
17	16	ssrdv	|- ( W e. PreHil -> dom K C_ C )