Theorem chssoc

Description: A closed subspace less than its orthocomplement is zero. (Contributed by NM, 14-Jun-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	chssoc	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to \left(A\subseteq \perp \left(A\right)\leftrightarrow A=0_{\mathscr{H}}\right)$$

Proof

Step	Hyp	Ref	Expression
1		inidm	$$⊢A\cap A=A$$
2		sslin	$$⊢A\subseteq \perp \left(A\right)\to A\cap A\subseteq A\cap \perp \left(A\right)$$
3	1 2	eqsstrrid	$$⊢A\subseteq \perp \left(A\right)\to A\subseteq A\cap \perp \left(A\right)$$
4		chocin	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to A\cap \perp \left(A\right)=0_{\mathscr{H}}$$
5	4	sseq2d	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to \left(A\subseteq A\cap \perp \left(A\right)\leftrightarrow A\subseteq 0_{\mathscr{H}}\right)$$
6		chle0	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to \left(A\subseteq 0_{\mathscr{H}}\leftrightarrow A=0_{\mathscr{H}}\right)$$
7	5 6	bitrd	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to \left(A\subseteq A\cap \perp \left(A\right)\leftrightarrow A=0_{\mathscr{H}}\right)$$
8	3 7	syl5ib	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to \left(A\subseteq \perp \left(A\right)\to A=0_{\mathscr{H}}\right)$$
9		simpr	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge A=0_{\mathscr{H}}\right)\to A=0_{\mathscr{H}}$$
10		choccl	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to \perp \left(A\right)\in {\mathbf{C}}_{\mathscr{H}}$$
11		ch0le	$$⊢\perp \left(A\right)\in {\mathbf{C}}_{\mathscr{H}}\to 0_{\mathscr{H}}\subseteq \perp \left(A\right)$$
12	10 11	syl	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to 0_{\mathscr{H}}\subseteq \perp \left(A\right)$$
13	12	adantr	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge A=0_{\mathscr{H}}\right)\to 0_{\mathscr{H}}\subseteq \perp \left(A\right)$$
14	9 13	eqsstrd	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge A=0_{\mathscr{H}}\right)\to A\subseteq \perp \left(A\right)$$
15	14	ex	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to \left(A=0_{\mathscr{H}}\to A\subseteq \perp \left(A\right)\right)$$
16	8 15	impbid	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to \left(A\subseteq \perp \left(A\right)\leftrightarrow A=0_{\mathscr{H}}\right)$$