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	⊢ 𝐴 ∈ C_ℋ
	Assertion	ococi	⊢ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) = 𝐴

Proof

Step	Hyp	Ref	Expression
1		ococ.1	⊢ 𝐴 ∈ C_ℋ
2	1	chshii	⊢ 𝐴 ∈ S_ℋ
3		shocsh	⊢ ( 𝐴 ∈ S_ℋ → ( ⊥ ‘ 𝐴 ) ∈ S_ℋ )
4	2 3	ax-mp	⊢ ( ⊥ ‘ 𝐴 ) ∈ S_ℋ
5		shocsh	⊢ ( ( ⊥ ‘ 𝐴 ) ∈ S_ℋ → ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∈ S_ℋ )
6	4 5	ax-mp	⊢ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∈ S_ℋ
7		shococss	⊢ ( 𝐴 ∈ S_ℋ → 𝐴 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) )
8	2 7	ax-mp	⊢ 𝐴 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) )
9		incom	⊢ ( ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐴 ) ) = ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) )
10		ocin	⊢ ( ( ⊥ ‘ 𝐴 ) ∈ S_ℋ → ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ) = 0_ℋ )
11	4 10	ax-mp	⊢ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ) = 0_ℋ
12	9 11	eqtri	⊢ ( ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐴 ) ) = 0_ℋ
13	1 6 8 12	omlsii	⊢ 𝐴 = ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) )
14	13	eqcomi	⊢ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) = 𝐴