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 e. CH
Assertion ococi 
|- ( _|_ ` ( _|_ ` A ) ) = A

Proof

Step Hyp Ref Expression
1 ococ.1 
 |-  A e. CH
2 1 chshii 
 |-  A e. SH
3 shocsh 
 |-  ( A e. SH -> ( _|_ ` A ) e. SH )
4 2 3 ax-mp 
 |-  ( _|_ ` A ) e. SH
5 shocsh 
 |-  ( ( _|_ ` A ) e. SH -> ( _|_ ` ( _|_ ` A ) ) e. SH )
6 4 5 ax-mp 
 |-  ( _|_ ` ( _|_ ` A ) ) e. SH
7 shococss 
 |-  ( A e. SH -> A C_ ( _|_ ` ( _|_ ` A ) ) )
8 2 7 ax-mp 
 |-  A C_ ( _|_ ` ( _|_ ` A ) )
9 incom 
 |-  ( ( _|_ ` ( _|_ ` A ) ) i^i ( _|_ ` A ) ) = ( ( _|_ ` A ) i^i ( _|_ ` ( _|_ ` A ) ) )
10 ocin 
 |-  ( ( _|_ ` A ) e. SH -> ( ( _|_ ` A ) i^i ( _|_ ` ( _|_ ` A ) ) ) = 0H )
11 4 10 ax-mp 
 |-  ( ( _|_ ` A ) i^i ( _|_ ` ( _|_ ` A ) ) ) = 0H
12 9 11 eqtri 
 |-  ( ( _|_ ` ( _|_ ` A ) ) i^i ( _|_ ` A ) ) = 0H
13 1 6 8 12 omlsii 
 |-  A = ( _|_ ` ( _|_ ` A ) )
14 13 eqcomi 
 |-  ( _|_ ` ( _|_ ` A ) ) = A