Proof of Theorem hhshsslem1
Step | Hyp | Ref
| Expression |
1 | | eqid 2826 |
. . . 4
⊢
(BaseSet‘𝑊) =
(BaseSet‘𝑊) |
2 | | eqid 2826 |
. . . 4
⊢ (
+𝑣 ‘𝑊) = ( +𝑣 ‘𝑊) |
3 | 1, 2 | bafval 28015 |
. . 3
⊢
(BaseSet‘𝑊) =
ran ( +𝑣 ‘𝑊) |
4 | | hhsst.1 |
. . . . . . 7
⊢ 𝑈 = 〈〈
+ℎ , ·ℎ 〉,
normℎ〉 |
5 | 4 | hhnv 28578 |
. . . . . 6
⊢ 𝑈 ∈ NrmCVec |
6 | | hhssp3.3 |
. . . . . 6
⊢ 𝑊 ∈ (SubSp‘𝑈) |
7 | | eqid 2826 |
. . . . . . 7
⊢
(SubSp‘𝑈) =
(SubSp‘𝑈) |
8 | 7 | sspnv 28137 |
. . . . . 6
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ (SubSp‘𝑈)) → 𝑊 ∈ NrmCVec) |
9 | 5, 6, 8 | mp2an 685 |
. . . . 5
⊢ 𝑊 ∈ NrmCVec |
10 | 2 | nvgrp 28028 |
. . . . 5
⊢ (𝑊 ∈ NrmCVec → (
+𝑣 ‘𝑊) ∈ GrpOp) |
11 | | grporndm 27921 |
. . . . 5
⊢ ((
+𝑣 ‘𝑊) ∈ GrpOp → ran (
+𝑣 ‘𝑊) = dom dom ( +𝑣
‘𝑊)) |
12 | 9, 10, 11 | mp2b 10 |
. . . 4
⊢ ran (
+𝑣 ‘𝑊) = dom dom ( +𝑣
‘𝑊) |
13 | | hhsst.2 |
. . . . . . . . . 10
⊢ 𝑊 = 〈〈(
+ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ
↾ (ℂ × 𝐻))〉, (normℎ ↾
𝐻)〉 |
14 | 13 | fveq2i 6437 |
. . . . . . . . 9
⊢ (
+𝑣 ‘𝑊) = ( +𝑣
‘〈〈( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ
↾ (ℂ × 𝐻))〉, (normℎ ↾
𝐻)〉) |
15 | | eqid 2826 |
. . . . . . . . . . 11
⊢ (
+𝑣 ‘〈〈( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ
↾ (ℂ × 𝐻))〉, (normℎ ↾
𝐻)〉) = (
+𝑣 ‘〈〈( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ
↾ (ℂ × 𝐻))〉, (normℎ ↾
𝐻)〉) |
16 | 15 | vafval 28014 |
. . . . . . . . . 10
⊢ (
+𝑣 ‘〈〈( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ
↾ (ℂ × 𝐻))〉, (normℎ ↾
𝐻)〉) = (1st
‘(1st ‘〈〈( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ
↾ (ℂ × 𝐻))〉, (normℎ ↾
𝐻)〉)) |
17 | | opex 5154 |
. . . . . . . . . . . . 13
⊢ 〈(
+ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ
↾ (ℂ × 𝐻))〉 ∈ V |
18 | | normf 28536 |
. . . . . . . . . . . . . . 15
⊢
normℎ: ℋ⟶ℝ |
19 | | ax-hilex 28412 |
. . . . . . . . . . . . . . 15
⊢ ℋ
∈ V |
20 | | fex 6746 |
. . . . . . . . . . . . . . 15
⊢
((normℎ: ℋ⟶ℝ ∧ ℋ ∈
V) → normℎ ∈ V) |
21 | 18, 19, 20 | mp2an 685 |
. . . . . . . . . . . . . 14
⊢
normℎ ∈ V |
22 | 21 | resex 5681 |
. . . . . . . . . . . . 13
⊢
(normℎ ↾ 𝐻) ∈ V |
23 | 17, 22 | op1st 7437 |
. . . . . . . . . . . 12
⊢
(1st ‘〈〈( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ
↾ (ℂ × 𝐻))〉, (normℎ ↾
𝐻)〉) = 〈(
+ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ
↾ (ℂ × 𝐻))〉 |
24 | 23 | fveq2i 6437 |
. . . . . . . . . . 11
⊢
(1st ‘(1st ‘〈〈(
+ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ
↾ (ℂ × 𝐻))〉, (normℎ ↾
𝐻)〉)) =
(1st ‘〈( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ
↾ (ℂ × 𝐻))〉) |
25 | | hilablo 28573 |
. . . . . . . . . . . . 13
⊢
+ℎ ∈ AbelOp |
26 | | resexg 5680 |
. . . . . . . . . . . . 13
⊢ (
+ℎ ∈ AbelOp → ( +ℎ ↾ (𝐻 × 𝐻)) ∈ V) |
27 | 25, 26 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ (
+ℎ ↾ (𝐻 × 𝐻)) ∈ V |
28 | | hvmulex 28424 |
. . . . . . . . . . . . 13
⊢
·ℎ ∈ V |
29 | 28 | resex 5681 |
. . . . . . . . . . . 12
⊢ (
·ℎ ↾ (ℂ × 𝐻)) ∈ V |
30 | 27, 29 | op1st 7437 |
. . . . . . . . . . 11
⊢
(1st ‘〈( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ
↾ (ℂ × 𝐻))〉) = ( +ℎ ↾
(𝐻 × 𝐻)) |
31 | 24, 30 | eqtri 2850 |
. . . . . . . . . 10
⊢
(1st ‘(1st ‘〈〈(
+ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ
↾ (ℂ × 𝐻))〉, (normℎ ↾
𝐻)〉)) = (
+ℎ ↾ (𝐻 × 𝐻)) |
32 | 16, 31 | eqtri 2850 |
. . . . . . . . 9
⊢ (
+𝑣 ‘〈〈( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ
↾ (ℂ × 𝐻))〉, (normℎ ↾
𝐻)〉) = (
+ℎ ↾ (𝐻 × 𝐻)) |
33 | 14, 32 | eqtri 2850 |
. . . . . . . 8
⊢ (
+𝑣 ‘𝑊) = ( +ℎ ↾ (𝐻 × 𝐻)) |
34 | 33 | dmeqi 5558 |
. . . . . . 7
⊢ dom (
+𝑣 ‘𝑊) = dom ( +ℎ ↾
(𝐻 × 𝐻)) |
35 | | hhssp3.4 |
. . . . . . . . . 10
⊢ 𝐻 ⊆
ℋ |
36 | | xpss12 5358 |
. . . . . . . . . 10
⊢ ((𝐻 ⊆ ℋ ∧ 𝐻 ⊆ ℋ) → (𝐻 × 𝐻) ⊆ ( ℋ ×
ℋ)) |
37 | 35, 35, 36 | mp2an 685 |
. . . . . . . . 9
⊢ (𝐻 × 𝐻) ⊆ ( ℋ ×
ℋ) |
38 | | ax-hfvadd 28413 |
. . . . . . . . . 10
⊢
+ℎ :( ℋ × ℋ)⟶
ℋ |
39 | 38 | fdmi 6289 |
. . . . . . . . 9
⊢ dom
+ℎ = ( ℋ × ℋ) |
40 | 37, 39 | sseqtr4i 3864 |
. . . . . . . 8
⊢ (𝐻 × 𝐻) ⊆ dom
+ℎ |
41 | | ssdmres 5657 |
. . . . . . . 8
⊢ ((𝐻 × 𝐻) ⊆ dom +ℎ ↔
dom ( +ℎ ↾ (𝐻 × 𝐻)) = (𝐻 × 𝐻)) |
42 | 40, 41 | mpbi 222 |
. . . . . . 7
⊢ dom (
+ℎ ↾ (𝐻 × 𝐻)) = (𝐻 × 𝐻) |
43 | 34, 42 | eqtri 2850 |
. . . . . 6
⊢ dom (
+𝑣 ‘𝑊) = (𝐻 × 𝐻) |
44 | 43 | dmeqi 5558 |
. . . . 5
⊢ dom dom (
+𝑣 ‘𝑊) = dom (𝐻 × 𝐻) |
45 | | dmxpid 5578 |
. . . . 5
⊢ dom
(𝐻 × 𝐻) = 𝐻 |
46 | 44, 45 | eqtri 2850 |
. . . 4
⊢ dom dom (
+𝑣 ‘𝑊) = 𝐻 |
47 | 12, 46 | eqtri 2850 |
. . 3
⊢ ran (
+𝑣 ‘𝑊) = 𝐻 |
48 | 3, 47 | eqtri 2850 |
. 2
⊢
(BaseSet‘𝑊) =
𝐻 |
49 | 48 | eqcomi 2835 |
1
⊢ 𝐻 = (BaseSet‘𝑊) |