Theorem 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 {\mathbf{S}}_{\mathscr{H}}$$
	shslub.2	$$⊢B\in {\mathbf{S}}_{\mathscr{H}}$$
	shslub.3	$$⊢C\in {\mathbf{S}}_{\mathscr{H}}$$
Assertion	shslubi	$$⊢\left(A\subseteq C\wedge B\subseteq C\right)\leftrightarrow A{+}_{\mathscr{H}}B\subseteq C$$

Proof

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