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 C_{ℋ} \to (A \subseteq ⊥ (A) \leftrightarrow A = 0_{ℋ})$

Step	Hyp	Ref	Expression
1		inidm	$⊢ A \cap A = A$
2		sslin	$⊢ A \subseteq ⊥ (A) \to A \cap A \subseteq A \cap ⊥ (A)$
3	1 2	eqsstrrid	$⊢ A \subseteq ⊥ (A) \to A \subseteq A \cap ⊥ (A)$
4		chocin	$⊢ A \in C_{ℋ} \to A \cap ⊥ (A) = 0_{ℋ}$
5	4	sseq2d	$⊢ A \in C_{ℋ} \to (A \subseteq A \cap ⊥ (A) \leftrightarrow A \subseteq 0_{ℋ})$
6		chle0	$⊢ A \in C_{ℋ} \to (A \subseteq 0_{ℋ} \leftrightarrow A = 0_{ℋ})$
7	5 6	bitrd	$⊢ A \in C_{ℋ} \to (A \subseteq A \cap ⊥ (A) \leftrightarrow A = 0_{ℋ})$
8	3 7	imbitrid	$⊢ A \in C_{ℋ} \to (A \subseteq ⊥ (A) \to A = 0_{ℋ})$
9		simpr	$⊢ (A \in C_{ℋ} \land A = 0_{ℋ}) \to A = 0_{ℋ}$
10		choccl	$⊢ A \in C_{ℋ} \to ⊥ (A) \in C_{ℋ}$
11		ch0le	$⊢ ⊥ (A) \in C_{ℋ} \to 0_{ℋ} \subseteq ⊥ (A)$
12	10 11	syl	$⊢ A \in C_{ℋ} \to 0_{ℋ} \subseteq ⊥ (A)$
13	12	adantr	$⊢ (A \in C_{ℋ} \land A = 0_{ℋ}) \to 0_{ℋ} \subseteq ⊥ (A)$
14	9 13	eqsstrd	$⊢ (A \in C_{ℋ} \land A = 0_{ℋ}) \to A \subseteq ⊥ (A)$
15	14	ex	$⊢ A \in C_{ℋ} \to (A = 0_{ℋ} \to A \subseteq ⊥ (A))$
16	8 15	impbid	$⊢ A \in C_{ℋ} \to (A \subseteq ⊥ (A) \leftrightarrow A = 0_{ℋ})$

Metamath Proof Explorer