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

Metamath Proof Explorer

Theorem chocin

Description: Intersection of a closed subspace and its orthocomplement. Part of Proposition 1 of Kalmbach p. 65. (Contributed by NM, 13-Jun-2006) (New usage is discouraged.)

Ref Expression
Assertion chocin 
|- ( A e. CH -> ( A i^i ( _|_ ` A ) ) = 0H )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( A = if ( A e. CH , A , 0H ) -> A = if ( A e. CH , A , 0H ) )
2 fveq2 
 |-  ( A = if ( A e. CH , A , 0H ) -> ( _|_ ` A ) = ( _|_ ` if ( A e. CH , A , 0H ) ) )
3 1 2 ineq12d 
 |-  ( A = if ( A e. CH , A , 0H ) -> ( A i^i ( _|_ ` A ) ) = ( if ( A e. CH , A , 0H ) i^i ( _|_ ` if ( A e. CH , A , 0H ) ) ) )
4 3 eqeq1d 
 |-  ( A = if ( A e. CH , A , 0H ) -> ( ( A i^i ( _|_ ` A ) ) = 0H <-> ( if ( A e. CH , A , 0H ) i^i ( _|_ ` if ( A e. CH , A , 0H ) ) ) = 0H ) )
5 h0elch 
 |-  0H e. CH
6 5 elimel 
 |-  if ( A e. CH , A , 0H ) e. CH
7 6 chocini 
 |-  ( if ( A e. CH , A , 0H ) i^i ( _|_ ` if ( A e. CH , A , 0H ) ) ) = 0H
8 4 7 dedth 
 |-  ( A e. CH -> ( A i^i ( _|_ ` A ) ) = 0H )