Theorem h1did

Description: A generating vector belongs to the 1-dimensional subspace it generates. (Contributed by NM, 22-Jul-2001) (New usage is discouraged.)

	Ref	Expression
Assertion	h1did	⊢ ( 𝐴 ∈ ℋ → 𝐴 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐴 } ) ) )

Proof

Step	Hyp	Ref	Expression
1		snssi	⊢ ( 𝐴 ∈ ℋ → { 𝐴 } ⊆ ℋ )
2		ococss	⊢ ( { 𝐴 } ⊆ ℋ → { 𝐴 } ⊆ ( ⊥ ‘ ( ⊥ ‘ { 𝐴 } ) ) )
3	1 2	syl	⊢ ( 𝐴 ∈ ℋ → { 𝐴 } ⊆ ( ⊥ ‘ ( ⊥ ‘ { 𝐴 } ) ) )
4		snssg	⊢ ( 𝐴 ∈ ℋ → ( 𝐴 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐴 } ) ) ↔ { 𝐴 } ⊆ ( ⊥ ‘ ( ⊥ ‘ { 𝐴 } ) ) ) )
5	3 4	mpbird	⊢ ( 𝐴 ∈ ℋ → 𝐴 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐴 } ) ) )