Theorem shjshseli

Description: A closed subspace sum equals Hilbert lattice join. Part of Lemma 31.1.5 of MaedaMaeda p. 136. (Contributed by NM, 30-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	shjshseli	$$⊢A{+}_{\mathscr{H}}B\in {\mathbf{C}}_{\mathscr{H}}\leftrightarrow A{+}_{\mathscr{H}}B=A{\vee }_{\mathscr{H}}B$$

Proof

Step	Hyp	Ref	Expression
1		shjshs.1	$$⊢A\in {\mathbf{S}}_{\mathscr{H}}$$
2		shjshs.2	$$⊢B\in {\mathbf{S}}_{\mathscr{H}}$$
3	1 2	shjshsi	$$⊢A{\vee }_{\mathscr{H}}B=\perp \left(\perp \left(A{+}_{\mathscr{H}}B\right)\right)$$
4		ococ	$$⊢A{+}_{\mathscr{H}}B\in {\mathbf{C}}_{\mathscr{H}}\to \perp \left(\perp \left(A{+}_{\mathscr{H}}B\right)\right)=A{+}_{\mathscr{H}}B$$
5	3 4	syl5req	$$⊢A{+}_{\mathscr{H}}B\in {\mathbf{C}}_{\mathscr{H}}\to A{+}_{\mathscr{H}}B=A{\vee }_{\mathscr{H}}B$$
6	1 2	shjcli	$$⊢A{\vee }_{\mathscr{H}}B\in {\mathbf{C}}_{\mathscr{H}}$$
7		eleq1	$$⊢A{+}_{\mathscr{H}}B=A{\vee }_{\mathscr{H}}B\to \left(A{+}_{\mathscr{H}}B\in {\mathbf{C}}_{\mathscr{H}}\leftrightarrow A{\vee }_{\mathscr{H}}B\in {\mathbf{C}}_{\mathscr{H}}\right)$$
8	6 7	mpbiri	$$⊢A{+}_{\mathscr{H}}B=A{\vee }_{\mathscr{H}}B\to A{+}_{\mathscr{H}}B\in {\mathbf{C}}_{\mathscr{H}}$$
9	5 8	impbii	$$⊢A{+}_{\mathscr{H}}B\in {\mathbf{C}}_{\mathscr{H}}\leftrightarrow A{+}_{\mathscr{H}}B=A{\vee }_{\mathscr{H}}B$$