Theorem shsubcl

Description: Closure of vector subtraction in a subspace of a Hilbert space. (Contributed by NM, 18-Oct-1999) (New usage is discouraged.)

	Ref	Expression
Assertion	shsubcl	|- ( ( H e. SH /\ A e. H /\ B e. H ) -> ( A -h B ) e. H )

Proof

Step	Hyp	Ref	Expression
1		shss	|- ( H e. SH -> H C_ ~H )
2	1	sseld	|- ( H e. SH -> ( A e. H -> A e. ~H ) )
3	1	sseld	|- ( H e. SH -> ( B e. H -> B e. ~H ) )
4	2 3	anim12d	|- ( H e. SH -> ( ( A e. H /\ B e. H ) -> ( A e. ~H /\ B e. ~H ) ) )
5	4	3impib	|- ( ( H e. SH /\ A e. H /\ B e. H ) -> ( A e. ~H /\ B e. ~H ) )
6		hvsubval	|- ( ( A e. ~H /\ B e. ~H ) -> ( A -h B ) = ( A +h ( -u 1 .h B ) ) )
7	5 6	syl	|- ( ( H e. SH /\ A e. H /\ B e. H ) -> ( A -h B ) = ( A +h ( -u 1 .h B ) ) )
8		neg1cn	|- -u 1 e. CC
9		shmulcl	|- ( ( H e. SH /\ -u 1 e. CC /\ B e. H ) -> ( -u 1 .h B ) e. H )
10	8 9	mp3an2	|- ( ( H e. SH /\ B e. H ) -> ( -u 1 .h B ) e. H )
11	10	3adant2	|- ( ( H e. SH /\ A e. H /\ B e. H ) -> ( -u 1 .h B ) e. H )
12		shaddcl	|- ( ( H e. SH /\ A e. H /\ ( -u 1 .h B ) e. H ) -> ( A +h ( -u 1 .h B ) ) e. H )
13	11 12	syld3an3	|- ( ( H e. SH /\ A e. H /\ B e. H ) -> ( A +h ( -u 1 .h B ) ) e. H )
14	7 13	eqeltrd	|- ( ( H e. SH /\ A e. H /\ B e. H ) -> ( A -h B ) e. H )