This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ococi

Description: Complement of complement of a closed subspace of Hilbert space. Theorem 3.7(ii) of Beran p. 102. (Contributed by NM, 11-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypothesis ococ.1 ⊢ A ∈ C ℋ
Assertion ococi ⊢ ⊥ ⁡ ⊥ ⁡ A = A

Proof

Step Hyp Ref Expression
1 ococ.1 ⊢ A ∈ C ℋ
2 1 chshii ⊢ A ∈ S ℋ
3 shocsh ⊢ A ∈ S ℋ → ⊥ ⁡ A ∈ S ℋ
4 2 3 ax-mp ⊢ ⊥ ⁡ A ∈ S ℋ
5 shocsh ⊢ ⊥ ⁡ A ∈ S ℋ → ⊥ ⁡ ⊥ ⁡ A ∈ S ℋ
6 4 5 ax-mp ⊢ ⊥ ⁡ ⊥ ⁡ A ∈ S ℋ
7 shococss ⊢ A ∈ S ℋ → A ⊆ ⊥ ⁡ ⊥ ⁡ A
8 2 7 ax-mp ⊢ A ⊆ ⊥ ⁡ ⊥ ⁡ A
9 incom ⊢ ⊥ ⁡ ⊥ ⁡ A ∩ ⊥ ⁡ A = ⊥ ⁡ A ∩ ⊥ ⁡ ⊥ ⁡ A
10 ocin ⊢ ⊥ ⁡ A ∈ S ℋ → ⊥ ⁡ A ∩ ⊥ ⁡ ⊥ ⁡ A = 0 ℋ
11 4 10 ax-mp ⊢ ⊥ ⁡ A ∩ ⊥ ⁡ ⊥ ⁡ A = 0 ℋ
12 9 11 eqtri ⊢ ⊥ ⁡ ⊥ ⁡ A ∩ ⊥ ⁡ A = 0 ℋ
13 1 6 8 12 omlsii ⊢ A = ⊥ ⁡ ⊥ ⁡ A
14 13 eqcomi ⊢ ⊥ ⁡ ⊥ ⁡ A = A