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 \subseteq ℋ \land A \subseteq B) \to span (A) \subseteq span (B)$

Step	Hyp	Ref	Expression
1		sstr2	$⊢ A \subseteq B \to (B \subseteq x \to A \subseteq x)$
2	1	adantr	$⊢ (A \subseteq B \land x \in S_{ℋ}) \to (B \subseteq x \to A \subseteq x)$
3	2	ss2rabdv	$⊢ A \subseteq B \to \{x \in S_{ℋ} \| B \subseteq x\} \subseteq \{x \in S_{ℋ} \| A \subseteq x\}$
4		intss	$⊢ \{x \in S_{ℋ} \| B \subseteq x\} \subseteq \{x \in S_{ℋ} \| A \subseteq x\} \to ⋂ \{x \in S_{ℋ} \| A \subseteq x\} \subseteq ⋂ \{x \in S_{ℋ} \| B \subseteq x\}$
5	3 4	syl	$⊢ A \subseteq B \to ⋂ \{x \in S_{ℋ} \| A \subseteq x\} \subseteq ⋂ \{x \in S_{ℋ} \| B \subseteq x\}$
6	5	adantl	$⊢ (B \subseteq ℋ \land A \subseteq B) \to ⋂ \{x \in S_{ℋ} \| A \subseteq x\} \subseteq ⋂ \{x \in S_{ℋ} \| B \subseteq x\}$
7		sstr	$⊢ (A \subseteq B \land B \subseteq ℋ) \to A \subseteq ℋ$
8	7	ancoms	$⊢ (B \subseteq ℋ \land A \subseteq B) \to A \subseteq ℋ$
9		spanval	$⊢ A \subseteq ℋ \to span (A) = ⋂ \{x \in S_{ℋ} \| A \subseteq x\}$
10	8 9	syl	$⊢ (B \subseteq ℋ \land A \subseteq B) \to span (A) = ⋂ \{x \in S_{ℋ} \| A \subseteq x\}$
11		spanval	$⊢ B \subseteq ℋ \to span (B) = ⋂ \{x \in S_{ℋ} \| B \subseteq x\}$
12	11	adantr	$⊢ (B \subseteq ℋ \land A \subseteq B) \to span (B) = ⋂ \{x \in S_{ℋ} \| B \subseteq x\}$
13	6 10 12	3sstr4d	$⊢ (B \subseteq ℋ \land A \subseteq B) \to span (A) \subseteq span (B)$

Metamath Proof Explorer