Metamath Proof Explorer

Theorem hhshsslem1

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

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

Proof

Step Hyp Ref Expression
1 hhsst.1 ⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
2 hhsst.2 ⊢ 𝑊 = ⟨ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ , ( normℎ ↾ 𝐻 ) ⟩
3 hhssp3.3 ⊢ 𝑊 ∈ ( SubSp ‘ 𝑈 )
4 hhssp3.4 ⊢ 𝐻 ⊆ ℋ
5 eqid ⊢ ( BaseSet ‘ 𝑊 ) = ( BaseSet ‘ 𝑊 )
6 eqid ⊢ ( +𝑣 ‘ 𝑊 ) = ( +𝑣 ‘ 𝑊 )
7 5 6 bafval ⊢ ( BaseSet ‘ 𝑊 ) = ran ( +𝑣 ‘ 𝑊 )
8 1 hhnv ⊢ 𝑈 ∈ NrmCVec
9 eqid ⊢ ( SubSp ‘ 𝑈 ) = ( SubSp ‘ 𝑈 )
10 9 sspnv ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ ( SubSp ‘ 𝑈 ) ) → 𝑊 ∈ NrmCVec )
11 8 3 10 mp2an ⊢ 𝑊 ∈ NrmCVec
12 6 nvgrp ⊢ ( 𝑊 ∈ NrmCVec → ( +𝑣 ‘ 𝑊 ) ∈ GrpOp )
13 grporndm ⊢ ( ( +𝑣 ‘ 𝑊 ) ∈ GrpOp → ran ( +𝑣 ‘ 𝑊 ) = dom dom ( +𝑣 ‘ 𝑊 ) )
14 11 12 13 mp2b ⊢ ran ( +𝑣 ‘ 𝑊 ) = dom dom ( +𝑣 ‘ 𝑊 )
15 2 fveq2i ⊢ ( +𝑣 ‘ 𝑊 ) = ( +𝑣 ‘ ⟨ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ , ( normℎ ↾ 𝐻 ) ⟩ )
16 eqid ⊢ ( +𝑣 ‘ ⟨ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ , ( normℎ ↾ 𝐻 ) ⟩ ) = ( +𝑣 ‘ ⟨ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ , ( normℎ ↾ 𝐻 ) ⟩ )
17 16 vafval ⊢ ( +𝑣 ‘ ⟨ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ , ( normℎ ↾ 𝐻 ) ⟩ ) = ( 1st ‘ ( 1st ‘ ⟨ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ , ( normℎ ↾ 𝐻 ) ⟩ ) )
18 opex ⊢ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ ∈ V
19 normf ⊢ normℎ : ℋ ⟶ ℝ
20 ax-hilex ⊢ ℋ ∈ V
21 fex ⊢ ( ( normℎ : ℋ ⟶ ℝ ∧ ℋ ∈ V ) → normℎ ∈ V )
22 19 20 21 mp2an ⊢ normℎ ∈ V
23 22 resex ⊢ ( normℎ ↾ 𝐻 ) ∈ V
24 18 23 op1st ⊢ ( 1st ‘ ⟨ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ , ( normℎ ↾ 𝐻 ) ⟩ ) = ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩
25 24 fveq2i ⊢ ( 1st ‘ ( 1st ‘ ⟨ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ , ( normℎ ↾ 𝐻 ) ⟩ ) ) = ( 1st ‘ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ )
26 hilablo ⊢ +ℎ ∈ AbelOp
27 resexg ⊢ ( +ℎ ∈ AbelOp → ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) ∈ V )
28 26 27 ax-mp ⊢ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) ∈ V
29 hvmulex ⊢ ·ℎ ∈ V
30 29 resex ⊢ ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ∈ V
31 28 30 op1st ⊢ ( 1st ‘ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ ) = ( +ℎ ↾ ( 𝐻 × 𝐻 ) )
32 25 31 eqtri ⊢ ( 1st ‘ ( 1st ‘ ⟨ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ , ( normℎ ↾ 𝐻 ) ⟩ ) ) = ( +ℎ ↾ ( 𝐻 × 𝐻 ) )
33 17 32 eqtri ⊢ ( +𝑣 ‘ ⟨ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ , ( normℎ ↾ 𝐻 ) ⟩ ) = ( +ℎ ↾ ( 𝐻 × 𝐻 ) )
34 15 33 eqtri ⊢ ( +𝑣 ‘ 𝑊 ) = ( +ℎ ↾ ( 𝐻 × 𝐻 ) )
35 34 dmeqi ⊢ dom ( +𝑣 ‘ 𝑊 ) = dom ( +ℎ ↾ ( 𝐻 × 𝐻 ) )
36 xpss12 ⊢ ( ( 𝐻 ⊆ ℋ ∧ 𝐻 ⊆ ℋ ) → ( 𝐻 × 𝐻 ) ⊆ ( ℋ × ℋ ) )
37 4 4 36 mp2an ⊢ ( 𝐻 × 𝐻 ) ⊆ ( ℋ × ℋ )
38 ax-hfvadd ⊢ +ℎ : ( ℋ × ℋ ) ⟶ ℋ
39 38 fdmi ⊢ dom +ℎ = ( ℋ × ℋ )
40 37 39 sseqtrri ⊢ ( 𝐻 × 𝐻 ) ⊆ dom +ℎ
41 ssdmres ⊢ ( ( 𝐻 × 𝐻 ) ⊆ dom +ℎ ↔ dom ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) = ( 𝐻 × 𝐻 ) )
42 40 41 mpbi ⊢ dom ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) = ( 𝐻 × 𝐻 )
43 35 42 eqtri ⊢ dom ( +𝑣 ‘ 𝑊 ) = ( 𝐻 × 𝐻 )
44 43 dmeqi ⊢ dom dom ( +𝑣 ‘ 𝑊 ) = dom ( 𝐻 × 𝐻 )
45 dmxpid ⊢ dom ( 𝐻 × 𝐻 ) = 𝐻
46 44 45 eqtri ⊢ dom dom ( +𝑣 ‘ 𝑊 ) = 𝐻
47 14 46 eqtri ⊢ ran ( +𝑣 ‘ 𝑊 ) = 𝐻
48 7 47 eqtri ⊢ ( BaseSet ‘ 𝑊 ) = 𝐻
49 48 eqcomi ⊢ 𝐻 = ( BaseSet ‘ 𝑊 )