Theorem cncph 28596

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.)

Hypothesis

Ref	Expression
cncph.6	⊢ 𝑈 = ⟨⟨ + , · ⟩, abs⟩

Assertion

Ref	Expression
cncph	⊢ 𝑈 ∈ CPreHilOLD

Proof of Theorem cncph

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		cncph.6	. 2 ⊢ 𝑈 = ⟨⟨ + , · ⟩, abs⟩
2		eqid 2821	. . . 4 ⊢ ⟨⟨ + , · ⟩, abs⟩ = ⟨⟨ + , · ⟩, abs⟩
3	2	cnnv 28454	. . 3 ⊢ ⟨⟨ + , · ⟩, abs⟩ ∈ NrmCVec
4		mulm1 11081	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℂ → (-1 · 𝑦) = -𝑦)
5	4	adantl 484	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (-1 · 𝑦) = -𝑦)
6	5	oveq2d 7172	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 + (-1 · 𝑦)) = (𝑥 + -𝑦))
7		negsub 10934	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 + -𝑦) = (𝑥 − 𝑦))
8	6, 7	eqtrd 2856	. . . . . . . 8 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 + (-1 · 𝑦)) = (𝑥 − 𝑦))
9	8	fveq2d 6674	. . . . . . 7 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (abs‘(𝑥 + (-1 · 𝑦))) = (abs‘(𝑥 − 𝑦)))
10	9	oveq1d 7171	. . . . . 6 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((abs‘(𝑥 + (-1 · 𝑦)))↑2) = ((abs‘(𝑥 − 𝑦))↑2))
11	10	oveq2d 7172	. . . . 5 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (((abs‘(𝑥 + 𝑦))↑2) + ((abs‘(𝑥 + (-1 · 𝑦)))↑2)) = (((abs‘(𝑥 + 𝑦))↑2) + ((abs‘(𝑥 − 𝑦))↑2)))
12		sqabsadd 14642	. . . . . . . 8 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((abs‘(𝑥 + 𝑦))↑2) = ((((abs‘𝑥)↑2) + ((abs‘𝑦)↑2)) + (2 · (ℜ‘(𝑥 · (∗‘𝑦))))))
13		sqabssub 14643	. . . . . . . 8 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((abs‘(𝑥 − 𝑦))↑2) = ((((abs‘𝑥)↑2) + ((abs‘𝑦)↑2)) − (2 · (ℜ‘(𝑥 · (∗‘𝑦))))))
14	12, 13	oveq12d 7174	. . . . . . 7 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (((abs‘(𝑥 + 𝑦))↑2) + ((abs‘(𝑥 − 𝑦))↑2)) = (((((abs‘𝑥)↑2) + ((abs‘𝑦)↑2)) + (2 · (ℜ‘(𝑥 · (∗‘𝑦))))) + ((((abs‘𝑥)↑2) + ((abs‘𝑦)↑2)) − (2 · (ℜ‘(𝑥 · (∗‘𝑦)))))))
15		abscl 14638	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℂ → (abs‘𝑥) ∈ ℝ)
16	15	recnd 10669	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℂ → (abs‘𝑥) ∈ ℂ)
17	16	sqcld 13509	. . . . . . . . 9 ⊢ (𝑥 ∈ ℂ → ((abs‘𝑥)↑2) ∈ ℂ)
18		abscl 14638	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℂ → (abs‘𝑦) ∈ ℝ)
19	18	recnd 10669	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℂ → (abs‘𝑦) ∈ ℂ)
20	19	sqcld 13509	. . . . . . . . 9 ⊢ (𝑦 ∈ ℂ → ((abs‘𝑦)↑2) ∈ ℂ)
21		addcl 10619	. . . . . . . . 9 ⊢ ((((abs‘𝑥)↑2) ∈ ℂ ∧ ((abs‘𝑦)↑2) ∈ ℂ) → (((abs‘𝑥)↑2) + ((abs‘𝑦)↑2)) ∈ ℂ)
22	17, 20, 21	syl2an 597	. . . . . . . 8 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (((abs‘𝑥)↑2) + ((abs‘𝑦)↑2)) ∈ ℂ)
23		2cn 11713	. . . . . . . . 9 ⊢ 2 ∈ ℂ
24		cjcl 14464	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℂ → (∗‘𝑦) ∈ ℂ)
25		mulcl 10621	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℂ ∧ (∗‘𝑦) ∈ ℂ) → (𝑥 · (∗‘𝑦)) ∈ ℂ)
26	24, 25	sylan2 594	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · (∗‘𝑦)) ∈ ℂ)
27		recl 14469	. . . . . . . . . . 11 ⊢ ((𝑥 · (∗‘𝑦)) ∈ ℂ → (ℜ‘(𝑥 · (∗‘𝑦))) ∈ ℝ)
28	27	recnd 10669	. . . . . . . . . 10 ⊢ ((𝑥 · (∗‘𝑦)) ∈ ℂ → (ℜ‘(𝑥 · (∗‘𝑦))) ∈ ℂ)
29	26, 28	syl 17	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (ℜ‘(𝑥 · (∗‘𝑦))) ∈ ℂ)
30		mulcl 10621	. . . . . . . . 9 ⊢ ((2 ∈ ℂ ∧ (ℜ‘(𝑥 · (∗‘𝑦))) ∈ ℂ) → (2 · (ℜ‘(𝑥 · (∗‘𝑦)))) ∈ ℂ)
31	23, 29, 30	sylancr 589	. . . . . . . 8 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (2 · (ℜ‘(𝑥 · (∗‘𝑦)))) ∈ ℂ)
32	22, 31, 22	ppncand 11037	. . . . . . 7 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (((((abs‘𝑥)↑2) + ((abs‘𝑦)↑2)) + (2 · (ℜ‘(𝑥 · (∗‘𝑦))))) + ((((abs‘𝑥)↑2) + ((abs‘𝑦)↑2)) − (2 · (ℜ‘(𝑥 · (∗‘𝑦)))))) = ((((abs‘𝑥)↑2) + ((abs‘𝑦)↑2)) + (((abs‘𝑥)↑2) + ((abs‘𝑦)↑2))))
33	14, 32	eqtrd 2856	. . . . . 6 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (((abs‘(𝑥 + 𝑦))↑2) + ((abs‘(𝑥 − 𝑦))↑2)) = ((((abs‘𝑥)↑2) + ((abs‘𝑦)↑2)) + (((abs‘𝑥)↑2) + ((abs‘𝑦)↑2))))
34		2times 11774	. . . . . . . 8 ⊢ ((((abs‘𝑥)↑2) + ((abs‘𝑦)↑2)) ∈ ℂ → (2 · (((abs‘𝑥)↑2) + ((abs‘𝑦)↑2))) = ((((abs‘𝑥)↑2) + ((abs‘𝑦)↑2)) + (((abs‘𝑥)↑2) + ((abs‘𝑦)↑2))))
35	34	eqcomd 2827	. . . . . . 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 2856	. . . . 5 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (((abs‘(𝑥 + 𝑦))↑2) + ((abs‘(𝑥 − 𝑦))↑2)) = (2 · (((abs‘𝑥)↑2) + ((abs‘𝑦)↑2))))
38	11, 37	eqtrd 2856	. . . 4 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (((abs‘(𝑥 + 𝑦))↑2) + ((abs‘(𝑥 + (-1 · 𝑦)))↑2)) = (2 · (((abs‘𝑥)↑2) + ((abs‘𝑦)↑2))))
39	38	rgen2 3203	. . 3 ⊢ ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℂ (((abs‘(𝑥 + 𝑦))↑2) + ((abs‘(𝑥 + (-1 · 𝑦)))↑2)) = (2 · (((abs‘𝑥)↑2) + ((abs‘𝑦)↑2)))
40		addex 12388	. . . 4 ⊢ + ∈ V
41		mulex 12389	. . . 4 ⊢ · ∈ V
42		absf 14697	. . . . 5 ⊢ abs:ℂ⟶ℝ
43		cnex 10618	. . . . 5 ⊢ ℂ ∈ V
44		fex 6989	. . . . 5 ⊢ ((abs:ℂ⟶ℝ ∧ ℂ ∈ V) → abs ∈ V)
45	42, 43, 44	mp2an 690	. . . 4 ⊢ abs ∈ V
46		cnaddabloOLD 28358	. . . . . . 7 ⊢ + ∈ AbelOp
47		ablogrpo 28324	. . . . . . 7 ⊢ ( + ∈ AbelOp → + ∈ GrpOp)
48	46, 47	ax-mp 5	. . . . . 6 ⊢ + ∈ GrpOp
49		ax-addf 10616	. . . . . . 7 ⊢ + :(ℂ × ℂ)⟶ℂ
50	49	fdmi 6524	. . . . . 6 ⊢ dom + = (ℂ × ℂ)
51	48, 50	grporn 28298	. . . . 5 ⊢ ℂ = ran +
52	51	isphg 28594	. . . 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 1457	. . 3 ⊢ (⟨⟨ + , · ⟩, abs⟩ ∈ CPreHilOLD ↔ (⟨⟨ + , · ⟩, abs⟩ ∈ NrmCVec ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℂ (((abs‘(𝑥 + 𝑦))↑2) + ((abs‘(𝑥 + (-1 · 𝑦)))↑2)) = (2 · (((abs‘𝑥)↑2) + ((abs‘𝑦)↑2)))))
54	3, 39, 53	mpbir2an 709	. 2 ⊢ ⟨⟨ + , · ⟩, abs⟩ ∈ CPreHilOLD
55	1, 54	eqeltri 2909	1 ⊢ 𝑈 ∈ CPreHilOLD

