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ℎ ) → ¬ 𝐴 ∈ 𝐻 )