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 syl5bir ( 𝐻S → ( ( 𝐴𝐻𝐴 ∈ ( ⊥ ‘ 𝐻 ) ) → 𝐴 ∈ 0 ) )
6 5 expcomd ( 𝐻S → ( 𝐴 ∈ ( ⊥ ‘ 𝐻 ) → ( 𝐴𝐻𝐴 ∈ 0 ) ) )
7 6 imp ( ( 𝐻S𝐴 ∈ ( ⊥ ‘ 𝐻 ) ) → ( 𝐴𝐻𝐴 ∈ 0 ) )
8 elch0 ( 𝐴 ∈ 0𝐴 = 0 )
9 7 8 syl6ib ( ( 𝐻S𝐴 ∈ ( ⊥ ‘ 𝐻 ) ) → ( 𝐴𝐻𝐴 = 0 ) )
10 9 necon3ad ( ( 𝐻S𝐴 ∈ ( ⊥ ‘ 𝐻 ) ) → ( 𝐴 ≠ 0 → ¬ 𝐴𝐻 ) )
11 10 3impia ( ( 𝐻S𝐴 ∈ ( ⊥ ‘ 𝐻 ) ∧ 𝐴 ≠ 0 ) → ¬ 𝐴𝐻 )