Theorem shlub

Description: Hilbert lattice join is the least upper bound (among Hilbert lattice elements) of two subspaces. (Contributed by NM, 15-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	shlub	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\wedge C\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(\left(A\subseteq C\wedge B\subseteq C\right)\leftrightarrow A{\vee }_{\mathscr{H}}B\subseteq C\right)$$

Proof

Step	Hyp	Ref	Expression
1		unss	$$⊢\left(A\subseteq C\wedge B\subseteq C\right)\leftrightarrow A\cup B\subseteq C$$
2		simp1	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\wedge C\in {\mathbf{C}}_{\mathscr{H}}\right)\to A\in {\mathbf{S}}_{\mathscr{H}}$$
3		shss	$$⊢A\in {\mathbf{S}}_{\mathscr{H}}\to A\subseteq \mathscr{H}$$
4	2 3	syl	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\wedge C\in {\mathbf{C}}_{\mathscr{H}}\right)\to A\subseteq \mathscr{H}$$
5		simp2	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\wedge C\in {\mathbf{C}}_{\mathscr{H}}\right)\to B\in {\mathbf{S}}_{\mathscr{H}}$$
6		shss	$$⊢B\in {\mathbf{S}}_{\mathscr{H}}\to B\subseteq \mathscr{H}$$
7	5 6	syl	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\wedge C\in {\mathbf{C}}_{\mathscr{H}}\right)\to B\subseteq \mathscr{H}$$
8	4 7	unssd	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\wedge C\in {\mathbf{C}}_{\mathscr{H}}\right)\to A\cup B\subseteq \mathscr{H}$$
9		chss	$$⊢C\in {\mathbf{C}}_{\mathscr{H}}\to C\subseteq \mathscr{H}$$
10	9	3ad2ant3	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\wedge C\in {\mathbf{C}}_{\mathscr{H}}\right)\to C\subseteq \mathscr{H}$$
11		occon2	$$⊢\left(A\cup B\subseteq \mathscr{H}\wedge C\subseteq \mathscr{H}\right)\to \left(A\cup B\subseteq C\to \perp \left(\perp \left(A\cup B\right)\right)\subseteq \perp \left(\perp \left(C\right)\right)\right)$$
12	8 10 11	syl2anc	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\wedge C\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(A\cup B\subseteq C\to \perp \left(\perp \left(A\cup B\right)\right)\subseteq \perp \left(\perp \left(C\right)\right)\right)$$
13	1 12	biimtrid	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\wedge C\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(\left(A\subseteq C\wedge B\subseteq C\right)\to \perp \left(\perp \left(A\cup B\right)\right)\subseteq \perp \left(\perp \left(C\right)\right)\right)$$
14		shjval	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\right)\to A{\vee }_{\mathscr{H}}B=\perp \left(\perp \left(A\cup B\right)\right)$$
15	2 5 14	syl2anc	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\wedge C\in {\mathbf{C}}_{\mathscr{H}}\right)\to A{\vee }_{\mathscr{H}}B=\perp \left(\perp \left(A\cup B\right)\right)$$
16		ococ	$$⊢C\in {\mathbf{C}}_{\mathscr{H}}\to \perp \left(\perp \left(C\right)\right)=C$$
17	16	3ad2ant3	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\wedge C\in {\mathbf{C}}_{\mathscr{H}}\right)\to \perp \left(\perp \left(C\right)\right)=C$$
18	17	eqcomd	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\wedge C\in {\mathbf{C}}_{\mathscr{H}}\right)\to C=\perp \left(\perp \left(C\right)\right)$$
19	15 18	sseq12d	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\wedge C\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(A{\vee }_{\mathscr{H}}B\subseteq C\leftrightarrow \perp \left(\perp \left(A\cup B\right)\right)\subseteq \perp \left(\perp \left(C\right)\right)\right)$$
20	13 19	sylibrd	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\wedge C\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(\left(A\subseteq C\wedge B\subseteq C\right)\to A{\vee }_{\mathscr{H}}B\subseteq C\right)$$
21		shub1	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\right)\to A\subseteq A{\vee }_{\mathscr{H}}B$$
22	2 5 21	syl2anc	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\wedge C\in {\mathbf{C}}_{\mathscr{H}}\right)\to A\subseteq A{\vee }_{\mathscr{H}}B$$
23		sstr	$$⊢\left(A\subseteq A{\vee }_{\mathscr{H}}B\wedge A{\vee }_{\mathscr{H}}B\subseteq C\right)\to A\subseteq C$$
24	22 23	sylan	$$⊢\left(\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\wedge C\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge A{\vee }_{\mathscr{H}}B\subseteq C\right)\to A\subseteq C$$
25		shub2	$$⊢\left(B\in {\mathbf{S}}_{\mathscr{H}}\wedge A\in {\mathbf{S}}_{\mathscr{H}}\right)\to B\subseteq A{\vee }_{\mathscr{H}}B$$
26	5 2 25	syl2anc	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\wedge C\in {\mathbf{C}}_{\mathscr{H}}\right)\to B\subseteq A{\vee }_{\mathscr{H}}B$$
27		sstr	$$⊢\left(B\subseteq A{\vee }_{\mathscr{H}}B\wedge A{\vee }_{\mathscr{H}}B\subseteq C\right)\to B\subseteq C$$
28	26 27	sylan	$$⊢\left(\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\wedge C\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge A{\vee }_{\mathscr{H}}B\subseteq C\right)\to B\subseteq C$$
29	24 28	jca	$$⊢\left(\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\wedge C\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge A{\vee }_{\mathscr{H}}B\subseteq C\right)\to \left(A\subseteq C\wedge B\subseteq C\right)$$
30	29	ex	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\wedge C\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(A{\vee }_{\mathscr{H}}B\subseteq C\to \left(A\subseteq C\wedge B\subseteq C\right)\right)$$
31	20 30	impbid	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\wedge C\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(\left(A\subseteq C\wedge B\subseteq C\right)\leftrightarrow A{\vee }_{\mathscr{H}}B\subseteq C\right)$$