Theorem h1dn0

Description: A nonzero vector generates a (nonzero) 1-dimensional subspace. (Contributed by NM, 22-Jul-2001) (New usage is discouraged.)

	Ref	Expression
Assertion	h1dn0	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( ⊥ ‘ ( ⊥ ‘ { 𝐴 } ) ) ≠ 0ℋ )

Proof

Step	Hyp	Ref	Expression
1		h1did	⊢ ( 𝐴 ∈ ℋ → 𝐴 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐴 } ) ) )
2		eleq2	⊢ ( ( ⊥ ‘ ( ⊥ ‘ { 𝐴 } ) ) = 0ℋ → ( 𝐴 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐴 } ) ) ↔ 𝐴 ∈ 0ℋ ) )
3	1 2	syl5ibcom	⊢ ( 𝐴 ∈ ℋ → ( ( ⊥ ‘ ( ⊥ ‘ { 𝐴 } ) ) = 0ℋ → 𝐴 ∈ 0ℋ ) )
4		elch0	⊢ ( 𝐴 ∈ 0ℋ ↔ 𝐴 = 0ℎ )
5	3 4	imbitrdi	⊢ ( 𝐴 ∈ ℋ → ( ( ⊥ ‘ ( ⊥ ‘ { 𝐴 } ) ) = 0ℋ → 𝐴 = 0ℎ ) )
6	5	necon3d	⊢ ( 𝐴 ∈ ℋ → ( 𝐴 ≠ 0ℎ → ( ⊥ ‘ ( ⊥ ‘ { 𝐴 } ) ) ≠ 0ℋ ) )
7	6	imp	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( ⊥ ‘ ( ⊥ ‘ { 𝐴 } ) ) ≠ 0ℋ )