shslubi

Description: The least upper bound law for Hilbert subspace sum. (Contributed by NM, 15-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Hypotheses	shslub.1	$⊢ A \in S_{ℋ}$
	shslub.2	$⊢ B \in S_{ℋ}$
	shslub.3	$⊢ C \in S_{ℋ}$
Assertion	shslubi	$⊢ (A \subseteq C \land B \subseteq C) \leftrightarrow A +_{ℋ} B \subseteq C$

Step	Hyp	Ref	Expression
1		shslub.1	$⊢ A \in S_{ℋ}$
2		shslub.2	$⊢ B \in S_{ℋ}$
3		shslub.3	$⊢ C \in S_{ℋ}$
4	1 3 2	shlessi	$⊢ A \subseteq C \to A +_{ℋ} B \subseteq C +_{ℋ} B$
5	3 2	shscomi	$⊢ C +_{ℋ} B = B +_{ℋ} C$
6	4 5	sseqtrdi	$⊢ A \subseteq C \to A +_{ℋ} B \subseteq B +_{ℋ} C$
7	2 3 3	shlessi	$⊢ B \subseteq C \to B +_{ℋ} C \subseteq C +_{ℋ} C$
8	3	shsidmi	$⊢ C +_{ℋ} C = C$
9	7 8	sseqtrdi	$⊢ B \subseteq C \to B +_{ℋ} C \subseteq C$
10	6 9	sylan9ss	$⊢ (A \subseteq C \land B \subseteq C) \to A +_{ℋ} B \subseteq C$
11	1 2	shsub1i	$⊢ A \subseteq A +_{ℋ} B$
12		sstr	$⊢ (A \subseteq A +_{ℋ} B \land A +_{ℋ} B \subseteq C) \to A \subseteq C$
13	11 12	mpan	$⊢ A +_{ℋ} B \subseteq C \to A \subseteq C$
14	2 1	shsub2i	$⊢ B \subseteq A +_{ℋ} B$
15		sstr	$⊢ (B \subseteq A +_{ℋ} B \land A +_{ℋ} B \subseteq C) \to B \subseteq C$
16	14 15	mpan	$⊢ A +_{ℋ} B \subseteq C \to B \subseteq C$
17	13 16	jca	$⊢ A +_{ℋ} B \subseteq C \to (A \subseteq C \land B \subseteq C)$
18	10 17	impbii	$⊢ (A \subseteq C \land B \subseteq C) \leftrightarrow A +_{ℋ} B \subseteq C$

Metamath Proof Explorer