Metamath Proof Explorer

Theorem hhshsslem2

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

Ref Expression
Hypotheses hhsst.1 ⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
hhsst.2 ⊢ 𝑊 = ⟨ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ , ( normℎ ↾ 𝐻 ) ⟩
hhssp3.3 ⊢ 𝑊 ∈ ( SubSp ‘ 𝑈 )
hhssp3.4 ⊢ 𝐻 ⊆ ℋ
Assertion hhshsslem2 𝐻 ∈ Sℋ

Proof

Step Hyp Ref Expression
1 hhsst.1 ⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
2 hhsst.2 ⊢ 𝑊 = ⟨ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ , ( normℎ ↾ 𝐻 ) ⟩
3 hhssp3.3 ⊢ 𝑊 ∈ ( SubSp ‘ 𝑈 )
4 hhssp3.4 ⊢ 𝐻 ⊆ ℋ
5 1 hhnv ⊢ 𝑈 ∈ NrmCVec
6 1 hh0v ⊢ 0ℎ = ( 0vec ‘ 𝑈 )
7 eqid ⊢ ( 0vec ‘ 𝑊 ) = ( 0vec ‘ 𝑊 )
8 eqid ⊢ ( SubSp ‘ 𝑈 ) = ( SubSp ‘ 𝑈 )
9 6 7 8 sspz ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ ( SubSp ‘ 𝑈 ) ) → ( 0vec ‘ 𝑊 ) = 0ℎ )
10 5 3 9 mp2an ⊢ ( 0vec ‘ 𝑊 ) = 0ℎ
11 8 sspnv ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ ( SubSp ‘ 𝑈 ) ) → 𝑊 ∈ NrmCVec )
12 5 3 11 mp2an ⊢ 𝑊 ∈ NrmCVec
13 eqid ⊢ ( BaseSet ‘ 𝑊 ) = ( BaseSet ‘ 𝑊 )
14 13 7 nvzcl ⊢ ( 𝑊 ∈ NrmCVec → ( 0vec ‘ 𝑊 ) ∈ ( BaseSet ‘ 𝑊 ) )
15 12 14 ax-mp ⊢ ( 0vec ‘ 𝑊 ) ∈ ( BaseSet ‘ 𝑊 )
16 1 2 3 4 hhshsslem1 ⊢ 𝐻 = ( BaseSet ‘ 𝑊 )
17 15 16 eleqtrri ⊢ ( 0vec ‘ 𝑊 ) ∈ 𝐻
18 10 17 eqeltrri ⊢ 0ℎ ∈ 𝐻
19 4 18 pm3.2i ⊢ ( 𝐻 ⊆ ℋ ∧ 0ℎ ∈ 𝐻 )
20 1 hhva ⊢ +ℎ = ( +𝑣 ‘ 𝑈 )
21 eqid ⊢ ( +𝑣 ‘ 𝑊 ) = ( +𝑣 ‘ 𝑊 )
22 16 20 21 8 sspgval ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ ( SubSp ‘ 𝑈 ) ) ∧ ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ) ) → ( 𝑥 ( +𝑣 ‘ 𝑊 ) 𝑦 ) = ( 𝑥 +ℎ 𝑦 ) )
23 5 3 22 mpanl12 ⊢ ( ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ) → ( 𝑥 ( +𝑣 ‘ 𝑊 ) 𝑦 ) = ( 𝑥 +ℎ 𝑦 ) )
24 16 21 nvgcl ⊢ ( ( 𝑊 ∈ NrmCVec ∧ 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ) → ( 𝑥 ( +𝑣 ‘ 𝑊 ) 𝑦 ) ∈ 𝐻 )
25 12 24 mp3an1 ⊢ ( ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ) → ( 𝑥 ( +𝑣 ‘ 𝑊 ) 𝑦 ) ∈ 𝐻 )
26 23 25 eqeltrrd ⊢ ( ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ) → ( 𝑥 +ℎ 𝑦 ) ∈ 𝐻 )
27 26 rgen2 ⊢ ∀ 𝑥 ∈ 𝐻 ∀ 𝑦 ∈ 𝐻 ( 𝑥 +ℎ 𝑦 ) ∈ 𝐻
28 1 hhsm ⊢ ·ℎ = ( ·𝑠OLD ‘ 𝑈 )
29 eqid ⊢ ( ·𝑠OLD ‘ 𝑊 ) = ( ·𝑠OLD ‘ 𝑊 )
30 16 28 29 8 sspsval ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ ( SubSp ‘ 𝑈 ) ) ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝐻 ) ) → ( 𝑥 ( ·𝑠OLD ‘ 𝑊 ) 𝑦 ) = ( 𝑥 ·ℎ 𝑦 ) )
31 5 3 30 mpanl12 ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝐻 ) → ( 𝑥 ( ·𝑠OLD ‘ 𝑊 ) 𝑦 ) = ( 𝑥 ·ℎ 𝑦 ) )
32 16 29 nvscl ⊢ ( ( 𝑊 ∈ NrmCVec ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝐻 ) → ( 𝑥 ( ·𝑠OLD ‘ 𝑊 ) 𝑦 ) ∈ 𝐻 )
33 12 32 mp3an1 ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝐻 ) → ( 𝑥 ( ·𝑠OLD ‘ 𝑊 ) 𝑦 ) ∈ 𝐻 )
34 31 33 eqeltrrd ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝐻 ) → ( 𝑥 ·ℎ 𝑦 ) ∈ 𝐻 )
35 34 rgen2 ⊢ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ 𝐻 ( 𝑥 ·ℎ 𝑦 ) ∈ 𝐻
36 27 35 pm3.2i ⊢ ( ∀ 𝑥 ∈ 𝐻 ∀ 𝑦 ∈ 𝐻 ( 𝑥 +ℎ 𝑦 ) ∈ 𝐻 ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ 𝐻 ( 𝑥 ·ℎ 𝑦 ) ∈ 𝐻 )
37 issh2 ⊢ ( 𝐻 ∈ Sℋ ↔ ( ( 𝐻 ⊆ ℋ ∧ 0ℎ ∈ 𝐻 ) ∧ ( ∀ 𝑥 ∈ 𝐻 ∀ 𝑦 ∈ 𝐻 ( 𝑥 +ℎ 𝑦 ) ∈ 𝐻 ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ 𝐻 ( 𝑥 ·ℎ 𝑦 ) ∈ 𝐻 ) ) )
38 19 36 37 mpbir2an ⊢ 𝐻 ∈ Sℋ