This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝐵 ) )