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