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	⊢ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) = 𝐴