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	ralrimivw	|- ( A C_ B -> A. x e. SH ( B C_ x -> A C_ x ) )
3		ss2rab	|- ( { x e. SH | B C_ x } C_ { x e. SH | A C_ x } <-> A. x e. SH ( B C_ x -> A C_ x ) )
4	2 3	sylibr	|- ( A C_ B -> { x e. SH | B C_ x } C_ { x e. SH | A C_ x } )
5		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 } )
6	4 5	syl	|- ( A C_ B -> |^| { x e. SH | A C_ x } C_ |^| { x e. SH | B C_ x } )
7	6	adantl	|- ( ( B C_ ~H /\ A C_ B ) -> |^| { x e. SH | A C_ x } C_ |^| { x e. SH | B C_ x } )
8		sstr	|- ( ( A C_ B /\ B C_ ~H ) -> A C_ ~H )
9	8	ancoms	|- ( ( B C_ ~H /\ A C_ B ) -> A C_ ~H )
10		spanval	|- ( A C_ ~H -> ( span ` A ) = |^| { x e. SH | A C_ x } )
11	9 10	syl	|- ( ( B C_ ~H /\ A C_ B ) -> ( span ` A ) = |^| { x e. SH | A C_ x } )
12		spanval	|- ( B C_ ~H -> ( span ` B ) = |^| { x e. SH | B C_ x } )
13	12	adantr	|- ( ( B C_ ~H /\ A C_ B ) -> ( span ` B ) = |^| { x e. SH | B C_ x } )
14	7 11 13	3sstr4d	|- ( ( B C_ ~H /\ A C_ B ) -> ( span ` A ) C_ ( span ` B ) )