Metamath Proof Explorer

Theorem hhsst

Description: A member of SH is a subspace. (Contributed by NM, 6-Apr-2008) (New usage is discouraged.)

Ref Expression
Hypotheses hhsst.1 ⊢U=+ℎ⋅ℎnormℎ
hhsst.2 ⊢W=+ℎ↾H×H⋅ℎ↾ℂ×Hnormℎ↾H
Assertion hhsst ⊢H∈Sℋ→W∈SubSp⁡U

Proof

Step Hyp Ref Expression
1 hhsst.1 ⊢U=+ℎ⋅ℎnormℎ
2 hhsst.2 ⊢W=+ℎ↾H×H⋅ℎ↾ℂ×Hnormℎ↾H
3 2 hhssnvt ⊢H∈Sℋ→W∈NrmCVec
4 resss ⊢+ℎ↾H×H⊆+ℎ
5 resss ⊢⋅ℎ↾ℂ×H⊆⋅ℎ
6 resss ⊢normℎ↾H⊆normℎ
7 4 5 6 3pm3.2i ⊢+ℎ↾H×H⊆+ℎ∧⋅ℎ↾ℂ×H⊆⋅ℎ∧normℎ↾H⊆normℎ
8 3 7 jctir ⊢H∈Sℋ→W∈NrmCVec∧+ℎ↾H×H⊆+ℎ∧⋅ℎ↾ℂ×H⊆⋅ℎ∧normℎ↾H⊆normℎ
9 1 hhnv ⊢U∈NrmCVec
10 1 hhva ⊢+ℎ=+v⁡U
11 2 hhssva ⊢+ℎ↾H×H=+v⁡W
12 1 hhsm ⊢⋅ℎ=⋅𝑠OLD⁡U
13 2 hhsssm ⊢⋅ℎ↾ℂ×H=⋅𝑠OLD⁡W
14 1 hhnm ⊢normℎ=normCV⁡U
15 2 hhssnm ⊢normℎ↾H=normCV⁡W
16 eqid ⊢SubSp⁡U=SubSp⁡U
17 10 11 12 13 14 15 16 isssp ⊢U∈NrmCVec→W∈SubSp⁡U↔W∈NrmCVec∧+ℎ↾H×H⊆+ℎ∧⋅ℎ↾ℂ×H⊆⋅ℎ∧normℎ↾H⊆normℎ
18 9 17 ax-mp ⊢W∈SubSp⁡U↔W∈NrmCVec∧+ℎ↾H×H⊆+ℎ∧⋅ℎ↾ℂ×H⊆⋅ℎ∧normℎ↾H⊆normℎ
19 8 18 sylibr ⊢H∈Sℋ→W∈SubSp⁡U