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 × H norm H
Assertion hhsst H S W SubSp U

Proof

Step Hyp Ref Expression
1 hhsst.1 U = + norm
2 hhsst.2 W = + H × H × H norm 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 = norm CV U
15 2 hhssnm norm H = norm CV 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