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