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