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 ) )
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 )