Step | Hyp | Ref
| Expression |
1 | | cncph.6 |
. 2
⊢ 𝑈 = 〈〈 + , ·
〉, abs〉 |
2 | | eqid 2610 |
. . . 4
⊢
〈〈 + , · 〉, abs〉 = 〈〈 + , ·
〉, abs〉 |
3 | 2 | cnnv 26916 |
. . 3
⊢
〈〈 + , · 〉, abs〉 ∈
NrmCVec |
4 | | mulm1 10350 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℂ → (-1
· 𝑦) = -𝑦) |
5 | 4 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (-1
· 𝑦) = -𝑦) |
6 | 5 | oveq2d 6565 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 + (-1 · 𝑦)) = (𝑥 + -𝑦)) |
7 | | negsub 10208 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 + -𝑦) = (𝑥 − 𝑦)) |
8 | 6, 7 | eqtrd 2644 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 + (-1 · 𝑦)) = (𝑥 − 𝑦)) |
9 | 8 | fveq2d 6107 |
. . . . . . 7
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) →
(abs‘(𝑥 + (-1
· 𝑦))) =
(abs‘(𝑥 − 𝑦))) |
10 | 9 | oveq1d 6564 |
. . . . . 6
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) →
((abs‘(𝑥 + (-1
· 𝑦)))↑2) =
((abs‘(𝑥 −
𝑦))↑2)) |
11 | 10 | oveq2d 6565 |
. . . . 5
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) →
(((abs‘(𝑥 + 𝑦))↑2) + ((abs‘(𝑥 + (-1 · 𝑦)))↑2)) =
(((abs‘(𝑥 + 𝑦))↑2) + ((abs‘(𝑥 − 𝑦))↑2))) |
12 | | sqabsadd 13870 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) →
((abs‘(𝑥 + 𝑦))↑2) = ((((abs‘𝑥)↑2) + ((abs‘𝑦)↑2)) + (2 ·
(ℜ‘(𝑥 ·
(∗‘𝑦)))))) |
13 | | sqabssub 13871 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) →
((abs‘(𝑥 −
𝑦))↑2) =
((((abs‘𝑥)↑2) +
((abs‘𝑦)↑2))
− (2 · (ℜ‘(𝑥 · (∗‘𝑦)))))) |
14 | 12, 13 | oveq12d 6567 |
. . . . . . 7
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) →
(((abs‘(𝑥 + 𝑦))↑2) + ((abs‘(𝑥 − 𝑦))↑2)) = (((((abs‘𝑥)↑2) + ((abs‘𝑦)↑2)) + (2 ·
(ℜ‘(𝑥 ·
(∗‘𝑦))))) +
((((abs‘𝑥)↑2) +
((abs‘𝑦)↑2))
− (2 · (ℜ‘(𝑥 · (∗‘𝑦))))))) |
15 | | abscl 13866 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℂ →
(abs‘𝑥) ∈
ℝ) |
16 | 15 | recnd 9947 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℂ →
(abs‘𝑥) ∈
ℂ) |
17 | 16 | sqcld 12868 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℂ →
((abs‘𝑥)↑2)
∈ ℂ) |
18 | | abscl 13866 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℂ →
(abs‘𝑦) ∈
ℝ) |
19 | 18 | recnd 9947 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℂ →
(abs‘𝑦) ∈
ℂ) |
20 | 19 | sqcld 12868 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℂ →
((abs‘𝑦)↑2)
∈ ℂ) |
21 | | addcl 9897 |
. . . . . . . . 9
⊢
((((abs‘𝑥)↑2) ∈ ℂ ∧
((abs‘𝑦)↑2)
∈ ℂ) → (((abs‘𝑥)↑2) + ((abs‘𝑦)↑2)) ∈ ℂ) |
22 | 17, 20, 21 | syl2an 493 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) →
(((abs‘𝑥)↑2) +
((abs‘𝑦)↑2))
∈ ℂ) |
23 | | 2cn 10968 |
. . . . . . . . 9
⊢ 2 ∈
ℂ |
24 | | cjcl 13693 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℂ →
(∗‘𝑦) ∈
ℂ) |
25 | | mulcl 9899 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℂ ∧
(∗‘𝑦) ∈
ℂ) → (𝑥 ·
(∗‘𝑦)) ∈
ℂ) |
26 | 24, 25 | sylan2 490 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · (∗‘𝑦)) ∈
ℂ) |
27 | | recl 13698 |
. . . . . . . . . . 11
⊢ ((𝑥 · (∗‘𝑦)) ∈ ℂ →
(ℜ‘(𝑥 ·
(∗‘𝑦))) ∈
ℝ) |
28 | 27 | recnd 9947 |
. . . . . . . . . 10
⊢ ((𝑥 · (∗‘𝑦)) ∈ ℂ →
(ℜ‘(𝑥 ·
(∗‘𝑦))) ∈
ℂ) |
29 | 26, 28 | syl 17 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) →
(ℜ‘(𝑥 ·
(∗‘𝑦))) ∈
ℂ) |
30 | | mulcl 9899 |
. . . . . . . . 9
⊢ ((2
∈ ℂ ∧ (ℜ‘(𝑥 · (∗‘𝑦))) ∈ ℂ) → (2 ·
(ℜ‘(𝑥 ·
(∗‘𝑦))))
∈ ℂ) |
31 | 23, 29, 30 | sylancr 694 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (2
· (ℜ‘(𝑥
· (∗‘𝑦)))) ∈ ℂ) |
32 | 22, 31, 22 | ppncand 10311 |
. . . . . . 7
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) →
(((((abs‘𝑥)↑2) +
((abs‘𝑦)↑2)) +
(2 · (ℜ‘(𝑥 · (∗‘𝑦))))) + ((((abs‘𝑥)↑2) + ((abs‘𝑦)↑2)) − (2 ·
(ℜ‘(𝑥 ·
(∗‘𝑦)))))) =
((((abs‘𝑥)↑2) +
((abs‘𝑦)↑2)) +
(((abs‘𝑥)↑2) +
((abs‘𝑦)↑2)))) |
33 | 14, 32 | eqtrd 2644 |
. . . . . 6
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) →
(((abs‘(𝑥 + 𝑦))↑2) + ((abs‘(𝑥 − 𝑦))↑2)) = ((((abs‘𝑥)↑2) + ((abs‘𝑦)↑2)) + (((abs‘𝑥)↑2) + ((abs‘𝑦)↑2)))) |
34 | | 2times 11022 |
. . . . . . . 8
⊢
((((abs‘𝑥)↑2) + ((abs‘𝑦)↑2)) ∈ ℂ → (2 ·
(((abs‘𝑥)↑2) +
((abs‘𝑦)↑2))) =
((((abs‘𝑥)↑2) +
((abs‘𝑦)↑2)) +
(((abs‘𝑥)↑2) +
((abs‘𝑦)↑2)))) |
35 | 34 | eqcomd 2616 |
. . . . . . 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 2644 |
. . . . 5
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) →
(((abs‘(𝑥 + 𝑦))↑2) + ((abs‘(𝑥 − 𝑦))↑2)) = (2 · (((abs‘𝑥)↑2) + ((abs‘𝑦)↑2)))) |
38 | 11, 37 | eqtrd 2644 |
. . . 4
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) →
(((abs‘(𝑥 + 𝑦))↑2) + ((abs‘(𝑥 + (-1 · 𝑦)))↑2)) = (2 ·
(((abs‘𝑥)↑2) +
((abs‘𝑦)↑2)))) |
39 | 38 | rgen2a 2960 |
. . 3
⊢
∀𝑥 ∈
ℂ ∀𝑦 ∈
ℂ (((abs‘(𝑥 +
𝑦))↑2) +
((abs‘(𝑥 + (-1
· 𝑦)))↑2)) = (2
· (((abs‘𝑥)↑2) + ((abs‘𝑦)↑2))) |
40 | | addex 11706 |
. . . 4
⊢ + ∈
V |
41 | | mulex 11707 |
. . . 4
⊢ ·
∈ V |
42 | | absf 13925 |
. . . . 5
⊢
abs:ℂ⟶ℝ |
43 | | cnex 9896 |
. . . . 5
⊢ ℂ
∈ V |
44 | | fex 6394 |
. . . . 5
⊢
((abs:ℂ⟶ℝ ∧ ℂ ∈ V) → abs ∈
V) |
45 | 42, 43, 44 | mp2an 704 |
. . . 4
⊢ abs
∈ V |
46 | | cnaddabloOLD 26820 |
. . . . . . 7
⊢ + ∈
AbelOp |
47 | | ablogrpo 26785 |
. . . . . . 7
⊢ ( +
∈ AbelOp → + ∈ GrpOp) |
48 | 46, 47 | ax-mp 5 |
. . . . . 6
⊢ + ∈
GrpOp |
49 | | ax-addf 9894 |
. . . . . . 7
⊢ +
:(ℂ × ℂ)⟶ℂ |
50 | 49 | fdmi 5965 |
. . . . . 6
⊢ dom + =
(ℂ × ℂ) |
51 | 48, 50 | grporn 26759 |
. . . . 5
⊢ ℂ =
ran + |
52 | 51 | isphg 27056 |
. . . 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 1416 |
. . 3
⊢
(〈〈 + , · 〉, abs〉 ∈
CPreHilOLD ↔ (〈〈 + , · 〉, abs〉
∈ NrmCVec ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℂ (((abs‘(𝑥 + 𝑦))↑2) + ((abs‘(𝑥 + (-1 · 𝑦)))↑2)) = (2 · (((abs‘𝑥)↑2) + ((abs‘𝑦)↑2))))) |
54 | 3, 39, 53 | mpbir2an 957 |
. 2
⊢
〈〈 + , · 〉, abs〉 ∈
CPreHilOLD |
55 | 1, 54 | eqeltri 2684 |
1
⊢ 𝑈 ∈
CPreHilOLD |