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 )