Theorem shjshsi

Description: Hilbert lattice join equals the double orthocomplement of subspace sum. (Contributed by NM, 27-Nov-2004) (New usage is discouraged.)

	Ref	Expression
Hypotheses	shjshs.1	$$⊢A\in {\mathbf{S}}_{\mathscr{H}}$$
	shjshs.2	$$⊢B\in {\mathbf{S}}_{\mathscr{H}}$$
Assertion	shjshsi	$$⊢A{\vee }_{\mathscr{H}}B=\perp \left(\perp \left(A{+}_{\mathscr{H}}B\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		shjshs.1	$$⊢A\in {\mathbf{S}}_{\mathscr{H}}$$
2		shjshs.2	$$⊢B\in {\mathbf{S}}_{\mathscr{H}}$$
3		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)$$
4	1 2 3	mp2an	$$⊢A{\vee }_{\mathscr{H}}B=\perp \left(\perp \left(A\cup B\right)\right)$$
5	1 2	shunssi	$$⊢A\cup B\subseteq A{+}_{\mathscr{H}}B$$
6	1	shssii	$$⊢A\subseteq \mathscr{H}$$
7	2	shssii	$$⊢B\subseteq \mathscr{H}$$
8	6 7	unssi	$$⊢A\cup B\subseteq \mathscr{H}$$
9	1 2	shscli	$$⊢A{+}_{\mathscr{H}}B\in {\mathbf{S}}_{\mathscr{H}}$$
10	9	shssii	$$⊢A{+}_{\mathscr{H}}B\subseteq \mathscr{H}$$
11	8 10	occon2i	$$⊢A\cup B\subseteq A{+}_{\mathscr{H}}B\to \perp \left(\perp \left(A\cup B\right)\right)\subseteq \perp \left(\perp \left(A{+}_{\mathscr{H}}B\right)\right)$$
12	5 11	ax-mp	$$⊢\perp \left(\perp \left(A\cup B\right)\right)\subseteq \perp \left(\perp \left(A{+}_{\mathscr{H}}B\right)\right)$$
13	4 12	eqsstri	$$⊢A{\vee }_{\mathscr{H}}B\subseteq \perp \left(\perp \left(A{+}_{\mathscr{H}}B\right)\right)$$
14	1 2	shsleji	$$⊢A{+}_{\mathscr{H}}B\subseteq A{\vee }_{\mathscr{H}}B$$
15	1 2	shjcli	$$⊢A{\vee }_{\mathscr{H}}B\in {\mathbf{C}}_{\mathscr{H}}$$
16	15	chssii	$$⊢A{\vee }_{\mathscr{H}}B\subseteq \mathscr{H}$$
17		occon	$$⊢\left(A{+}_{\mathscr{H}}B\subseteq \mathscr{H}\wedge A{\vee }_{\mathscr{H}}B\subseteq \mathscr{H}\right)\to \left(A{+}_{\mathscr{H}}B\subseteq A{\vee }_{\mathscr{H}}B\to \perp \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \perp \left(A{+}_{\mathscr{H}}B\right)\right)$$
18	10 16 17	mp2an	$$⊢A{+}_{\mathscr{H}}B\subseteq A{\vee }_{\mathscr{H}}B\to \perp \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \perp \left(A{+}_{\mathscr{H}}B\right)$$
19	14 18	ax-mp	$$⊢\perp \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \perp \left(A{+}_{\mathscr{H}}B\right)$$
20		occl	$$⊢A{+}_{\mathscr{H}}B\subseteq \mathscr{H}\to \perp \left(A{+}_{\mathscr{H}}B\right)\in {\mathbf{C}}_{\mathscr{H}}$$
21	10 20	ax-mp	$$⊢\perp \left(A{+}_{\mathscr{H}}B\right)\in {\mathbf{C}}_{\mathscr{H}}$$
22	15 21	chsscon1i	$$⊢\perp \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \perp \left(A{+}_{\mathscr{H}}B\right)\leftrightarrow \perp \left(\perp \left(A{+}_{\mathscr{H}}B\right)\right)\subseteq A{\vee }_{\mathscr{H}}B$$
23	19 22	mpbi	$$⊢\perp \left(\perp \left(A{+}_{\mathscr{H}}B\right)\right)\subseteq A{\vee }_{\mathscr{H}}B$$
24	13 23	eqssi	$$⊢A{\vee }_{\mathscr{H}}B=\perp \left(\perp \left(A{+}_{\mathscr{H}}B\right)\right)$$