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 S A H A 0 ¬ A H

Proof

Step Hyp Ref Expression
1 elin A H H A H A H
2 ocin H S H H = 0
3 2 eleq2d H S A H H A 0
4 3 biimpd H S A H H A 0
5 1 4 syl5bir H S A H A H A 0
6 5 expcomd H S A H A H A 0
7 6 imp H S A H A H A 0
8 elch0 A 0 A = 0
9 7 8 syl6ib H S A H A H A = 0
10 9 necon3ad H S A H A 0 ¬ A H
11 10 3impia H S A H A 0 ¬ A H