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	⊢ ( ( 𝐵 ⊆ ℋ ∧ 𝐴 ⊆ 𝐵 ) → ( span ‘ 𝐴 ) ⊆ ( span ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		sstr2	⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐵 ⊆ 𝑥 → 𝐴 ⊆ 𝑥 ) )
2	1	adantr	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ Sℋ ) → ( 𝐵 ⊆ 𝑥 → 𝐴 ⊆ 𝑥 ) )
3	2	ss2rabdv	⊢ ( 𝐴 ⊆ 𝐵 → { 𝑥 ∈ Sℋ ∣ 𝐵 ⊆ 𝑥 } ⊆ { 𝑥 ∈ Sℋ ∣ 𝐴 ⊆ 𝑥 } )
4		intss	⊢ ( { 𝑥 ∈ Sℋ ∣ 𝐵 ⊆ 𝑥 } ⊆ { 𝑥 ∈ Sℋ ∣ 𝐴 ⊆ 𝑥 } → ∩ { 𝑥 ∈ Sℋ ∣ 𝐴 ⊆ 𝑥 } ⊆ ∩ { 𝑥 ∈ Sℋ ∣ 𝐵 ⊆ 𝑥 } )
5	3 4	syl	⊢ ( 𝐴 ⊆ 𝐵 → ∩ { 𝑥 ∈ Sℋ ∣ 𝐴 ⊆ 𝑥 } ⊆ ∩ { 𝑥 ∈ Sℋ ∣ 𝐵 ⊆ 𝑥 } )
6	5	adantl	⊢ ( ( 𝐵 ⊆ ℋ ∧ 𝐴 ⊆ 𝐵 ) → ∩ { 𝑥 ∈ Sℋ ∣ 𝐴 ⊆ 𝑥 } ⊆ ∩ { 𝑥 ∈ Sℋ ∣ 𝐵 ⊆ 𝑥 } )
7		sstr	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℋ ) → 𝐴 ⊆ ℋ )
8	7	ancoms	⊢ ( ( 𝐵 ⊆ ℋ ∧ 𝐴 ⊆ 𝐵 ) → 𝐴 ⊆ ℋ )
9		spanval	⊢ ( 𝐴 ⊆ ℋ → ( span ‘ 𝐴 ) = ∩ { 𝑥 ∈ Sℋ ∣ 𝐴 ⊆ 𝑥 } )
10	8 9	syl	⊢ ( ( 𝐵 ⊆ ℋ ∧ 𝐴 ⊆ 𝐵 ) → ( span ‘ 𝐴 ) = ∩ { 𝑥 ∈ Sℋ ∣ 𝐴 ⊆ 𝑥 } )
11		spanval	⊢ ( 𝐵 ⊆ ℋ → ( span ‘ 𝐵 ) = ∩ { 𝑥 ∈ Sℋ ∣ 𝐵 ⊆ 𝑥 } )
12	11	adantr	⊢ ( ( 𝐵 ⊆ ℋ ∧ 𝐴 ⊆ 𝐵 ) → ( span ‘ 𝐵 ) = ∩ { 𝑥 ∈ Sℋ ∣ 𝐵 ⊆ 𝑥 } )
13	6 10 12	3sstr4d	⊢ ( ( 𝐵 ⊆ ℋ ∧ 𝐴 ⊆ 𝐵 ) → ( span ‘ 𝐴 ) ⊆ ( span ‘ 𝐵 ) )