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 biimtrrid ⊢ 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 imbitrdi ⊢ 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