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