Syntax hints:   ↔ wb 208   ∧ wa 398   = wceq 1537   ∈ wcel 2114  ∀wral 3138  Vcvv 3494  ⟨cop 4573   × cxp 5553  ⟶wf 6351  ‘cfv 6355  (class class class)co 7156  ℂcc 10535  ℝcr 10536  1c1 10538   + caddc 10540   · cmul 10542   − cmin 10870  -cneg 10871  2c2 11693  ↑cexp 13430  ∗ccj 14455  ℜcre 14456  abscabs 14593  GrpOpcgr 28266  AbelOpcablo 28321  NrmCVeccnv 28361  CPreHil_OLDccphlo 28589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-rep 5190  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461  ax-cnex 10593  ax-resscn 10594  ax-1cn 10595  ax-icn 10596  ax-addcl 10597  ax-addrcl 10598  ax-mulcl 10599  ax-mulrcl 10600  ax-mulcom 10601  ax-addass 10602  ax-mulass 10603  ax-distr 10604  ax-i2m1 10605  ax-1ne0 10606  ax-1rid 10607  ax-rnegex 10608  ax-rrecex 10609  ax-cnre 10610  ax-pre-lttri 10611  ax-pre-lttrn 10612  ax-pre-ltadd 10613  ax-pre-mulgt0 10614  ax-pre-sup 10615  ax-addf 10616  ax-mulf 10617

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4839  df-iun 4921  df-br 5067  df-opab 5129  df-mpt 5147  df-tr 5173  df-id 5460  df-eprel 5465  df-po 5474  df-so 5475  df-fr 5514  df-we 5516  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-pred 6148  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-riota 7114  df-ov 7159  df-oprab 7160  df-mpo 7161  df-om 7581  df-2nd 7690  df-wrecs 7947  df-recs 8008  df-rdg 8046  df-er 8289  df-en 8510  df-dom 8511  df-sdom 8512  df-sup 8906  df-pnf 10677  df-mnf 10678  df-xr 10679  df-ltxr 10680  df-le 10681  df-sub 10872  df-neg 10873  df-div 11298  df-nn 11639  df-2 11701  df-3 11702  df-n0 11899  df-z 11983  df-uz 12245  df-rp 12391  df-seq 13371  df-exp 13431  df-cj 14458  df-re 14459  df-im 14460  df-sqrt 14594  df-abs 14595  df-grpo 28270  df-gid 28271  df-ablo 28322  df-vc 28336  df-nv 28369  df-ph 28590

This theorem is referenced by:  elimphu  28598  cnchl  28693