Metamath Proof Explorer

Theorem cncph

Description: The set of complex numbers is an inner product (pre-Hilbert) space. (Contributed by Steve Rodriguez, 28-Apr-2007) (Revised by Mario Carneiro, 7-Nov-2013) (New usage is discouraged.)

Ref Expression
Hypothesis cncph.6 ⊢ 𝑈 = ⟨ ⟨ + , · ⟩ , abs ⟩
Assertion cncph 𝑈 ∈ CPreHilOLD

Proof

Step Hyp Ref Expression
1 cncph.6 ⊢ 𝑈 = ⟨ ⟨ + , · ⟩ , abs ⟩
2 eqid ⊢ ⟨ ⟨ + , · ⟩ , abs ⟩ = ⟨ ⟨ + , · ⟩ , abs ⟩
3 2 cnnv ⊢ ⟨ ⟨ + , · ⟩ , abs ⟩ ∈ NrmCVec
4 mulm1 ⊢ ( 𝑦 ∈ ℂ → ( - 1 · 𝑦 ) = - 𝑦 )
5 4 adantl ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( - 1 · 𝑦 ) = - 𝑦 )
6 5 oveq2d ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 + ( - 1 · 𝑦 ) ) = ( 𝑥 + - 𝑦 ) )
7 negsub ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 + - 𝑦 ) = ( 𝑥 − 𝑦 ) )
8 6 7 eqtrd ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 + ( - 1 · 𝑦 ) ) = ( 𝑥 − 𝑦 ) )
9 8 fveq2d ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( abs ‘ ( 𝑥 + ( - 1 · 𝑦 ) ) ) = ( abs ‘ ( 𝑥 − 𝑦 ) ) )
10 9 oveq1d ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( abs ‘ ( 𝑥 + ( - 1 · 𝑦 ) ) ) ↑ 2 ) = ( ( abs ‘ ( 𝑥 − 𝑦 ) ) ↑ 2 ) )
11 10 oveq2d ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( ( abs ‘ ( 𝑥 + 𝑦 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝑥 + ( - 1 · 𝑦 ) ) ) ↑ 2 ) ) = ( ( ( abs ‘ ( 𝑥 + 𝑦 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝑥 − 𝑦 ) ) ↑ 2 ) ) )
12 sqabsadd ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( abs ‘ ( 𝑥 + 𝑦 ) ) ↑ 2 ) = ( ( ( ( abs ‘ 𝑥 ) ↑ 2 ) + ( ( abs ‘ 𝑦 ) ↑ 2 ) ) + ( 2 · ( ℜ ‘ ( 𝑥 · ( ∗ ‘ 𝑦 ) ) ) ) ) )
13 sqabssub ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( abs ‘ ( 𝑥 − 𝑦 ) ) ↑ 2 ) = ( ( ( ( abs ‘ 𝑥 ) ↑ 2 ) + ( ( abs ‘ 𝑦 ) ↑ 2 ) ) − ( 2 · ( ℜ ‘ ( 𝑥 · ( ∗ ‘ 𝑦 ) ) ) ) ) )
14 12 13 oveq12d ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( ( abs ‘ ( 𝑥 + 𝑦 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝑥 − 𝑦 ) ) ↑ 2 ) ) = ( ( ( ( ( abs ‘ 𝑥 ) ↑ 2 ) + ( ( abs ‘ 𝑦 ) ↑ 2 ) ) + ( 2 · ( ℜ ‘ ( 𝑥 · ( ∗ ‘ 𝑦 ) ) ) ) ) + ( ( ( ( abs ‘ 𝑥 ) ↑ 2 ) + ( ( abs ‘ 𝑦 ) ↑ 2 ) ) − ( 2 · ( ℜ ‘ ( 𝑥 · ( ∗ ‘ 𝑦 ) ) ) ) ) ) )
15 abscl ⊢ ( 𝑥 ∈ ℂ → ( abs ‘ 𝑥 ) ∈ ℝ )
16 15 recnd ⊢ ( 𝑥 ∈ ℂ → ( abs ‘ 𝑥 ) ∈ ℂ )
17 16 sqcld ⊢ ( 𝑥 ∈ ℂ → ( ( abs ‘ 𝑥 ) ↑ 2 ) ∈ ℂ )
18 abscl ⊢ ( 𝑦 ∈ ℂ → ( abs ‘ 𝑦 ) ∈ ℝ )
19 18 recnd ⊢ ( 𝑦 ∈ ℂ → ( abs ‘ 𝑦 ) ∈ ℂ )
20 19 sqcld ⊢ ( 𝑦 ∈ ℂ → ( ( abs ‘ 𝑦 ) ↑ 2 ) ∈ ℂ )
21 addcl ⊢ ( ( ( ( abs ‘ 𝑥 ) ↑ 2 ) ∈ ℂ ∧ ( ( abs ‘ 𝑦 ) ↑ 2 ) ∈ ℂ ) → ( ( ( abs ‘ 𝑥 ) ↑ 2 ) + ( ( abs ‘ 𝑦 ) ↑ 2 ) ) ∈ ℂ )
22 17 20 21 syl2an ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( ( abs ‘ 𝑥 ) ↑ 2 ) + ( ( abs ‘ 𝑦 ) ↑ 2 ) ) ∈ ℂ )
23 2cn ⊢ 2 ∈ ℂ
24 cjcl ⊢ ( 𝑦 ∈ ℂ → ( ∗ ‘ 𝑦 ) ∈ ℂ )
25 mulcl ⊢ ( ( 𝑥 ∈ ℂ ∧ ( ∗ ‘ 𝑦 ) ∈ ℂ ) → ( 𝑥 · ( ∗ ‘ 𝑦 ) ) ∈ ℂ )
26 24 25 sylan2 ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 · ( ∗ ‘ 𝑦 ) ) ∈ ℂ )
27 recl ⊢ ( ( 𝑥 · ( ∗ ‘ 𝑦 ) ) ∈ ℂ → ( ℜ ‘ ( 𝑥 · ( ∗ ‘ 𝑦 ) ) ) ∈ ℝ )
28 27 recnd ⊢ ( ( 𝑥 · ( ∗ ‘ 𝑦 ) ) ∈ ℂ → ( ℜ ‘ ( 𝑥 · ( ∗ ‘ 𝑦 ) ) ) ∈ ℂ )
29 26 28 syl ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ℜ ‘ ( 𝑥 · ( ∗ ‘ 𝑦 ) ) ) ∈ ℂ )
30 mulcl ⊢ ( ( 2 ∈ ℂ ∧ ( ℜ ‘ ( 𝑥 · ( ∗ ‘ 𝑦 ) ) ) ∈ ℂ ) → ( 2 · ( ℜ ‘ ( 𝑥 · ( ∗ ‘ 𝑦 ) ) ) ) ∈ ℂ )
31 23 29 30 sylancr ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 2 · ( ℜ ‘ ( 𝑥 · ( ∗ ‘ 𝑦 ) ) ) ) ∈ ℂ )
32 22 31 22 ppncand ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( ( ( ( abs ‘ 𝑥 ) ↑ 2 ) + ( ( abs ‘ 𝑦 ) ↑ 2 ) ) + ( 2 · ( ℜ ‘ ( 𝑥 · ( ∗ ‘ 𝑦 ) ) ) ) ) + ( ( ( ( abs ‘ 𝑥 ) ↑ 2 ) + ( ( abs ‘ 𝑦 ) ↑ 2 ) ) − ( 2 · ( ℜ ‘ ( 𝑥 · ( ∗ ‘ 𝑦 ) ) ) ) ) ) = ( ( ( ( abs ‘ 𝑥 ) ↑ 2 ) + ( ( abs ‘ 𝑦 ) ↑ 2 ) ) + ( ( ( abs ‘ 𝑥 ) ↑ 2 ) + ( ( abs ‘ 𝑦 ) ↑ 2 ) ) ) )
33 14 32 eqtrd ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( ( abs ‘ ( 𝑥 + 𝑦 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝑥 − 𝑦 ) ) ↑ 2 ) ) = ( ( ( ( abs ‘ 𝑥 ) ↑ 2 ) + ( ( abs ‘ 𝑦 ) ↑ 2 ) ) + ( ( ( abs ‘ 𝑥 ) ↑ 2 ) + ( ( abs ‘ 𝑦 ) ↑ 2 ) ) ) )
34 2times ⊢ ( ( ( ( abs ‘ 𝑥 ) ↑ 2 ) + ( ( abs ‘ 𝑦 ) ↑ 2 ) ) ∈ ℂ → ( 2 · ( ( ( abs ‘ 𝑥 ) ↑ 2 ) + ( ( abs ‘ 𝑦 ) ↑ 2 ) ) ) = ( ( ( ( abs ‘ 𝑥 ) ↑ 2 ) + ( ( abs ‘ 𝑦 ) ↑ 2 ) ) + ( ( ( abs ‘ 𝑥 ) ↑ 2 ) + ( ( abs ‘ 𝑦 ) ↑ 2 ) ) ) )
35 34 eqcomd ⊢ ( ( ( ( abs ‘ 𝑥 ) ↑ 2 ) + ( ( abs ‘ 𝑦 ) ↑ 2 ) ) ∈ ℂ → ( ( ( ( abs ‘ 𝑥 ) ↑ 2 ) + ( ( abs ‘ 𝑦 ) ↑ 2 ) ) + ( ( ( abs ‘ 𝑥 ) ↑ 2 ) + ( ( abs ‘ 𝑦 ) ↑ 2 ) ) ) = ( 2 · ( ( ( abs ‘ 𝑥 ) ↑ 2 ) + ( ( abs ‘ 𝑦 ) ↑ 2 ) ) ) )
36 22 35 syl ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( ( ( abs ‘ 𝑥 ) ↑ 2 ) + ( ( abs ‘ 𝑦 ) ↑ 2 ) ) + ( ( ( abs ‘ 𝑥 ) ↑ 2 ) + ( ( abs ‘ 𝑦 ) ↑ 2 ) ) ) = ( 2 · ( ( ( abs ‘ 𝑥 ) ↑ 2 ) + ( ( abs ‘ 𝑦 ) ↑ 2 ) ) ) )
37 33 36 eqtrd ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( ( abs ‘ ( 𝑥 + 𝑦 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝑥 − 𝑦 ) ) ↑ 2 ) ) = ( 2 · ( ( ( abs ‘ 𝑥 ) ↑ 2 ) + ( ( abs ‘ 𝑦 ) ↑ 2 ) ) ) )
38 11 37 eqtrd ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( ( abs ‘ ( 𝑥 + 𝑦 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝑥 + ( - 1 · 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( abs ‘ 𝑥 ) ↑ 2 ) + ( ( abs ‘ 𝑦 ) ↑ 2 ) ) ) )
39 38 rgen2 ⊢ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℂ ( ( ( abs ‘ ( 𝑥 + 𝑦 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝑥 + ( - 1 · 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( abs ‘ 𝑥 ) ↑ 2 ) + ( ( abs ‘ 𝑦 ) ↑ 2 ) ) )
40 addex ⊢ + ∈ V
41 mulex ⊢ · ∈ V
42 absf ⊢ abs : ℂ ⟶ ℝ
43 cnex ⊢ ℂ ∈ V
44 fex ⊢ ( ( abs : ℂ ⟶ ℝ ∧ ℂ ∈ V ) → abs ∈ V )
45 42 43 44 mp2an ⊢ abs ∈ V
46 cnaddabloOLD ⊢ + ∈ AbelOp
47 ablogrpo ⊢ ( + ∈ AbelOp → + ∈ GrpOp )
48 46 47 ax-mp ⊢ + ∈ GrpOp
49 ax-addf ⊢ + : ( ℂ × ℂ ) ⟶ ℂ
50 49 fdmi ⊢ dom + = ( ℂ × ℂ )
51 48 50 grporn ⊢ ℂ = ran +
52 51 isphg ⊢ ( ( + ∈ V ∧ · ∈ V ∧ abs ∈ V ) → ( ⟨ ⟨ + , · ⟩ , abs ⟩ ∈ CPreHilOLD ↔ ( ⟨ ⟨ + , · ⟩ , abs ⟩ ∈ NrmCVec ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℂ ( ( ( abs ‘ ( 𝑥 + 𝑦 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝑥 + ( - 1 · 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( abs ‘ 𝑥 ) ↑ 2 ) + ( ( abs ‘ 𝑦 ) ↑ 2 ) ) ) ) ) )
53 40 41 45 52 mp3an ⊢ ( ⟨ ⟨ + , · ⟩ , abs ⟩ ∈ CPreHilOLD ↔ ( ⟨ ⟨ + , · ⟩ , abs ⟩ ∈ NrmCVec ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℂ ( ( ( abs ‘ ( 𝑥 + 𝑦 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝑥 + ( - 1 · 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( abs ‘ 𝑥 ) ↑ 2 ) + ( ( abs ‘ 𝑦 ) ↑ 2 ) ) ) ) )
54 3 39 53 mpbir2an ⊢ ⟨ ⟨ + , · ⟩ , abs ⟩ ∈ CPreHilOLD
55 1 54 eqeltri ⊢ 𝑈 ∈ CPreHilOLD