| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . 3
⊢
〈〈 +ℎ , ·ℎ
〉, normℎ〉 = 〈〈 +ℎ ,
·ℎ 〉,
normℎ〉 |
| 2 | 1 | hhnv 31184 |
. 2
⊢
〈〈 +ℎ , ·ℎ
〉, normℎ〉 ∈ NrmCVec |
| 3 | | normpar 31174 |
. . . 4
⊢ ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) →
(((normℎ‘(𝑥 −ℎ 𝑦))↑2) +
((normℎ‘(𝑥 +ℎ 𝑦))↑2)) = ((2 ·
((normℎ‘𝑥)↑2)) + (2 ·
((normℎ‘𝑦)↑2)))) |
| 4 | | hvsubval 31035 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) → (𝑥 −ℎ
𝑦) = (𝑥 +ℎ (-1
·ℎ 𝑦))) |
| 5 | 4 | fveq2d 6910 |
. . . . . . 7
⊢ ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) →
(normℎ‘(𝑥 −ℎ 𝑦)) =
(normℎ‘(𝑥 +ℎ (-1
·ℎ 𝑦)))) |
| 6 | 5 | oveq1d 7446 |
. . . . . 6
⊢ ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) →
((normℎ‘(𝑥 −ℎ 𝑦))↑2) =
((normℎ‘(𝑥 +ℎ (-1
·ℎ 𝑦)))↑2)) |
| 7 | 6 | oveq2d 7447 |
. . . . 5
⊢ ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) →
(((normℎ‘(𝑥 +ℎ 𝑦))↑2) +
((normℎ‘(𝑥 −ℎ 𝑦))↑2)) =
(((normℎ‘(𝑥 +ℎ 𝑦))↑2) +
((normℎ‘(𝑥 +ℎ (-1
·ℎ 𝑦)))↑2))) |
| 8 | | hvaddcl 31031 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) → (𝑥 +ℎ 𝑦) ∈
ℋ) |
| 9 | | normcl 31144 |
. . . . . . . . 9
⊢ ((𝑥 +ℎ 𝑦) ∈ ℋ →
(normℎ‘(𝑥 +ℎ 𝑦)) ∈ ℝ) |
| 10 | 8, 9 | syl 17 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) →
(normℎ‘(𝑥 +ℎ 𝑦)) ∈ ℝ) |
| 11 | 10 | recnd 11289 |
. . . . . . 7
⊢ ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) →
(normℎ‘(𝑥 +ℎ 𝑦)) ∈ ℂ) |
| 12 | 11 | sqcld 14184 |
. . . . . 6
⊢ ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) →
((normℎ‘(𝑥 +ℎ 𝑦))↑2) ∈ ℂ) |
| 13 | | hvsubcl 31036 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) → (𝑥 −ℎ
𝑦) ∈
ℋ) |
| 14 | | normcl 31144 |
. . . . . . . . 9
⊢ ((𝑥 −ℎ
𝑦) ∈ ℋ →
(normℎ‘(𝑥 −ℎ 𝑦)) ∈
ℝ) |
| 15 | 14 | recnd 11289 |
. . . . . . . 8
⊢ ((𝑥 −ℎ
𝑦) ∈ ℋ →
(normℎ‘(𝑥 −ℎ 𝑦)) ∈
ℂ) |
| 16 | 13, 15 | syl 17 |
. . . . . . 7
⊢ ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) →
(normℎ‘(𝑥 −ℎ 𝑦)) ∈
ℂ) |
| 17 | 16 | sqcld 14184 |
. . . . . 6
⊢ ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) →
((normℎ‘(𝑥 −ℎ 𝑦))↑2) ∈
ℂ) |
| 18 | 12, 17 | addcomd 11463 |
. . . . 5
⊢ ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) →
(((normℎ‘(𝑥 +ℎ 𝑦))↑2) +
((normℎ‘(𝑥 −ℎ 𝑦))↑2)) =
(((normℎ‘(𝑥 −ℎ 𝑦))↑2) +
((normℎ‘(𝑥 +ℎ 𝑦))↑2))) |
| 19 | 7, 18 | eqtr3d 2779 |
. . . 4
⊢ ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) →
(((normℎ‘(𝑥 +ℎ 𝑦))↑2) +
((normℎ‘(𝑥 +ℎ (-1
·ℎ 𝑦)))↑2)) =
(((normℎ‘(𝑥 −ℎ 𝑦))↑2) +
((normℎ‘(𝑥 +ℎ 𝑦))↑2))) |
| 20 | | normcl 31144 |
. . . . . . 7
⊢ (𝑥 ∈ ℋ →
(normℎ‘𝑥) ∈ ℝ) |
| 21 | 20 | recnd 11289 |
. . . . . 6
⊢ (𝑥 ∈ ℋ →
(normℎ‘𝑥) ∈ ℂ) |
| 22 | 21 | sqcld 14184 |
. . . . 5
⊢ (𝑥 ∈ ℋ →
((normℎ‘𝑥)↑2) ∈ ℂ) |
| 23 | | normcl 31144 |
. . . . . . 7
⊢ (𝑦 ∈ ℋ →
(normℎ‘𝑦) ∈ ℝ) |
| 24 | 23 | recnd 11289 |
. . . . . 6
⊢ (𝑦 ∈ ℋ →
(normℎ‘𝑦) ∈ ℂ) |
| 25 | 24 | sqcld 14184 |
. . . . 5
⊢ (𝑦 ∈ ℋ →
((normℎ‘𝑦)↑2) ∈ ℂ) |
| 26 | | 2cn 12341 |
. . . . . 6
⊢ 2 ∈
ℂ |
| 27 | | adddi 11244 |
. . . . . 6
⊢ ((2
∈ ℂ ∧ ((normℎ‘𝑥)↑2) ∈ ℂ ∧
((normℎ‘𝑦)↑2) ∈ ℂ) → (2 ·
(((normℎ‘𝑥)↑2) +
((normℎ‘𝑦)↑2))) = ((2 ·
((normℎ‘𝑥)↑2)) + (2 ·
((normℎ‘𝑦)↑2)))) |
| 28 | 26, 27 | mp3an1 1450 |
. . . . 5
⊢
((((normℎ‘𝑥)↑2) ∈ ℂ ∧
((normℎ‘𝑦)↑2) ∈ ℂ) → (2 ·
(((normℎ‘𝑥)↑2) +
((normℎ‘𝑦)↑2))) = ((2 ·
((normℎ‘𝑥)↑2)) + (2 ·
((normℎ‘𝑦)↑2)))) |
| 29 | 22, 25, 28 | syl2an 596 |
. . . 4
⊢ ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) → (2
· (((normℎ‘𝑥)↑2) +
((normℎ‘𝑦)↑2))) = ((2 ·
((normℎ‘𝑥)↑2)) + (2 ·
((normℎ‘𝑦)↑2)))) |
| 30 | 3, 19, 29 | 3eqtr4d 2787 |
. . 3
⊢ ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) →
(((normℎ‘(𝑥 +ℎ 𝑦))↑2) +
((normℎ‘(𝑥 +ℎ (-1
·ℎ 𝑦)))↑2)) = (2 ·
(((normℎ‘𝑥)↑2) +
((normℎ‘𝑦)↑2)))) |
| 31 | 30 | rgen2 3199 |
. 2
⊢
∀𝑥 ∈
ℋ ∀𝑦 ∈
ℋ (((normℎ‘(𝑥 +ℎ 𝑦))↑2) +
((normℎ‘(𝑥 +ℎ (-1
·ℎ 𝑦)))↑2)) = (2 ·
(((normℎ‘𝑥)↑2) +
((normℎ‘𝑦)↑2))) |
| 32 | | hilablo 31179 |
. . . 4
⊢
+ℎ ∈ AbelOp |
| 33 | 32 | elexi 3503 |
. . 3
⊢
+ℎ ∈ V |
| 34 | | hvmulex 31030 |
. . 3
⊢
·ℎ ∈ V |
| 35 | | normf 31142 |
. . . 4
⊢
normℎ: ℋ⟶ℝ |
| 36 | | ax-hilex 31018 |
. . . 4
⊢ ℋ
∈ V |
| 37 | | fex 7246 |
. . . 4
⊢
((normℎ: ℋ⟶ℝ ∧ ℋ ∈
V) → normℎ ∈ V) |
| 38 | 35, 36, 37 | mp2an 692 |
. . 3
⊢
normℎ ∈ V |
| 39 | | hhnv.1 |
. . . . 5
⊢ 𝑈 = 〈〈
+ℎ , ·ℎ 〉,
normℎ〉 |
| 40 | 39 | eleq1i 2832 |
. . . 4
⊢ (𝑈 ∈ CPreHilOLD
↔ 〈〈 +ℎ , ·ℎ
〉, normℎ〉 ∈
CPreHilOLD) |
| 41 | | ablogrpo 30566 |
. . . . . . 7
⊢ (
+ℎ ∈ AbelOp → +ℎ ∈
GrpOp) |
| 42 | 32, 41 | ax-mp 5 |
. . . . . 6
⊢
+ℎ ∈ GrpOp |
| 43 | | ax-hfvadd 31019 |
. . . . . . 7
⊢
+ℎ :( ℋ × ℋ)⟶
ℋ |
| 44 | 43 | fdmi 6747 |
. . . . . 6
⊢ dom
+ℎ = ( ℋ × ℋ) |
| 45 | 42, 44 | grporn 30540 |
. . . . 5
⊢ ℋ
= ran +ℎ |
| 46 | 45 | isphg 30836 |
. . . 4
⊢ ((
+ℎ ∈ V ∧ ·ℎ ∈ V
∧ normℎ ∈ V) → (〈〈
+ℎ , ·ℎ 〉,
normℎ〉 ∈ CPreHilOLD ↔ (〈〈
+ℎ , ·ℎ 〉,
normℎ〉 ∈ NrmCVec ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ
(((normℎ‘(𝑥 +ℎ 𝑦))↑2) +
((normℎ‘(𝑥 +ℎ (-1
·ℎ 𝑦)))↑2)) = (2 ·
(((normℎ‘𝑥)↑2) +
((normℎ‘𝑦)↑2)))))) |
| 47 | 40, 46 | bitrid 283 |
. . 3
⊢ ((
+ℎ ∈ V ∧ ·ℎ ∈ V
∧ normℎ ∈ V) → (𝑈 ∈ CPreHilOLD ↔
(〈〈 +ℎ , ·ℎ 〉,
normℎ〉 ∈ NrmCVec ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ
(((normℎ‘(𝑥 +ℎ 𝑦))↑2) +
((normℎ‘(𝑥 +ℎ (-1
·ℎ 𝑦)))↑2)) = (2 ·
(((normℎ‘𝑥)↑2) +
((normℎ‘𝑦)↑2)))))) |
| 48 | 33, 34, 38, 47 | mp3an 1463 |
. 2
⊢ (𝑈 ∈ CPreHilOLD
↔ (〈〈 +ℎ , ·ℎ
〉, normℎ〉 ∈ NrmCVec ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ
(((normℎ‘(𝑥 +ℎ 𝑦))↑2) +
((normℎ‘(𝑥 +ℎ (-1
·ℎ 𝑦)))↑2)) = (2 ·
(((normℎ‘𝑥)↑2) +
((normℎ‘𝑦)↑2))))) |
| 49 | 2, 31, 48 | mpbir2an 711 |
1
⊢ 𝑈 ∈
CPreHilOLD |