Theorem shlesb1i

Description: Hilbert lattice ordering in terms of subspace sum. (Contributed by NM, 23-Nov-2004) (New usage is discouraged.)

	Ref	Expression
Hypotheses	shlesb1.1	$$⊢A\in {\mathbf{S}}_{\mathscr{H}}$$
	shlesb1.2	$$⊢B\in {\mathbf{S}}_{\mathscr{H}}$$
Assertion	shlesb1i	$$⊢A\subseteq B\leftrightarrow A{+}_{\mathscr{H}}B=B$$

Proof

Step	Hyp	Ref	Expression
1		shlesb1.1	$$⊢A\in {\mathbf{S}}_{\mathscr{H}}$$
2		shlesb1.2	$$⊢B\in {\mathbf{S}}_{\mathscr{H}}$$
3		ssid	$$⊢B\subseteq B$$
4	3	biantrur	$$⊢A\subseteq B\leftrightarrow \left(B\subseteq B\wedge A\subseteq B\right)$$
5	2 1 2	shslubi	$$⊢\left(B\subseteq B\wedge A\subseteq B\right)\leftrightarrow B{+}_{\mathscr{H}}A\subseteq B$$
6	2 1	shsub2i	$$⊢B\subseteq A{+}_{\mathscr{H}}B$$
7		eqss	$$⊢A{+}_{\mathscr{H}}B=B\leftrightarrow \left(A{+}_{\mathscr{H}}B\subseteq B\wedge B\subseteq A{+}_{\mathscr{H}}B\right)$$
8	6 7	mpbiran2	$$⊢A{+}_{\mathscr{H}}B=B\leftrightarrow A{+}_{\mathscr{H}}B\subseteq B$$
9	1 2	shscomi	$$⊢A{+}_{\mathscr{H}}B=B{+}_{\mathscr{H}}A$$
10	9	sseq1i	$$⊢A{+}_{\mathscr{H}}B\subseteq B\leftrightarrow B{+}_{\mathscr{H}}A\subseteq B$$
11	8 10	bitr2i	$$⊢B{+}_{\mathscr{H}}A\subseteq B\leftrightarrow A{+}_{\mathscr{H}}B=B$$
12	4 5 11	3bitri	$$⊢A\subseteq B\leftrightarrow A{+}_{\mathscr{H}}B=B$$