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