Theorem orthin

Description: The intersection of orthogonal subspaces is the zero subspace. (Contributed by NM, 24-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	orthin	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\right)\to \left(A\subseteq \perp \left(B\right)\to A\cap B=0_{\mathscr{H}}\right)$$

Proof

Step	Hyp	Ref	Expression
1		ssrin	$$⊢A\subseteq \perp \left(B\right)\to A\cap B\subseteq \perp \left(B\right)\cap B$$
2		incom	$$⊢\perp \left(B\right)\cap B=B\cap \perp \left(B\right)$$
3	1 2	sseqtrdi	$$⊢A\subseteq \perp \left(B\right)\to A\cap B\subseteq B\cap \perp \left(B\right)$$
4		ocin	$$⊢B\in {\mathbf{S}}_{\mathscr{H}}\to B\cap \perp \left(B\right)=0_{\mathscr{H}}$$
5	4	sseq2d	$$⊢B\in {\mathbf{S}}_{\mathscr{H}}\to \left(A\cap B\subseteq B\cap \perp \left(B\right)\leftrightarrow A\cap B\subseteq 0_{\mathscr{H}}\right)$$
6	3 5	imbitrid	$$⊢B\in {\mathbf{S}}_{\mathscr{H}}\to \left(A\subseteq \perp \left(B\right)\to A\cap B\subseteq 0_{\mathscr{H}}\right)$$
7	6	adantl	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\right)\to \left(A\subseteq \perp \left(B\right)\to A\cap B\subseteq 0_{\mathscr{H}}\right)$$
8		shincl	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\right)\to A\cap B\in {\mathbf{S}}_{\mathscr{H}}$$
9		sh0le	$$⊢A\cap B\in {\mathbf{S}}_{\mathscr{H}}\to 0_{\mathscr{H}}\subseteq A\cap B$$
10	8 9	syl	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\right)\to 0_{\mathscr{H}}\subseteq A\cap B$$
11	7 10	jctird	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\right)\to \left(A\subseteq \perp \left(B\right)\to \left(A\cap B\subseteq 0_{\mathscr{H}}\wedge 0_{\mathscr{H}}\subseteq A\cap B\right)\right)$$
12		eqss	$$⊢A\cap B=0_{\mathscr{H}}\leftrightarrow \left(A\cap B\subseteq 0_{\mathscr{H}}\wedge 0_{\mathscr{H}}\subseteq A\cap B\right)$$
13	11 12	imbitrrdi	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\right)\to \left(A\subseteq \perp \left(B\right)\to A\cap B=0_{\mathscr{H}}\right)$$