# 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 syl5bir
` |-  ( 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 syl6ib
` |-  ( ( H e. SH /\ A e. ( _|_ ` H ) ) -> ( A e. H -> A = 0h ) )`
` |-  ( ( H e. SH /\ A e. ( _|_ ` H ) ) -> ( A =/= 0h -> -. A e. H ) )`
` |-  ( ( H e. SH /\ A e. ( _|_ ` H ) /\ A =/= 0h ) -> -. A e. H )`