Metamath Proof Explorer

Theorem choc0

Description: The orthocomplement of the zero subspace is the unit subspace. (Contributed by NM, 15-Oct-1999) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 h0elsh 
 |-  0H e. SH
2 shocel 
 |-  ( 0H e. SH -> ( x e. ( _|_ ` 0H ) <-> ( x e. ~H /\ A. y e. 0H ( x .ih y ) = 0 ) ) )
3 1 2 ax-mp 
 |-  ( x e. ( _|_ ` 0H ) <-> ( x e. ~H /\ A. y e. 0H ( x .ih y ) = 0 ) )
4 hi02 
 |-  ( x e. ~H -> ( x .ih 0h ) = 0 )
5 df-ral 
 |-  ( A. y e. 0H ( x .ih y ) = 0 <-> A. y ( y e. 0H -> ( x .ih y ) = 0 ) )
6 elch0 
 |-  ( y e. 0H <-> y = 0h )
7 6 imbi1i 
 |-  ( ( y e. 0H -> ( x .ih y ) = 0 ) <-> ( y = 0h -> ( x .ih y ) = 0 ) )
8 7 albii 
 |-  ( A. y ( y e. 0H -> ( x .ih y ) = 0 ) <-> A. y ( y = 0h -> ( x .ih y ) = 0 ) )
9 ax-hv0cl 
 |-  0h e. ~H
10 9 elexi 
 |-  0h e. _V
11 oveq2 
 |-  ( y = 0h -> ( x .ih y ) = ( x .ih 0h ) )
12 11 eqeq1d 
 |-  ( y = 0h -> ( ( x .ih y ) = 0 <-> ( x .ih 0h ) = 0 ) )
13 10 12 ceqsalv 
 |-  ( A. y ( y = 0h -> ( x .ih y ) = 0 ) <-> ( x .ih 0h ) = 0 )
14 8 13 bitri 
 |-  ( A. y ( y e. 0H -> ( x .ih y ) = 0 ) <-> ( x .ih 0h ) = 0 )
15 5 14 bitri 
 |-  ( A. y e. 0H ( x .ih y ) = 0 <-> ( x .ih 0h ) = 0 )
16 4 15 sylibr 
 |-  ( x e. ~H -> A. y e. 0H ( x .ih y ) = 0 )
17 abai 
 |-  ( ( x e. ~H /\ A. y e. 0H ( x .ih y ) = 0 ) <-> ( x e. ~H /\ ( x e. ~H -> A. y e. 0H ( x .ih y ) = 0 ) ) )
18 16 17 mpbiran2 
 |-  ( ( x e. ~H /\ A. y e. 0H ( x .ih y ) = 0 ) <-> x e. ~H )
19 3 18 bitri 
 |-  ( x e. ( _|_ ` 0H ) <-> x e. ~H )
20 19 eqriv 
 |-  ( _|_ ` 0H ) = ~H