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 ⊢normCV⁡U=normCV⁡U
9 eqid ⊢normCV⁡W=normCV⁡W
10 4 5 6 7 8 9 3 isssp ⊢U∈NrmCVec→W∈H↔W∈NrmCVec∧+v⁡W⊆+v⁡U∧⋅𝑠OLD⁡W⊆⋅𝑠OLD⁡U∧normCV⁡W⊆normCV⁡U
11 10 simplbda ⊢U∈NrmCVec∧W∈H→+v⁡W⊆+v⁡U∧⋅𝑠OLD⁡W⊆⋅𝑠OLD⁡U∧normCV⁡W⊆normCV⁡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