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

Metamath Proof Explorer

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 ∧ 𝑊 ∈ 𝐻 ) → 𝑌 ⊆ 𝑋 )