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	ralrimivw	⊢ ( 𝐴 ⊆ 𝐵 → ∀ 𝑥 ∈ Sℋ ( 𝐵 ⊆ 𝑥 → 𝐴 ⊆ 𝑥 ) )
3		ss2rab	⊢ ( { 𝑥 ∈ Sℋ ∣ 𝐵 ⊆ 𝑥 } ⊆ { 𝑥 ∈ Sℋ ∣ 𝐴 ⊆ 𝑥 } ↔ ∀ 𝑥 ∈ Sℋ ( 𝐵 ⊆ 𝑥 → 𝐴 ⊆ 𝑥 ) )
4	2 3	sylibr	⊢ ( 𝐴 ⊆ 𝐵 → { 𝑥 ∈ Sℋ ∣ 𝐵 ⊆ 𝑥 } ⊆ { 𝑥 ∈ Sℋ ∣ 𝐴 ⊆ 𝑥 } )
5		intss	⊢ ( { 𝑥 ∈ Sℋ ∣ 𝐵 ⊆ 𝑥 } ⊆ { 𝑥 ∈ Sℋ ∣ 𝐴 ⊆ 𝑥 } → ∩ { 𝑥 ∈ Sℋ ∣ 𝐴 ⊆ 𝑥 } ⊆ ∩ { 𝑥 ∈ Sℋ ∣ 𝐵 ⊆ 𝑥 } )
6	4 5	syl	⊢ ( 𝐴 ⊆ 𝐵 → ∩ { 𝑥 ∈ Sℋ ∣ 𝐴 ⊆ 𝑥 } ⊆ ∩ { 𝑥 ∈ Sℋ ∣ 𝐵 ⊆ 𝑥 } )
7	6	adantl	⊢ ( ( 𝐵 ⊆ ℋ ∧ 𝐴 ⊆ 𝐵 ) → ∩ { 𝑥 ∈ Sℋ ∣ 𝐴 ⊆ 𝑥 } ⊆ ∩ { 𝑥 ∈ Sℋ ∣ 𝐵 ⊆ 𝑥 } )
8		sstr	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℋ ) → 𝐴 ⊆ ℋ )
9	8	ancoms	⊢ ( ( 𝐵 ⊆ ℋ ∧ 𝐴 ⊆ 𝐵 ) → 𝐴 ⊆ ℋ )
10		spanval	⊢ ( 𝐴 ⊆ ℋ → ( span ‘ 𝐴 ) = ∩ { 𝑥 ∈ Sℋ ∣ 𝐴 ⊆ 𝑥 } )
11	9 10	syl	⊢ ( ( 𝐵 ⊆ ℋ ∧ 𝐴 ⊆ 𝐵 ) → ( span ‘ 𝐴 ) = ∩ { 𝑥 ∈ Sℋ ∣ 𝐴 ⊆ 𝑥 } )
12		spanval	⊢ ( 𝐵 ⊆ ℋ → ( span ‘ 𝐵 ) = ∩ { 𝑥 ∈ Sℋ ∣ 𝐵 ⊆ 𝑥 } )
13	12	adantr	⊢ ( ( 𝐵 ⊆ ℋ ∧ 𝐴 ⊆ 𝐵 ) → ( span ‘ 𝐵 ) = ∩ { 𝑥 ∈ Sℋ ∣ 𝐵 ⊆ 𝑥 } )
14	7 11 13	3sstr4d	⊢ ( ( 𝐵 ⊆ ℋ ∧ 𝐴 ⊆ 𝐵 ) → ( span ‘ 𝐴 ) ⊆ ( span ‘ 𝐵 ) )