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

Metamath Proof Explorer

Theorem spansnss2

Description: The span of the singleton of an element of a subspace is included in the subspace. (Contributed by NM, 16-Dec-2004) (New usage is discouraged.)

Ref Expression
Assertion spansnss2 ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐵 ∈ 𝐴 ↔ ( span ‘ { 𝐵 } ) ⊆ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 spansnss ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ 𝐴 ) → ( span ‘ { 𝐵 } ) ⊆ 𝐴 )
2 1 ex ⊢ ( 𝐴 ∈ Sℋ → ( 𝐵 ∈ 𝐴 → ( span ‘ { 𝐵 } ) ⊆ 𝐴 ) )
3 2 adantr ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐵 ∈ 𝐴 → ( span ‘ { 𝐵 } ) ⊆ 𝐴 ) )
4 spansnid ⊢ ( 𝐵 ∈ ℋ → 𝐵 ∈ ( span ‘ { 𝐵 } ) )
5 ssel ⊢ ( ( span ‘ { 𝐵 } ) ⊆ 𝐴 → ( 𝐵 ∈ ( span ‘ { 𝐵 } ) → 𝐵 ∈ 𝐴 ) )
6 4 5 syl5com ⊢ ( 𝐵 ∈ ℋ → ( ( span ‘ { 𝐵 } ) ⊆ 𝐴 → 𝐵 ∈ 𝐴 ) )
7 6 adantl ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ ℋ ) → ( ( span ‘ { 𝐵 } ) ⊆ 𝐴 → 𝐵 ∈ 𝐴 ) )
8 3 7 impbid ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐵 ∈ 𝐴 ↔ ( span ‘ { 𝐵 } ) ⊆ 𝐴 ) )