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	$⊢ (A \in S_{ℋ} \land B \in S_{ℋ}) \to (A \subseteq ⊥ (B) \to A \cap B = 0_{ℋ})$

Step	Hyp	Ref	Expression
1		ssrin	$⊢ A \subseteq ⊥ (B) \to A \cap B \subseteq ⊥ (B) \cap B$
2		incom	$⊢ ⊥ (B) \cap B = B \cap ⊥ (B)$
3	1 2	sseqtrdi	$⊢ A \subseteq ⊥ (B) \to A \cap B \subseteq B \cap ⊥ (B)$
4		ocin	$⊢ B \in S_{ℋ} \to B \cap ⊥ (B) = 0_{ℋ}$
5	4	sseq2d	$⊢ B \in S_{ℋ} \to (A \cap B \subseteq B \cap ⊥ (B) \leftrightarrow A \cap B \subseteq 0_{ℋ})$
6	3 5	imbitrid	$⊢ B \in S_{ℋ} \to (A \subseteq ⊥ (B) \to A \cap B \subseteq 0_{ℋ})$
7	6	adantl	$⊢ (A \in S_{ℋ} \land B \in S_{ℋ}) \to (A \subseteq ⊥ (B) \to A \cap B \subseteq 0_{ℋ})$
8		shincl	$⊢ (A \in S_{ℋ} \land B \in S_{ℋ}) \to A \cap B \in S_{ℋ}$
9		sh0le	$⊢ A \cap B \in S_{ℋ} \to 0_{ℋ} \subseteq A \cap B$
10	8 9	syl	$⊢ (A \in S_{ℋ} \land B \in S_{ℋ}) \to 0_{ℋ} \subseteq A \cap B$
11	7 10	jctird	$⊢ (A \in S_{ℋ} \land B \in S_{ℋ}) \to (A \subseteq ⊥ (B) \to (A \cap B \subseteq 0_{ℋ} \land 0_{ℋ} \subseteq A \cap B))$
12		eqss	$⊢ A \cap B = 0_{ℋ} \leftrightarrow (A \cap B \subseteq 0_{ℋ} \land 0_{ℋ} \subseteq A \cap B)$
13	11 12	imbitrrdi	$⊢ (A \in S_{ℋ} \land B \in S_{ℋ}) \to (A \subseteq ⊥ (B) \to A \cap B = 0_{ℋ})$

Metamath Proof Explorer