Metamath Proof Explorer

Theorem choc1

Description: The orthocomplement of the unit subspace is the zero subspace. Does not require Axiom of Choice. (Contributed by NM, 24-Oct-1999) (New usage is discouraged.)

Ref Expression
Assertion choc1 
|- ( _|_ ` ~H ) = 0H

Proof

Step Hyp Ref Expression
1 helsh 
 |-  ~H e. SH
2 shocel 
 |-  ( ~H e. SH -> ( x e. ( _|_ ` ~H ) <-> ( x e. ~H /\ A. y e. ~H ( x .ih y ) = 0 ) ) )
3 1 2 ax-mp 
 |-  ( x e. ( _|_ ` ~H ) <-> ( x e. ~H /\ A. y e. ~H ( x .ih y ) = 0 ) )
4 3 simprbi 
 |-  ( x e. ( _|_ ` ~H ) -> A. y e. ~H ( x .ih y ) = 0 )
5 shocss 
 |-  ( ~H e. SH -> ( _|_ ` ~H ) C_ ~H )
6 1 5 ax-mp 
 |-  ( _|_ ` ~H ) C_ ~H
7 6 sseli 
 |-  ( x e. ( _|_ ` ~H ) -> x e. ~H )
8 hial0 
 |-  ( x e. ~H -> ( A. y e. ~H ( x .ih y ) = 0 <-> x = 0h ) )
9 7 8 syl 
 |-  ( x e. ( _|_ ` ~H ) -> ( A. y e. ~H ( x .ih y ) = 0 <-> x = 0h ) )
10 4 9 mpbid 
 |-  ( x e. ( _|_ ` ~H ) -> x = 0h )
11 elch0 
 |-  ( x e. 0H <-> x = 0h )
12 10 11 sylibr 
 |-  ( x e. ( _|_ ` ~H ) -> x e. 0H )
13 12 ssriv 
 |-  ( _|_ ` ~H ) C_ 0H
14 h0elsh 
 |-  0H e. SH
15 shococss 
 |-  ( 0H e. SH -> 0H C_ ( _|_ ` ( _|_ ` 0H ) ) )
16 14 15 ax-mp 
 |-  0H C_ ( _|_ ` ( _|_ ` 0H ) )
17 choc0 
 |-  ( _|_ ` 0H ) = ~H
18 17 fveq2i 
 |-  ( _|_ ` ( _|_ ` 0H ) ) = ( _|_ ` ~H )
19 16 18 sseqtri 
 |-  0H C_ ( _|_ ` ~H )
20 13 19 eqssi 
 |-  ( _|_ ` ~H ) = 0H