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

Metamath Proof Explorer

Theorem spansnss

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

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

Proof

Step Hyp Ref Expression
1 shel ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ 𝐴 ) → 𝐵 ∈ ℋ )
2 elspansn ⊢ ( 𝐵 ∈ ℋ → ( 𝑥 ∈ ( span ‘ { 𝐵 } ) ↔ ∃ 𝑦 ∈ ℂ 𝑥 = ( 𝑦 ·ℎ 𝐵 ) ) )
3 1 2 syl ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ 𝐴 ) → ( 𝑥 ∈ ( span ‘ { 𝐵 } ) ↔ ∃ 𝑦 ∈ ℂ 𝑥 = ( 𝑦 ·ℎ 𝐵 ) ) )
4 shmulcl ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝑦 ∈ ℂ ∧ 𝐵 ∈ 𝐴 ) → ( 𝑦 ·ℎ 𝐵 ) ∈ 𝐴 )
5 eleq1a ⊢ ( ( 𝑦 ·ℎ 𝐵 ) ∈ 𝐴 → ( 𝑥 = ( 𝑦 ·ℎ 𝐵 ) → 𝑥 ∈ 𝐴 ) )
6 4 5 syl ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝑦 ∈ ℂ ∧ 𝐵 ∈ 𝐴 ) → ( 𝑥 = ( 𝑦 ·ℎ 𝐵 ) → 𝑥 ∈ 𝐴 ) )
7 6 3exp ⊢ ( 𝐴 ∈ Sℋ → ( 𝑦 ∈ ℂ → ( 𝐵 ∈ 𝐴 → ( 𝑥 = ( 𝑦 ·ℎ 𝐵 ) → 𝑥 ∈ 𝐴 ) ) ) )
8 7 com23 ⊢ ( 𝐴 ∈ Sℋ → ( 𝐵 ∈ 𝐴 → ( 𝑦 ∈ ℂ → ( 𝑥 = ( 𝑦 ·ℎ 𝐵 ) → 𝑥 ∈ 𝐴 ) ) ) )
9 8 imp ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ 𝐴 ) → ( 𝑦 ∈ ℂ → ( 𝑥 = ( 𝑦 ·ℎ 𝐵 ) → 𝑥 ∈ 𝐴 ) ) )
10 9 rexlimdv ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ 𝐴 ) → ( ∃ 𝑦 ∈ ℂ 𝑥 = ( 𝑦 ·ℎ 𝐵 ) → 𝑥 ∈ 𝐴 ) )
11 3 10 sylbid ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ 𝐴 ) → ( 𝑥 ∈ ( span ‘ { 𝐵 } ) → 𝑥 ∈ 𝐴 ) )
12 11 ssrdv ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ 𝐴 ) → ( span ‘ { 𝐵 } ) ⊆ 𝐴 )