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 ‘ { 𝐵 } ) ⊆ 𝐴 )