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	syl5ib	|- ( 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 ) )