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 ⊢ X = BaseSet ⁡ U
sspba.y ⊢ Y = BaseSet ⁡ W
sspba.h ⊢ H = SubSp ⁡ U
Assertion sspba ⊢ U ∈ NrmCVec ∧ W ∈ H → Y ⊆ X

Proof

Step Hyp Ref Expression
1 sspba.x ⊢ X = BaseSet ⁡ U
2 sspba.y ⊢ Y = BaseSet ⁡ W
3 sspba.h ⊢ H = SubSp ⁡ U
4 eqid ⊢ + v ⁡ U = + v ⁡ U
5 eqid ⊢ + v ⁡ W = + v ⁡ W
6 eqid ⊢ ⋅ 𝑠OLD ⁡ U = ⋅ 𝑠OLD ⁡ U
7 eqid ⊢ ⋅ 𝑠OLD ⁡ W = ⋅ 𝑠OLD ⁡ W
8 eqid ⊢ norm CV ⁡ U = norm CV ⁡ U
9 eqid ⊢ norm CV ⁡ W = norm CV ⁡ W
10 4 5 6 7 8 9 3 isssp ⊢ U ∈ NrmCVec → W ∈ H ↔ W ∈ NrmCVec ∧ + v ⁡ W ⊆ + v ⁡ U ∧ ⋅ 𝑠OLD ⁡ W ⊆ ⋅ 𝑠OLD ⁡ U ∧ norm CV ⁡ W ⊆ norm CV ⁡ U
11 10 simplbda ⊢ U ∈ NrmCVec ∧ W ∈ H → + v ⁡ W ⊆ + v ⁡ U ∧ ⋅ 𝑠OLD ⁡ W ⊆ ⋅ 𝑠OLD ⁡ U ∧ norm CV ⁡ W ⊆ norm CV ⁡ U
12 11 simp1d ⊢ U ∈ NrmCVec ∧ W ∈ H → + v ⁡ W ⊆ + v ⁡ U
13 rnss ⊢ + v ⁡ W ⊆ + v ⁡ U → ran ⁡ + v ⁡ W ⊆ ran ⁡ + v ⁡ U
14 12 13 syl ⊢ U ∈ NrmCVec ∧ W ∈ H → ran ⁡ + v ⁡ W ⊆ ran ⁡ + v ⁡ U
15 2 5 bafval ⊢ Y = ran ⁡ + v ⁡ W
16 1 4 bafval ⊢ X = ran ⁡ + v ⁡ U
17 14 15 16 3sstr4g ⊢ U ∈ NrmCVec ∧ W ∈ H → Y ⊆ X