Theorem sspba

Description: The base set of a subspace is included in the parent base set. (Contributed by NM, 27-Jan-2008) (New usage is discouraged.)

	Ref	Expression
Hypotheses	sspba.x	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
	sspba.y	⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
	sspba.h	⊢ 𝐻 = ( SubSp ‘ 𝑈 )
Assertion	sspba	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → 𝑌 ⊆ 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		sspba.x	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2		sspba.y	⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
3		sspba.h	⊢ 𝐻 = ( SubSp ‘ 𝑈 )
4		eqid	⊢ ( +𝑣 ‘ 𝑈 ) = ( +𝑣 ‘ 𝑈 )
5		eqid	⊢ ( +𝑣 ‘ 𝑊 ) = ( +𝑣 ‘ 𝑊 )
6		eqid	⊢ ( ·𝑠OLD ‘ 𝑈 ) = ( ·𝑠OLD ‘ 𝑈 )
7		eqid	⊢ ( ·𝑠OLD ‘ 𝑊 ) = ( ·𝑠OLD ‘ 𝑊 )
8		eqid	⊢ ( normCV ‘ 𝑈 ) = ( normCV ‘ 𝑈 )
9		eqid	⊢ ( normCV ‘ 𝑊 ) = ( normCV ‘ 𝑊 )
10	4 5 6 7 8 9 3	isssp	⊢ ( 𝑈 ∈ NrmCVec → ( 𝑊 ∈ 𝐻 ↔ ( 𝑊 ∈ NrmCVec ∧ ( ( +𝑣 ‘ 𝑊 ) ⊆ ( +𝑣 ‘ 𝑈 ) ∧ ( ·𝑠OLD ‘ 𝑊 ) ⊆ ( ·𝑠OLD ‘ 𝑈 ) ∧ ( normCV ‘ 𝑊 ) ⊆ ( normCV ‘ 𝑈 ) ) ) ) )
11	10	simplbda	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → ( ( +𝑣 ‘ 𝑊 ) ⊆ ( +𝑣 ‘ 𝑈 ) ∧ ( ·𝑠OLD ‘ 𝑊 ) ⊆ ( ·𝑠OLD ‘ 𝑈 ) ∧ ( normCV ‘ 𝑊 ) ⊆ ( normCV ‘ 𝑈 ) ) )
12	11	simp1d	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → ( +𝑣 ‘ 𝑊 ) ⊆ ( +𝑣 ‘ 𝑈 ) )
13		rnss	⊢ ( ( +𝑣 ‘ 𝑊 ) ⊆ ( +𝑣 ‘ 𝑈 ) → ran ( +𝑣 ‘ 𝑊 ) ⊆ ran ( +𝑣 ‘ 𝑈 ) )
14	12 13	syl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → ran ( +𝑣 ‘ 𝑊 ) ⊆ ran ( +𝑣 ‘ 𝑈 ) )
15	2 5	bafval	⊢ 𝑌 = ran ( +𝑣 ‘ 𝑊 )
16	1 4	bafval	⊢ 𝑋 = ran ( +𝑣 ‘ 𝑈 )
17	14 15 16	3sstr4g	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → 𝑌 ⊆ 𝑋 )