Proof of Theorem hhsssh
| Step | Hyp | Ref
| Expression |
| 1 | | hhsst.1 |
. . . 4
⊢ 𝑈 = 〈〈
+ℎ , ·ℎ 〉,
normℎ〉 |
| 2 | | hhsst.2 |
. . . 4
⊢ 𝑊 = 〈〈(
+ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ
↾ (ℂ × 𝐻))〉, (normℎ ↾
𝐻)〉 |
| 3 | 1, 2 | hhsst 31285 |
. . 3
⊢ (𝐻 ∈
Sℋ → 𝑊 ∈ (SubSp‘𝑈)) |
| 4 | | shss 31229 |
. . 3
⊢ (𝐻 ∈
Sℋ → 𝐻 ⊆ ℋ) |
| 5 | 3, 4 | jca 511 |
. 2
⊢ (𝐻 ∈
Sℋ → (𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ)) |
| 6 | | eleq1 2829 |
. . 3
⊢ (𝐻 = if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) → (𝐻 ∈ Sℋ
↔ if((𝑊 ∈
(SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) ∈
Sℋ )) |
| 7 | | eqid 2737 |
. . . 4
⊢
〈〈( +ℎ ↾ (if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ))), (
·ℎ ↾ (ℂ × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ)))〉, (normℎ
↾ if((𝑊 ∈
(SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ))〉 =
〈〈( +ℎ ↾ (if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ))), (
·ℎ ↾ (ℂ × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ)))〉, (normℎ
↾ if((𝑊 ∈
(SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻,
ℋ))〉 |
| 8 | | xpeq1 5699 |
. . . . . . . . . . . . 13
⊢ (𝐻 = if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) → (𝐻 × 𝐻) = (if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) × 𝐻)) |
| 9 | | xpeq2 5706 |
. . . . . . . . . . . . 13
⊢ (𝐻 = if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) → (if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) × 𝐻) = (if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ))) |
| 10 | 8, 9 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ (𝐻 = if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) → (𝐻 × 𝐻) = (if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ))) |
| 11 | 10 | reseq2d 5997 |
. . . . . . . . . . 11
⊢ (𝐻 = if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) → ( +ℎ
↾ (𝐻 × 𝐻)) = ( +ℎ
↾ (if((𝑊 ∈
(SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ)))) |
| 12 | | xpeq2 5706 |
. . . . . . . . . . . 12
⊢ (𝐻 = if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) → (ℂ × 𝐻) = (ℂ × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ))) |
| 13 | 12 | reseq2d 5997 |
. . . . . . . . . . 11
⊢ (𝐻 = if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) → (
·ℎ ↾ (ℂ × 𝐻)) = ( ·ℎ
↾ (ℂ × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ)))) |
| 14 | 11, 13 | opeq12d 4881 |
. . . . . . . . . 10
⊢ (𝐻 = if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) → 〈(
+ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ
↾ (ℂ × 𝐻))〉 = 〈( +ℎ
↾ (if((𝑊 ∈
(SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ))), (
·ℎ ↾ (ℂ × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ)))〉) |
| 15 | | reseq2 5992 |
. . . . . . . . . 10
⊢ (𝐻 = if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) → (normℎ
↾ 𝐻) =
(normℎ ↾ if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ))) |
| 16 | 14, 15 | opeq12d 4881 |
. . . . . . . . 9
⊢ (𝐻 = if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) → 〈〈(
+ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ
↾ (ℂ × 𝐻))〉, (normℎ ↾
𝐻)〉 = 〈〈(
+ℎ ↾ (if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ))), (
·ℎ ↾ (ℂ × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ)))〉, (normℎ
↾ if((𝑊 ∈
(SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻,
ℋ))〉) |
| 17 | 2, 16 | eqtrid 2789 |
. . . . . . . 8
⊢ (𝐻 = if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) → 𝑊 = 〈〈( +ℎ
↾ (if((𝑊 ∈
(SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ))), (
·ℎ ↾ (ℂ × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ)))〉, (normℎ
↾ if((𝑊 ∈
(SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻,
ℋ))〉) |
| 18 | 17 | eleq1d 2826 |
. . . . . . 7
⊢ (𝐻 = if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) → (𝑊 ∈ (SubSp‘𝑈) ↔ 〈〈( +ℎ
↾ (if((𝑊 ∈
(SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ))), (
·ℎ ↾ (ℂ × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ)))〉, (normℎ
↾ if((𝑊 ∈
(SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ))〉 ∈
(SubSp‘𝑈))) |
| 19 | | sseq1 4009 |
. . . . . . 7
⊢ (𝐻 = if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) → (𝐻 ⊆ ℋ ↔ if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) ⊆
ℋ)) |
| 20 | 18, 19 | anbi12d 632 |
. . . . . 6
⊢ (𝐻 = if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) → ((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ) ↔ (〈〈(
+ℎ ↾ (if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ))), (
·ℎ ↾ (ℂ × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ)))〉, (normℎ
↾ if((𝑊 ∈
(SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ))〉 ∈
(SubSp‘𝑈) ∧
if((𝑊 ∈
(SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) ⊆
ℋ))) |
| 21 | | xpeq1 5699 |
. . . . . . . . . . . 12
⊢ ( ℋ
= if((𝑊 ∈
(SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) → ( ℋ
× ℋ) = (if((𝑊
∈ (SubSp‘𝑈)
∧ 𝐻 ⊆ ℋ),
𝐻, ℋ) ×
ℋ)) |
| 22 | | xpeq2 5706 |
. . . . . . . . . . . 12
⊢ ( ℋ
= if((𝑊 ∈
(SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) → (if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) × ℋ) = (if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ))) |
| 23 | 21, 22 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ ( ℋ
= if((𝑊 ∈
(SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) → ( ℋ
× ℋ) = (if((𝑊
∈ (SubSp‘𝑈)
∧ 𝐻 ⊆ ℋ),
𝐻, ℋ) ×
if((𝑊 ∈
(SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ))) |
| 24 | 23 | reseq2d 5997 |
. . . . . . . . . 10
⊢ ( ℋ
= if((𝑊 ∈
(SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) → (
+ℎ ↾ ( ℋ × ℋ)) = (
+ℎ ↾ (if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ)))) |
| 25 | | xpeq2 5706 |
. . . . . . . . . . 11
⊢ ( ℋ
= if((𝑊 ∈
(SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) → (ℂ
× ℋ) = (ℂ × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ))) |
| 26 | 25 | reseq2d 5997 |
. . . . . . . . . 10
⊢ ( ℋ
= if((𝑊 ∈
(SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) → (
·ℎ ↾ (ℂ × ℋ)) = (
·ℎ ↾ (ℂ × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ)))) |
| 27 | 24, 26 | opeq12d 4881 |
. . . . . . . . 9
⊢ ( ℋ
= if((𝑊 ∈
(SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) → 〈(
+ℎ ↾ ( ℋ × ℋ)), (
·ℎ ↾ (ℂ × ℋ))〉 =
〈( +ℎ ↾ (if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ))), (
·ℎ ↾ (ℂ × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ)))〉) |
| 28 | | reseq2 5992 |
. . . . . . . . 9
⊢ ( ℋ
= if((𝑊 ∈
(SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) →
(normℎ ↾ ℋ) = (normℎ ↾
if((𝑊 ∈
(SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ))) |
| 29 | 27, 28 | opeq12d 4881 |
. . . . . . . 8
⊢ ( ℋ
= if((𝑊 ∈
(SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) → 〈〈(
+ℎ ↾ ( ℋ × ℋ)), (
·ℎ ↾ (ℂ × ℋ))〉,
(normℎ ↾ ℋ)〉 = 〈〈(
+ℎ ↾ (if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ))), (
·ℎ ↾ (ℂ × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ)))〉, (normℎ
↾ if((𝑊 ∈
(SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻,
ℋ))〉) |
| 30 | 29 | eleq1d 2826 |
. . . . . . 7
⊢ ( ℋ
= if((𝑊 ∈
(SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) → (〈〈(
+ℎ ↾ ( ℋ × ℋ)), (
·ℎ ↾ (ℂ × ℋ))〉,
(normℎ ↾ ℋ)〉 ∈ (SubSp‘𝑈) ↔ 〈〈(
+ℎ ↾ (if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ))), (
·ℎ ↾ (ℂ × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ)))〉, (normℎ
↾ if((𝑊 ∈
(SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ))〉 ∈
(SubSp‘𝑈))) |
| 31 | | sseq1 4009 |
. . . . . . 7
⊢ ( ℋ
= if((𝑊 ∈
(SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) → ( ℋ
⊆ ℋ ↔ if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) ⊆
ℋ)) |
| 32 | 30, 31 | anbi12d 632 |
. . . . . 6
⊢ ( ℋ
= if((𝑊 ∈
(SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) →
((〈〈( +ℎ ↾ ( ℋ × ℋ)), (
·ℎ ↾ (ℂ × ℋ))〉,
(normℎ ↾ ℋ)〉 ∈ (SubSp‘𝑈) ∧ ℋ ⊆ ℋ)
↔ (〈〈( +ℎ ↾ (if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ))), (
·ℎ ↾ (ℂ × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ)))〉, (normℎ
↾ if((𝑊 ∈
(SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ))〉 ∈
(SubSp‘𝑈) ∧
if((𝑊 ∈
(SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) ⊆
ℋ))) |
| 33 | | ax-hfvadd 31019 |
. . . . . . . . . . . 12
⊢
+ℎ :( ℋ × ℋ)⟶
ℋ |
| 34 | | ffn 6736 |
. . . . . . . . . . . 12
⊢ (
+ℎ :( ℋ × ℋ)⟶ ℋ →
+ℎ Fn ( ℋ × ℋ)) |
| 35 | | fnresdm 6687 |
. . . . . . . . . . . 12
⊢ (
+ℎ Fn ( ℋ × ℋ) → (
+ℎ ↾ ( ℋ × ℋ)) = +ℎ
) |
| 36 | 33, 34, 35 | mp2b 10 |
. . . . . . . . . . 11
⊢ (
+ℎ ↾ ( ℋ × ℋ)) =
+ℎ |
| 37 | | ax-hfvmul 31024 |
. . . . . . . . . . . 12
⊢
·ℎ :(ℂ × ℋ)⟶
ℋ |
| 38 | | ffn 6736 |
. . . . . . . . . . . 12
⊢ (
·ℎ :(ℂ × ℋ)⟶ ℋ
→ ·ℎ Fn (ℂ ×
ℋ)) |
| 39 | | fnresdm 6687 |
. . . . . . . . . . . 12
⊢ (
·ℎ Fn (ℂ × ℋ) → (
·ℎ ↾ (ℂ × ℋ)) =
·ℎ ) |
| 40 | 37, 38, 39 | mp2b 10 |
. . . . . . . . . . 11
⊢ (
·ℎ ↾ (ℂ × ℋ)) =
·ℎ |
| 41 | 36, 40 | opeq12i 4878 |
. . . . . . . . . 10
⊢ 〈(
+ℎ ↾ ( ℋ × ℋ)), (
·ℎ ↾ (ℂ × ℋ))〉 =
〈 +ℎ , ·ℎ
〉 |
| 42 | | normf 31142 |
. . . . . . . . . . 11
⊢
normℎ: ℋ⟶ℝ |
| 43 | | ffn 6736 |
. . . . . . . . . . 11
⊢
(normℎ: ℋ⟶ℝ →
normℎ Fn ℋ) |
| 44 | | fnresdm 6687 |
. . . . . . . . . . 11
⊢
(normℎ Fn ℋ → (normℎ
↾ ℋ) = normℎ) |
| 45 | 42, 43, 44 | mp2b 10 |
. . . . . . . . . 10
⊢
(normℎ ↾ ℋ) =
normℎ |
| 46 | 41, 45 | opeq12i 4878 |
. . . . . . . . 9
⊢
〈〈( +ℎ ↾ ( ℋ × ℋ)),
( ·ℎ ↾ (ℂ × ℋ))〉,
(normℎ ↾ ℋ)〉 = 〈〈
+ℎ , ·ℎ 〉,
normℎ〉 |
| 47 | 46, 1 | eqtr4i 2768 |
. . . . . . . 8
⊢
〈〈( +ℎ ↾ ( ℋ × ℋ)),
( ·ℎ ↾ (ℂ × ℋ))〉,
(normℎ ↾ ℋ)〉 = 𝑈 |
| 48 | 1 | hhnv 31184 |
. . . . . . . . 9
⊢ 𝑈 ∈ NrmCVec |
| 49 | | eqid 2737 |
. . . . . . . . . 10
⊢
(SubSp‘𝑈) =
(SubSp‘𝑈) |
| 50 | 49 | sspid 30744 |
. . . . . . . . 9
⊢ (𝑈 ∈ NrmCVec → 𝑈 ∈ (SubSp‘𝑈)) |
| 51 | 48, 50 | ax-mp 5 |
. . . . . . . 8
⊢ 𝑈 ∈ (SubSp‘𝑈) |
| 52 | 47, 51 | eqeltri 2837 |
. . . . . . 7
⊢
〈〈( +ℎ ↾ ( ℋ × ℋ)),
( ·ℎ ↾ (ℂ × ℋ))〉,
(normℎ ↾ ℋ)〉 ∈ (SubSp‘𝑈) |
| 53 | | ssid 4006 |
. . . . . . 7
⊢ ℋ
⊆ ℋ |
| 54 | 52, 53 | pm3.2i 470 |
. . . . . 6
⊢
(〈〈( +ℎ ↾ ( ℋ × ℋ)),
( ·ℎ ↾ (ℂ × ℋ))〉,
(normℎ ↾ ℋ)〉 ∈ (SubSp‘𝑈) ∧ ℋ ⊆
ℋ) |
| 55 | 20, 32, 54 | elimhyp 4591 |
. . . . 5
⊢
(〈〈( +ℎ ↾ (if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ))), (
·ℎ ↾ (ℂ × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ)))〉, (normℎ
↾ if((𝑊 ∈
(SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ))〉 ∈
(SubSp‘𝑈) ∧
if((𝑊 ∈
(SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) ⊆
ℋ) |
| 56 | 55 | simpli 483 |
. . . 4
⊢
〈〈( +ℎ ↾ (if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ))), (
·ℎ ↾ (ℂ × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ)))〉, (normℎ
↾ if((𝑊 ∈
(SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ))〉 ∈
(SubSp‘𝑈) |
| 57 | 55 | simpri 485 |
. . . 4
⊢ if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) ⊆ ℋ |
| 58 | 1, 7, 56, 57 | hhshsslem2 31287 |
. . 3
⊢ if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) ∈
Sℋ |
| 59 | 6, 58 | dedth 4584 |
. 2
⊢ ((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ) → 𝐻 ∈ Sℋ
) |
| 60 | 5, 59 | impbii 209 |
1
⊢ (𝐻 ∈
Sℋ ↔ (𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ)) |