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 B A B span A span B

Proof

Step Hyp Ref Expression
1 sstr2 A B B x A x
2 1 adantr A B x S B x A x
3 2 ss2rabdv A B x S | B x x S | A x
4 intss x S | B x x S | A x x S | A x x S | B x
5 3 4 syl A B x S | A x x S | B x
6 5 adantl B A B x S | A x x S | B x
7 sstr A B B A
8 7 ancoms B A B A
9 spanval A span A = x S | A x
10 8 9 syl B A B span A = x S | A x
11 spanval B span B = x S | B x
12 11 adantr B A B span B = x S | B x
13 6 10 12 3sstr4d B A B span A span B