choc1

Description: The orthocomplement of the unit subspace is the zero subspace. Does not require Axiom of Choice. (Contributed by NM, 24-Oct-1999) (New usage is discouraged.)

		Ref	Expression
	Assertion	choc1	$⊢ ⊥ (ℋ) = 0_{ℋ}$

Proof

Step	Hyp	Ref	Expression
1		helsh	$⊢ ℋ \in S_{ℋ}$
2		shocel	$⊢ ℋ \in S_{ℋ} \to (x \in ⊥ (ℋ) \leftrightarrow (x \in ℋ \land \forall y \in ℋ x \cdot_{ih} y = 0))$
3	1 2	ax-mp	$⊢ x \in ⊥ (ℋ) \leftrightarrow (x \in ℋ \land \forall y \in ℋ x \cdot_{ih} y = 0)$
4	3	simprbi	$⊢ x \in ⊥ (ℋ) \to \forall y \in ℋ x \cdot_{ih} y = 0$
5		shocss	$⊢ ℋ \in S_{ℋ} \to ⊥ (ℋ) \subseteq ℋ$
6	1 5	ax-mp	$⊢ ⊥ (ℋ) \subseteq ℋ$
7	6	sseli	$⊢ x \in ⊥ (ℋ) \to x \in ℋ$
8		hial0	$⊢ x \in ℋ \to (\forall y \in ℋ x \cdot_{ih} y = 0 \leftrightarrow x = 0_{ℎ})$
9	7 8	syl	$⊢ x \in ⊥ (ℋ) \to (\forall y \in ℋ x \cdot_{ih} y = 0 \leftrightarrow x = 0_{ℎ})$
10	4 9	mpbid	$⊢ x \in ⊥ (ℋ) \to x = 0_{ℎ}$
11		elch0	$⊢ x \in 0_{ℋ} \leftrightarrow x = 0_{ℎ}$
12	10 11	sylibr	$⊢ x \in ⊥ (ℋ) \to x \in 0_{ℋ}$
13	12	ssriv	$⊢ ⊥ (ℋ) \subseteq 0_{ℋ}$
14		h0elsh	$⊢ 0_{ℋ} \in S_{ℋ}$
15		shococss	$⊢ 0_{ℋ} \in S_{ℋ} \to 0_{ℋ} \subseteq ⊥ (⊥ (0_{ℋ}))$
16	14 15	ax-mp	$⊢ 0_{ℋ} \subseteq ⊥ (⊥ (0_{ℋ}))$
17		choc0	$⊢ ⊥ (0_{ℋ}) = ℋ$
18	17	fveq2i	$⊢ ⊥ (⊥ (0_{ℋ})) = ⊥ (ℋ)$
19	16 18	sseqtri	$⊢ 0_{ℋ} \subseteq ⊥ (ℋ)$
20	13 19	eqssi	$⊢ ⊥ (ℋ) = 0_{ℋ}$

Metamath Proof Explorer

Theorem choc1

Proof