This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sh1dle

Description: A 1-dimensional subspace is less than or equal to any subspace containing its generating vector. (Contributed by NM, 24-Nov-2004) (New usage is discouraged.)

Ref Expression
Assertion sh1dle ⊢ A ∈ S ℋ ∧ B ∈ A → ⊥ ⁡ ⊥ ⁡ B ⊆ A

Proof

Step Hyp Ref Expression
1 shel ⊢ A ∈ S ℋ ∧ B ∈ A → B ∈ ℋ
2 spansn ⊢ B ∈ ℋ → span ⁡ B = ⊥ ⁡ ⊥ ⁡ B
3 1 2 syl ⊢ A ∈ S ℋ ∧ B ∈ A → span ⁡ B = ⊥ ⁡ ⊥ ⁡ B
4 spansnss ⊢ A ∈ S ℋ ∧ B ∈ A → span ⁡ B ⊆ A
5 3 4 eqsstrrd ⊢ A ∈ S ℋ ∧ B ∈ A → ⊥ ⁡ ⊥ ⁡ B ⊆ A