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

Metamath Proof Explorer

Theorem chssoc

Description: A closed subspace less than its orthocomplement is zero. (Contributed by NM, 14-Jun-2006) (New usage is discouraged.)

Ref Expression
Assertion chssoc 
|- ( A e. CH -> ( A C_ ( _|_ ` A ) <-> A = 0H ) )

Proof

Step Hyp Ref Expression
1 inidm 
 |-  ( A i^i A ) = A
2 sslin 
 |-  ( A C_ ( _|_ ` A ) -> ( A i^i A ) C_ ( A i^i ( _|_ ` A ) ) )
3 1 2 eqsstrrid 
 |-  ( A C_ ( _|_ ` A ) -> A C_ ( A i^i ( _|_ ` A ) ) )
4 chocin 
 |-  ( A e. CH -> ( A i^i ( _|_ ` A ) ) = 0H )
5 4 sseq2d 
 |-  ( A e. CH -> ( A C_ ( A i^i ( _|_ ` A ) ) <-> A C_ 0H ) )
6 chle0 
 |-  ( A e. CH -> ( A C_ 0H <-> A = 0H ) )
7 5 6 bitrd 
 |-  ( A e. CH -> ( A C_ ( A i^i ( _|_ ` A ) ) <-> A = 0H ) )
8 3 7 imbitrid 
 |-  ( A e. CH -> ( A C_ ( _|_ ` A ) -> A = 0H ) )
9 simpr 
 |-  ( ( A e. CH /\ A = 0H ) -> A = 0H )
10 choccl 
 |-  ( A e. CH -> ( _|_ ` A ) e. CH )
11 ch0le 
 |-  ( ( _|_ ` A ) e. CH -> 0H C_ ( _|_ ` A ) )
12 10 11 syl 
 |-  ( A e. CH -> 0H C_ ( _|_ ` A ) )
13 12 adantr 
 |-  ( ( A e. CH /\ A = 0H ) -> 0H C_ ( _|_ ` A ) )
14 9 13 eqsstrd 
 |-  ( ( A e. CH /\ A = 0H ) -> A C_ ( _|_ ` A ) )
15 14 ex 
 |-  ( A e. CH -> ( A = 0H -> A C_ ( _|_ ` A ) ) )
16 8 15 impbid 
 |-  ( A e. CH -> ( A C_ ( _|_ ` A ) <-> A = 0H ) )