| Step | Hyp | Ref
| Expression |
| 1 | | cncph.6 |
. 2
⊢ 𝑈 = 〈〈 + , ·
〉, abs〉 |
| 2 | | eqid 2737 |
. . . 4
⊢
〈〈 + , · 〉, abs〉 = 〈〈 + , ·
〉, abs〉 |
| 3 | 2 | cnnv 30696 |
. . 3
⊢
〈〈 + , · 〉, abs〉 ∈
NrmCVec |
| 4 | | mulm1 11704 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℂ → (-1
· 𝑦) = -𝑦) |
| 5 | 4 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (-1
· 𝑦) = -𝑦) |
| 6 | 5 | oveq2d 7447 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 + (-1 · 𝑦)) = (𝑥 + -𝑦)) |
| 7 | | negsub 11557 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 + -𝑦) = (𝑥 − 𝑦)) |
| 8 | 6, 7 | eqtrd 2777 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 + (-1 · 𝑦)) = (𝑥 − 𝑦)) |
| 9 | 8 | fveq2d 6910 |
. . . . . . 7
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) →
(abs‘(𝑥 + (-1
· 𝑦))) =
(abs‘(𝑥 − 𝑦))) |
| 10 | 9 | oveq1d 7446 |
. . . . . 6
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) →
((abs‘(𝑥 + (-1
· 𝑦)))↑2) =
((abs‘(𝑥 −
𝑦))↑2)) |
| 11 | 10 | oveq2d 7447 |
. . . . 5
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) →
(((abs‘(𝑥 + 𝑦))↑2) + ((abs‘(𝑥 + (-1 · 𝑦)))↑2)) =
(((abs‘(𝑥 + 𝑦))↑2) + ((abs‘(𝑥 − 𝑦))↑2))) |
| 12 | | sqabsadd 15321 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) →
((abs‘(𝑥 + 𝑦))↑2) = ((((abs‘𝑥)↑2) + ((abs‘𝑦)↑2)) + (2 ·
(ℜ‘(𝑥 ·
(∗‘𝑦)))))) |
| 13 | | sqabssub 15322 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) →
((abs‘(𝑥 −
𝑦))↑2) =
((((abs‘𝑥)↑2) +
((abs‘𝑦)↑2))
− (2 · (ℜ‘(𝑥 · (∗‘𝑦)))))) |
| 14 | 12, 13 | oveq12d 7449 |
. . . . . . 7
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) →
(((abs‘(𝑥 + 𝑦))↑2) + ((abs‘(𝑥 − 𝑦))↑2)) = (((((abs‘𝑥)↑2) + ((abs‘𝑦)↑2)) + (2 ·
(ℜ‘(𝑥 ·
(∗‘𝑦))))) +
((((abs‘𝑥)↑2) +
((abs‘𝑦)↑2))
− (2 · (ℜ‘(𝑥 · (∗‘𝑦))))))) |
| 15 | | abscl 15317 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℂ →
(abs‘𝑥) ∈
ℝ) |
| 16 | 15 | recnd 11289 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℂ →
(abs‘𝑥) ∈
ℂ) |
| 17 | 16 | sqcld 14184 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℂ →
((abs‘𝑥)↑2)
∈ ℂ) |
| 18 | | abscl 15317 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℂ →
(abs‘𝑦) ∈
ℝ) |
| 19 | 18 | recnd 11289 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℂ →
(abs‘𝑦) ∈
ℂ) |
| 20 | 19 | sqcld 14184 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℂ →
((abs‘𝑦)↑2)
∈ ℂ) |
| 21 | | addcl 11237 |
. . . . . . . . 9
⊢
((((abs‘𝑥)↑2) ∈ ℂ ∧
((abs‘𝑦)↑2)
∈ ℂ) → (((abs‘𝑥)↑2) + ((abs‘𝑦)↑2)) ∈ ℂ) |
| 22 | 17, 20, 21 | syl2an 596 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) →
(((abs‘𝑥)↑2) +
((abs‘𝑦)↑2))
∈ ℂ) |
| 23 | | 2cn 12341 |
. . . . . . . . 9
⊢ 2 ∈
ℂ |
| 24 | | cjcl 15144 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℂ →
(∗‘𝑦) ∈
ℂ) |
| 25 | | mulcl 11239 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℂ ∧
(∗‘𝑦) ∈
ℂ) → (𝑥 ·
(∗‘𝑦)) ∈
ℂ) |
| 26 | 24, 25 | sylan2 593 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · (∗‘𝑦)) ∈
ℂ) |
| 27 | | recl 15149 |
. . . . . . . . . . 11
⊢ ((𝑥 · (∗‘𝑦)) ∈ ℂ →
(ℜ‘(𝑥 ·
(∗‘𝑦))) ∈
ℝ) |
| 28 | 27 | recnd 11289 |
. . . . . . . . . 10
⊢ ((𝑥 · (∗‘𝑦)) ∈ ℂ →
(ℜ‘(𝑥 ·
(∗‘𝑦))) ∈
ℂ) |
| 29 | 26, 28 | syl 17 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) →
(ℜ‘(𝑥 ·
(∗‘𝑦))) ∈
ℂ) |
| 30 | | mulcl 11239 |
. . . . . . . . 9
⊢ ((2
∈ ℂ ∧ (ℜ‘(𝑥 · (∗‘𝑦))) ∈ ℂ) → (2 ·
(ℜ‘(𝑥 ·
(∗‘𝑦))))
∈ ℂ) |
| 31 | 23, 29, 30 | sylancr 587 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (2
· (ℜ‘(𝑥
· (∗‘𝑦)))) ∈ ℂ) |
| 32 | 22, 31, 22 | ppncand 11660 |
. . . . . . 7
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) →
(((((abs‘𝑥)↑2) +
((abs‘𝑦)↑2)) +
(2 · (ℜ‘(𝑥 · (∗‘𝑦))))) + ((((abs‘𝑥)↑2) + ((abs‘𝑦)↑2)) − (2 ·
(ℜ‘(𝑥 ·
(∗‘𝑦)))))) =
((((abs‘𝑥)↑2) +
((abs‘𝑦)↑2)) +
(((abs‘𝑥)↑2) +
((abs‘𝑦)↑2)))) |
| 33 | 14, 32 | eqtrd 2777 |
. . . . . 6
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) →
(((abs‘(𝑥 + 𝑦))↑2) + ((abs‘(𝑥 − 𝑦))↑2)) = ((((abs‘𝑥)↑2) + ((abs‘𝑦)↑2)) + (((abs‘𝑥)↑2) + ((abs‘𝑦)↑2)))) |
| 34 | | 2times 12402 |
. . . . . . . 8
⊢
((((abs‘𝑥)↑2) + ((abs‘𝑦)↑2)) ∈ ℂ → (2 ·
(((abs‘𝑥)↑2) +
((abs‘𝑦)↑2))) =
((((abs‘𝑥)↑2) +
((abs‘𝑦)↑2)) +
(((abs‘𝑥)↑2) +
((abs‘𝑦)↑2)))) |
| 35 | 34 | eqcomd 2743 |
. . . . . . 7
⊢
((((abs‘𝑥)↑2) + ((abs‘𝑦)↑2)) ∈ ℂ →
((((abs‘𝑥)↑2) +
((abs‘𝑦)↑2)) +
(((abs‘𝑥)↑2) +
((abs‘𝑦)↑2))) =
(2 · (((abs‘𝑥)↑2) + ((abs‘𝑦)↑2)))) |
| 36 | 22, 35 | syl 17 |
. . . . . 6
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) →
((((abs‘𝑥)↑2) +
((abs‘𝑦)↑2)) +
(((abs‘𝑥)↑2) +
((abs‘𝑦)↑2))) =
(2 · (((abs‘𝑥)↑2) + ((abs‘𝑦)↑2)))) |
| 37 | 33, 36 | eqtrd 2777 |
. . . . 5
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) →
(((abs‘(𝑥 + 𝑦))↑2) + ((abs‘(𝑥 − 𝑦))↑2)) = (2 · (((abs‘𝑥)↑2) + ((abs‘𝑦)↑2)))) |
| 38 | 11, 37 | eqtrd 2777 |
. . . 4
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) →
(((abs‘(𝑥 + 𝑦))↑2) + ((abs‘(𝑥 + (-1 · 𝑦)))↑2)) = (2 ·
(((abs‘𝑥)↑2) +
((abs‘𝑦)↑2)))) |
| 39 | 38 | rgen2 3199 |
. . 3
⊢
∀𝑥 ∈
ℂ ∀𝑦 ∈
ℂ (((abs‘(𝑥 +
𝑦))↑2) +
((abs‘(𝑥 + (-1
· 𝑦)))↑2)) = (2
· (((abs‘𝑥)↑2) + ((abs‘𝑦)↑2))) |
| 40 | | addex 13031 |
. . . 4
⊢ + ∈
V |
| 41 | | mulex 13033 |
. . . 4
⊢ ·
∈ V |
| 42 | | absf 15376 |
. . . . 5
⊢
abs:ℂ⟶ℝ |
| 43 | | cnex 11236 |
. . . . 5
⊢ ℂ
∈ V |
| 44 | | fex 7246 |
. . . . 5
⊢
((abs:ℂ⟶ℝ ∧ ℂ ∈ V) → abs ∈
V) |
| 45 | 42, 43, 44 | mp2an 692 |
. . . 4
⊢ abs
∈ V |
| 46 | | cnaddabloOLD 30600 |
. . . . . . 7
⊢ + ∈
AbelOp |
| 47 | | ablogrpo 30566 |
. . . . . . 7
⊢ ( +
∈ AbelOp → + ∈ GrpOp) |
| 48 | 46, 47 | ax-mp 5 |
. . . . . 6
⊢ + ∈
GrpOp |
| 49 | | ax-addf 11234 |
. . . . . . 7
⊢ +
:(ℂ × ℂ)⟶ℂ |
| 50 | 49 | fdmi 6747 |
. . . . . 6
⊢ dom + =
(ℂ × ℂ) |
| 51 | 48, 50 | grporn 30540 |
. . . . 5
⊢ ℂ =
ran + |
| 52 | 51 | isphg 30836 |
. . . 4
⊢ (( +
∈ V ∧ · ∈ V ∧ abs ∈ V) → (〈〈 + ,
· 〉, abs〉 ∈ CPreHilOLD ↔ (〈〈 +
, · 〉, abs〉 ∈ NrmCVec ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℂ (((abs‘(𝑥 + 𝑦))↑2) + ((abs‘(𝑥 + (-1 · 𝑦)))↑2)) = (2 · (((abs‘𝑥)↑2) + ((abs‘𝑦)↑2)))))) |
| 53 | 40, 41, 45, 52 | mp3an 1463 |
. . 3
⊢
(〈〈 + , · 〉, abs〉 ∈
CPreHilOLD ↔ (〈〈 + , · 〉, abs〉
∈ NrmCVec ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℂ (((abs‘(𝑥 + 𝑦))↑2) + ((abs‘(𝑥 + (-1 · 𝑦)))↑2)) = (2 · (((abs‘𝑥)↑2) + ((abs‘𝑦)↑2))))) |
| 54 | 3, 39, 53 | mpbir2an 711 |
. 2
⊢
〈〈 + , · 〉, abs〉 ∈
CPreHilOLD |
| 55 | 1, 54 | eqeltri 2837 |
1
⊢ 𝑈 ∈
CPreHilOLD |