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

Metamath Proof Explorer

Theorem ocnel

Description: A nonzero vector in the complement of a subspace does not belong to the subspace. (Contributed by NM, 10-Apr-2006) (New usage is discouraged.)

Ref Expression
Assertion ocnel 
|- ( ( H e. SH /\ A e. ( _|_ ` H ) /\ A =/= 0h ) -> -. A e. H )

Proof

Step Hyp Ref Expression
1 elin 
 |-  ( A e. ( H i^i ( _|_ ` H ) ) <-> ( A e. H /\ A e. ( _|_ ` H ) ) )
2 ocin 
 |-  ( H e. SH -> ( H i^i ( _|_ ` H ) ) = 0H )
3 2 eleq2d 
 |-  ( H e. SH -> ( A e. ( H i^i ( _|_ ` H ) ) <-> A e. 0H ) )
4 3 biimpd 
 |-  ( H e. SH -> ( A e. ( H i^i ( _|_ ` H ) ) -> A e. 0H ) )
5 1 4 biimtrrid 
 |-  ( H e. SH -> ( ( A e. H /\ A e. ( _|_ ` H ) ) -> A e. 0H ) )
6 5 expcomd 
 |-  ( H e. SH -> ( A e. ( _|_ ` H ) -> ( A e. H -> A e. 0H ) ) )
7 6 imp 
 |-  ( ( H e. SH /\ A e. ( _|_ ` H ) ) -> ( A e. H -> A e. 0H ) )
8 elch0 
 |-  ( A e. 0H <-> A = 0h )
9 7 8 imbitrdi 
 |-  ( ( H e. SH /\ A e. ( _|_ ` H ) ) -> ( A e. H -> A = 0h ) )
10 9 necon3ad 
 |-  ( ( H e. SH /\ A e. ( _|_ ` H ) ) -> ( A =/= 0h -> -. A e. H ) )
11 10 3impia 
 |-  ( ( H e. SH /\ A e. ( _|_ ` H ) /\ A =/= 0h ) -> -. A e. H )