Proof of Theorem hhshsslem1
| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . . 4
⊢
(BaseSet‘𝑊) =
(BaseSet‘𝑊) |
| 2 | | eqid 2737 |
. . . 4
⊢ (
+𝑣 ‘𝑊) = ( +𝑣 ‘𝑊) |
| 3 | 1, 2 | bafval 30623 |
. . 3
⊢
(BaseSet‘𝑊) =
ran ( +𝑣 ‘𝑊) |
| 4 | | hhsst.1 |
. . . . . . 7
⊢ 𝑈 = 〈〈
+ℎ , ·ℎ 〉,
normℎ〉 |
| 5 | 4 | hhnv 31184 |
. . . . . 6
⊢ 𝑈 ∈ NrmCVec |
| 6 | | hhssp3.3 |
. . . . . 6
⊢ 𝑊 ∈ (SubSp‘𝑈) |
| 7 | | eqid 2737 |
. . . . . . 7
⊢
(SubSp‘𝑈) =
(SubSp‘𝑈) |
| 8 | 7 | sspnv 30745 |
. . . . . 6
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ (SubSp‘𝑈)) → 𝑊 ∈ NrmCVec) |
| 9 | 5, 6, 8 | mp2an 692 |
. . . . 5
⊢ 𝑊 ∈ NrmCVec |
| 10 | 2 | nvgrp 30636 |
. . . . 5
⊢ (𝑊 ∈ NrmCVec → (
+𝑣 ‘𝑊) ∈ GrpOp) |
| 11 | | grporndm 30529 |
. . . . 5
⊢ ((
+𝑣 ‘𝑊) ∈ GrpOp → ran (
+𝑣 ‘𝑊) = dom dom ( +𝑣
‘𝑊)) |
| 12 | 9, 10, 11 | mp2b 10 |
. . . 4
⊢ ran (
+𝑣 ‘𝑊) = dom dom ( +𝑣
‘𝑊) |
| 13 | | hhsst.2 |
. . . . . . . . . 10
⊢ 𝑊 = 〈〈(
+ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ
↾ (ℂ × 𝐻))〉, (normℎ ↾
𝐻)〉 |
| 14 | 13 | fveq2i 6909 |
. . . . . . . . 9
⊢ (
+𝑣 ‘𝑊) = ( +𝑣
‘〈〈( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ
↾ (ℂ × 𝐻))〉, (normℎ ↾
𝐻)〉) |
| 15 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (
+𝑣 ‘〈〈( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ
↾ (ℂ × 𝐻))〉, (normℎ ↾
𝐻)〉) = (
+𝑣 ‘〈〈( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ
↾ (ℂ × 𝐻))〉, (normℎ ↾
𝐻)〉) |
| 16 | 15 | vafval 30622 |
. . . . . . . . . 10
⊢ (
+𝑣 ‘〈〈( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ
↾ (ℂ × 𝐻))〉, (normℎ ↾
𝐻)〉) = (1st
‘(1st ‘〈〈( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ
↾ (ℂ × 𝐻))〉, (normℎ ↾
𝐻)〉)) |
| 17 | | opex 5469 |
. . . . . . . . . . . . 13
⊢ 〈(
+ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ
↾ (ℂ × 𝐻))〉 ∈ V |
| 18 | | normf 31142 |
. . . . . . . . . . . . . . 15
⊢
normℎ: ℋ⟶ℝ |
| 19 | | ax-hilex 31018 |
. . . . . . . . . . . . . . 15
⊢ ℋ
∈ V |
| 20 | | fex 7246 |
. . . . . . . . . . . . . . 15
⊢
((normℎ: ℋ⟶ℝ ∧ ℋ ∈
V) → normℎ ∈ V) |
| 21 | 18, 19, 20 | mp2an 692 |
. . . . . . . . . . . . . 14
⊢
normℎ ∈ V |
| 22 | 21 | resex 6047 |
. . . . . . . . . . . . 13
⊢
(normℎ ↾ 𝐻) ∈ V |
| 23 | 17, 22 | op1st 8022 |
. . . . . . . . . . . 12
⊢
(1st ‘〈〈( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ
↾ (ℂ × 𝐻))〉, (normℎ ↾
𝐻)〉) = 〈(
+ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ
↾ (ℂ × 𝐻))〉 |
| 24 | 23 | fveq2i 6909 |
. . . . . . . . . . 11
⊢
(1st ‘(1st ‘〈〈(
+ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ
↾ (ℂ × 𝐻))〉, (normℎ ↾
𝐻)〉)) =
(1st ‘〈( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ
↾ (ℂ × 𝐻))〉) |
| 25 | | hilablo 31179 |
. . . . . . . . . . . . 13
⊢
+ℎ ∈ AbelOp |
| 26 | | resexg 6045 |
. . . . . . . . . . . . 13
⊢ (
+ℎ ∈ AbelOp → ( +ℎ ↾ (𝐻 × 𝐻)) ∈ V) |
| 27 | 25, 26 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ (
+ℎ ↾ (𝐻 × 𝐻)) ∈ V |
| 28 | | hvmulex 31030 |
. . . . . . . . . . . . 13
⊢
·ℎ ∈ V |
| 29 | 28 | resex 6047 |
. . . . . . . . . . . 12
⊢ (
·ℎ ↾ (ℂ × 𝐻)) ∈ V |
| 30 | 27, 29 | op1st 8022 |
. . . . . . . . . . 11
⊢
(1st ‘〈( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ
↾ (ℂ × 𝐻))〉) = ( +ℎ ↾
(𝐻 × 𝐻)) |
| 31 | 24, 30 | eqtri 2765 |
. . . . . . . . . 10
⊢
(1st ‘(1st ‘〈〈(
+ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ
↾ (ℂ × 𝐻))〉, (normℎ ↾
𝐻)〉)) = (
+ℎ ↾ (𝐻 × 𝐻)) |
| 32 | 16, 31 | eqtri 2765 |
. . . . . . . . 9
⊢ (
+𝑣 ‘〈〈( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ
↾ (ℂ × 𝐻))〉, (normℎ ↾
𝐻)〉) = (
+ℎ ↾ (𝐻 × 𝐻)) |
| 33 | 14, 32 | eqtri 2765 |
. . . . . . . 8
⊢ (
+𝑣 ‘𝑊) = ( +ℎ ↾ (𝐻 × 𝐻)) |
| 34 | 33 | dmeqi 5915 |
. . . . . . 7
⊢ dom (
+𝑣 ‘𝑊) = dom ( +ℎ ↾
(𝐻 × 𝐻)) |
| 35 | | hhssp3.4 |
. . . . . . . . . 10
⊢ 𝐻 ⊆
ℋ |
| 36 | | xpss12 5700 |
. . . . . . . . . 10
⊢ ((𝐻 ⊆ ℋ ∧ 𝐻 ⊆ ℋ) → (𝐻 × 𝐻) ⊆ ( ℋ ×
ℋ)) |
| 37 | 35, 35, 36 | mp2an 692 |
. . . . . . . . 9
⊢ (𝐻 × 𝐻) ⊆ ( ℋ ×
ℋ) |
| 38 | | ax-hfvadd 31019 |
. . . . . . . . . 10
⊢
+ℎ :( ℋ × ℋ)⟶
ℋ |
| 39 | 38 | fdmi 6747 |
. . . . . . . . 9
⊢ dom
+ℎ = ( ℋ × ℋ) |
| 40 | 37, 39 | sseqtrri 4033 |
. . . . . . . 8
⊢ (𝐻 × 𝐻) ⊆ dom
+ℎ |
| 41 | | ssdmres 6031 |
. . . . . . . 8
⊢ ((𝐻 × 𝐻) ⊆ dom +ℎ ↔
dom ( +ℎ ↾ (𝐻 × 𝐻)) = (𝐻 × 𝐻)) |
| 42 | 40, 41 | mpbi 230 |
. . . . . . 7
⊢ dom (
+ℎ ↾ (𝐻 × 𝐻)) = (𝐻 × 𝐻) |
| 43 | 34, 42 | eqtri 2765 |
. . . . . 6
⊢ dom (
+𝑣 ‘𝑊) = (𝐻 × 𝐻) |
| 44 | 43 | dmeqi 5915 |
. . . . 5
⊢ dom dom (
+𝑣 ‘𝑊) = dom (𝐻 × 𝐻) |
| 45 | | dmxpid 5941 |
. . . . 5
⊢ dom
(𝐻 × 𝐻) = 𝐻 |
| 46 | 44, 45 | eqtri 2765 |
. . . 4
⊢ dom dom (
+𝑣 ‘𝑊) = 𝐻 |
| 47 | 12, 46 | eqtri 2765 |
. . 3
⊢ ran (
+𝑣 ‘𝑊) = 𝐻 |
| 48 | 3, 47 | eqtri 2765 |
. 2
⊢
(BaseSet‘𝑊) =
𝐻 |
| 49 | 48 | eqcomi 2746 |
1
⊢ 𝐻 = (BaseSet‘𝑊) |