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