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 ( ( 𝐻 ∈ Sℋ ∧ 𝐴 ∈ ( ⊥ ‘ 𝐻 ) ∧ 𝐴 ≠ 0ℎ ) → ¬ 𝐴 ∈ 𝐻 )

Proof

Step Hyp Ref Expression
1 elin ⊢ ( 𝐴 ∈ ( 𝐻 ∩ ( ⊥ ‘ 𝐻 ) ) ↔ ( 𝐴 ∈ 𝐻 ∧ 𝐴 ∈ ( ⊥ ‘ 𝐻 ) ) )
2 ocin ⊢ ( 𝐻 ∈ Sℋ → ( 𝐻 ∩ ( ⊥ ‘ 𝐻 ) ) = 0ℋ )
3 2 eleq2d ⊢ ( 𝐻 ∈ Sℋ → ( 𝐴 ∈ ( 𝐻 ∩ ( ⊥ ‘ 𝐻 ) ) ↔ 𝐴 ∈ 0ℋ ) )
4 3 biimpd ⊢ ( 𝐻 ∈ Sℋ → ( 𝐴 ∈ ( 𝐻 ∩ ( ⊥ ‘ 𝐻 ) ) → 𝐴 ∈ 0ℋ ) )
5 1 4 biimtrrid ⊢ ( 𝐻 ∈ Sℋ → ( ( 𝐴 ∈ 𝐻 ∧ 𝐴 ∈ ( ⊥ ‘ 𝐻 ) ) → 𝐴 ∈ 0ℋ ) )
6 5 expcomd ⊢ ( 𝐻 ∈ Sℋ → ( 𝐴 ∈ ( ⊥ ‘ 𝐻 ) → ( 𝐴 ∈ 𝐻 → 𝐴 ∈ 0ℋ ) ) )
7 6 imp ⊢ ( ( 𝐻 ∈ Sℋ ∧ 𝐴 ∈ ( ⊥ ‘ 𝐻 ) ) → ( 𝐴 ∈ 𝐻 → 𝐴 ∈ 0ℋ ) )
8 elch0 ⊢ ( 𝐴 ∈ 0ℋ ↔ 𝐴 = 0ℎ )
9 7 8 imbitrdi ⊢ ( ( 𝐻 ∈ Sℋ ∧ 𝐴 ∈ ( ⊥ ‘ 𝐻 ) ) → ( 𝐴 ∈ 𝐻 → 𝐴 = 0ℎ ) )
10 9 necon3ad ⊢ ( ( 𝐻 ∈ Sℋ ∧ 𝐴 ∈ ( ⊥ ‘ 𝐻 ) ) → ( 𝐴 ≠ 0ℎ → ¬ 𝐴 ∈ 𝐻 ) )
11 10 3impia ⊢ ( ( 𝐻 ∈ Sℋ ∧ 𝐴 ∈ ( ⊥ ‘ 𝐻 ) ∧ 𝐴 ≠ 0ℎ ) → ¬ 𝐴 ∈ 𝐻 )