Theorem spanss

Description: Ordering relationship for the spans of subsets of Hilbert space. (Contributed by NM, 2-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	spanss	|- ( ( B C_ ~H /\ A C_ B ) -> ( span ` A ) C_ ( span ` B ) )

Proof

Step	Hyp	Ref	Expression
1		sstr2	|- ( A C_ B -> ( B C_ x -> A C_ x ) )
2	1	adantr	|- ( ( A C_ B /\ x e. SH ) -> ( B C_ x -> A C_ x ) )
3	2	ss2rabdv	|- ( A C_ B -> { x e. SH | B C_ x } C_ { x e. SH | A C_ x } )
4		intss	|- ( { x e. SH | B C_ x } C_ { x e. SH | A C_ x } -> |^| { x e. SH | A C_ x } C_ |^| { x e. SH | B C_ x } )
5	3 4	syl	|- ( A C_ B -> |^| { x e. SH | A C_ x } C_ |^| { x e. SH | B C_ x } )
6	5	adantl	|- ( ( B C_ ~H /\ A C_ B ) -> |^| { x e. SH | A C_ x } C_ |^| { x e. SH | B C_ x } )
7		sstr	|- ( ( A C_ B /\ B C_ ~H ) -> A C_ ~H )
8	7	ancoms	|- ( ( B C_ ~H /\ A C_ B ) -> A C_ ~H )
9		spanval	|- ( A C_ ~H -> ( span ` A ) = |^| { x e. SH | A C_ x } )
10	8 9	syl	|- ( ( B C_ ~H /\ A C_ B ) -> ( span ` A ) = |^| { x e. SH | A C_ x } )
11		spanval	|- ( B C_ ~H -> ( span ` B ) = |^| { x e. SH | B C_ x } )
12	11	adantr	|- ( ( B C_ ~H /\ A C_ B ) -> ( span ` B ) = |^| { x e. SH | B C_ x } )
13	6 10 12	3sstr4d	|- ( ( B C_ ~H /\ A C_ B ) -> ( span ` A ) C_ ( span ` B ) )