Metamath Proof Explorer

Theorem hhshsslem2

Description: Lemma for hhsssh . (Contributed by NM, 6-Apr-2008) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 hhsst.1 ⊢U=+ℎ⋅ℎnormℎ
2 hhsst.2 ⊢W=+ℎ↾H×H⋅ℎ↾ℂ×Hnormℎ↾H
3 hhssp3.3 ⊢W∈SubSp⁡U
4 hhssp3.4 ⊢H⊆ℋ
5 1 hhnv ⊢U∈NrmCVec
6 1 hh0v ⊢0ℎ=0vec⁡U
7 eqid ⊢0vec⁡W=0vec⁡W
8 eqid ⊢SubSp⁡U=SubSp⁡U
9 6 7 8 sspz ⊢U∈NrmCVec∧W∈SubSp⁡U→0vec⁡W=0ℎ
10 5 3 9 mp2an ⊢0vec⁡W=0ℎ
11 8 sspnv ⊢U∈NrmCVec∧W∈SubSp⁡U→W∈NrmCVec
12 5 3 11 mp2an ⊢W∈NrmCVec
13 eqid ⊢BaseSet⁡W=BaseSet⁡W
14 13 7 nvzcl ⊢W∈NrmCVec→0vec⁡W∈BaseSet⁡W
15 12 14 ax-mp ⊢0vec⁡W∈BaseSet⁡W
16 1 2 3 4 hhshsslem1 ⊢H=BaseSet⁡W
17 15 16 eleqtrri ⊢0vec⁡W∈H
18 10 17 eqeltrri ⊢0ℎ∈H
19 4 18 pm3.2i ⊢H⊆ℋ∧0ℎ∈H
20 1 hhva ⊢+ℎ=+v⁡U
21 eqid ⊢+v⁡W=+v⁡W
22 16 20 21 8 sspgval ⊢U∈NrmCVec∧W∈SubSp⁡U∧x∈H∧y∈H→x+v⁡Wy=x+ℎy
23 5 3 22 mpanl12 ⊢x∈H∧y∈H→x+v⁡Wy=x+ℎy
24 16 21 nvgcl ⊢W∈NrmCVec∧x∈H∧y∈H→x+v⁡Wy∈H
25 12 24 mp3an1 ⊢x∈H∧y∈H→x+v⁡Wy∈H
26 23 25 eqeltrrd ⊢x∈H∧y∈H→x+ℎy∈H
27 26 rgen2 ⊢∀x∈H∀y∈Hx+ℎy∈H
28 1 hhsm ⊢⋅ℎ=⋅𝑠OLD⁡U
29 eqid ⊢⋅𝑠OLD⁡W=⋅𝑠OLD⁡W
30 16 28 29 8 sspsval ⊢U∈NrmCVec∧W∈SubSp⁡U∧x∈ℂ∧y∈H→x⋅𝑠OLD⁡Wy=x⋅ℎy
31 5 3 30 mpanl12 ⊢x∈ℂ∧y∈H→x⋅𝑠OLD⁡Wy=x⋅ℎy
32 16 29 nvscl ⊢W∈NrmCVec∧x∈ℂ∧y∈H→x⋅𝑠OLD⁡Wy∈H
33 12 32 mp3an1 ⊢x∈ℂ∧y∈H→x⋅𝑠OLD⁡Wy∈H
34 31 33 eqeltrrd ⊢x∈ℂ∧y∈H→x⋅ℎy∈H
35 34 rgen2 ⊢∀x∈ℂ∀y∈Hx⋅ℎy∈H
36 27 35 pm3.2i ⊢∀x∈H∀y∈Hx+ℎy∈H∧∀x∈ℂ∀y∈Hx⋅ℎy∈H
37 issh2 ⊢H∈Sℋ↔H⊆ℋ∧0ℎ∈H∧∀x∈H∀y∈Hx+ℎy∈H∧∀x∈ℂ∀y∈Hx⋅ℎy∈H
38 19 36 37 mpbir2an ⊢H∈Sℋ