Theorem cnph 8422

Description: The set of complex numbers is an inner product (pre-Hilbert) space. (Contributed by Steve Rodriguez, 28-Apr-2007; revised by nm 15-Jan-2008.)

Hypothesis

Ref	Expression
cnph.6	|- U = <.<. + , x. >., abs>.

Assertion

Ref	Expression
cnph	|- U e. CPreHil

Proof of Theorem cnph

Step	Hyp	Ref	Expression
1		cnph.6	. 2 |- U = <.<. + , x. >., abs>.
2		addex 5297	. . . 4 |- + e. V
3		mulex 5298	. . . 4 |- x. e. V
4		axcnex 5247	. . . . 5 |- CC e. V
5		df-abs 6693	. . . . 5 |- abs = {<.x, y>. | (x e. CC /\ y = (sqr` (x x. (*` x))))}
6	4, 5	fopabex2 3604	. . . 4 |- abs e. V
7		cnaddabl 8078	. . . . . . 7 |- + e. Abel
8		ablgrp 8053	. . . . . . 7 |- ( + e. Abel -> + e. Grp)
9	7, 8	ax-mp 7	. . . . . 6 |- + e. Grp
10		axaddopr 5245	. . . . . 6 |- + :(CC X. CC)-->CC
11	9, 10	grprnOLD 8007	. . . . 5 |- CC = ran +
12	11	isphg 8420	. . . 4 |- (( + e. V /\ x. e. V /\ abs e. V) -> (<.<. + , x. >., abs>. e. CPreHil <-> (<.<. + , x. >., abs>. e. NrmCVec /\ A.x e. CC A.y e. CC (((abs` (x + y))^2) + ((abs` (x + (-u1 x. y)))^2)) = (2 x. (((abs` x)^2) + ((abs` y)^2))))))
13	2, 3, 6, 12	mp3an 914	. . 3 |- (<.<. + , x. >., abs>. e. CPreHil <-> (<.<. + , x. >., abs>. e. NrmCVec /\ A.x e. CC A.y e. CC (((abs` (x + y))^2) + ((abs` (x + (-u1 x. y)))^2)) = (2 x. (((abs` x)^2) + ((abs` y)^2)))))
14		eqid 1473	. . . 4 |- <.<. + , x. >., abs>. = <.<. + , x. >., abs>.
15	14	cnnv 8258	. . 3 |- <.<. + , x. >., abs>. e. NrmCVec
16		mulm1t 5451	. . . . . . . . . . 11 |- (y e. CC -> (-u1 x. y) = -uy)
17	16	adantl 388	. . . . . . . . . 10 |- ((x e. CC /\ y e. CC) -> (-u1 x. y) = -uy)
18	17	opreq2d 3967	. . . . . . . . 9 |- ((x e. CC /\ y e. CC) -> (x + (-u1 x. y)) = (x + -uy))
19		negsubt 5362	. . . . . . . . 9 |- ((x e. CC /\ y e. CC) -> (x + -uy) = (x - y))
20	18, 19	eqtrd 1504	. . . . . . . 8 |- ((x e. CC /\ y e. CC) -> (x + (-u1 x. y)) = (x - y))
21	20	fveq2d 3719	. . . . . . 7 |- ((x e. CC /\ y e. CC) -> (abs` (x + (-u1 x. y))) = (abs` (x - y)))
22	21	opreq1d 3966	. . . . . 6 |- ((x e. CC /\ y e. CC) -> ((abs` (x + (-u1 x. y)))^2) = ((abs` (x - y))^2))
23	22	opreq2d 3967	. . . . 5 |- ((x e. CC /\ y e. CC) -> (((abs` (x + y))^2) + ((abs` (x + (-u1 x. y)))^2)) = (((abs` (x + y))^2) + ((abs` (x - y))^2)))
24		sqabsaddt 6791	. . . . . . 7 |- ((x e. CC /\ y e. CC) -> ((abs` (x + y))^2) = ((((abs` x)^2) + ((abs` y)^2)) + (2 x. (Re` (x x. (*` y))))))
25		sqabssubt 6792	. . . . . . 7 |- ((x e. CC /\ y e. CC) -> ((abs` (x - y))^2) = ((((abs` x)^2) + ((abs` y)^2)) - (2 x. (Re` (x x. (*` y))))))
26	24, 25	opreq12d 3969	. . . . . 6 |- ((x e. CC /\ y e. CC) -> (((abs` (x + y))^2) + ((abs` (x - y))^2)) = (((((abs` x)^2) + ((abs` y)^2)) + (2 x. (Re` (x x. (*` y))))) + ((((abs` x)^2) + ((abs` y)^2)) - (2 x. (Re` (x x. (*` y)))))))
27		ppncant 5461	. . . . . . 7 |- (((((abs` x)^2) + ((abs` y)^2)) e. CC /\ (2 x. (Re` (x x. (*` y)))) e. CC /\ (((abs` x)^2) + ((abs` y)^2)) e. CC) -> (((((abs` x)^2) + ((abs` y)^2)) + (2 x. (Re` (x x. (*` y))))) + ((((abs` x)^2) + ((abs` y)^2)) - (2 x. (Re` (x x. (*` y)))))) = ((((abs` x)^2) + ((abs` y)^2)) + (((abs` x)^2) + ((abs` y)^2))))
28		axaddcl 5251	. . . . . . . 8 |- ((((abs` x)^2) e. CC /\ ((abs` y)^2) e. CC) -> (((abs` x)^2) + ((abs` y)^2)) e. CC)
29		absclt 6776	. . . . . . . . . 10 |- (x e. CC -> (abs` x) e. RR)
30	29	recnd 5295	. . . . . . . . 9 |- (x e. CC -> (abs` x) e. CC)
31		sqclt 6550	. . . . . . . . 9 |- ((abs` x) e. CC -> ((abs` x)^2) e. CC)
32	30, 31	syl 10	. . . . . . . 8 |- (x e. CC -> ((abs` x)^2) e. CC)
33		absclt 6776	. . . . . . . . . 10 |- (y e. CC -> (abs` y) e. RR)
34	33	recnd 5295	. . . . . . . . 9 |- (y e. CC -> (abs` y) e. CC)
35		sqclt 6550	. . . . . . . . 9 |- ((abs` y) e. CC -> ((abs` y)^2) e. CC)
36	34, 35	syl 10	. . . . . . . 8 |- (y e. CC -> ((abs` y)^2) e. CC)
37	28, 32, 36	syl2an 454	. . . . . . 7 |- ((x e. CC /\ y e. CC) -> (((abs` x)^2) + ((abs` y)^2)) e. CC)
38		axmulcl 5253	. . . . . . . . 9 |- ((x e. CC /\ (*` y) e. CC) -> (x x. (*` y)) e. CC)
39		cjclt 6704	. . . . . . . . 9 |- (y e. CC -> (*` y) e. CC)
40	38, 39	sylan2 451	. . . . . . . 8 |- ((x e. CC /\ y e. CC) -> (x x. (*` y)) e. CC)
41		reclt 6696	. . . . . . . . 9 |- ((x x. (*` y)) e. CC -> (Re` (x x. (*` y))) e. RR)
42	41	recnd 5295	. . . . . . . 8 |- ((x x. (*` y)) e. CC -> (Re` (x x. (*` y))) e. CC)
43		2cn 5935	. . . . . . . . 9 |- 2 e. CC
44		axmulcl 5253	. . . . . . . . 9 |- ((2 e. CC /\ (Re` (x x. (*` y))) e. CC) -> (2 x. (Re` (x x. (*` y)))) e. CC)
45	43, 44	mpan 694	. . . . . . . 8 |- ((Re` (x x. (*` y))) e. CC -> (2 x. (Re` (x x. (*` y)))) e. CC)
46	40, 42, 45	3syl 20	. . . . . . 7 |- ((x e. CC /\ y e. CC) -> (2 x. (Re` (x x. (*` y)))) e. CC)
47	27, 37, 46, 37	syl3anc 857	. . . . . 6 |- ((x e. CC /\ y e. CC) -> (((((abs` x)^2) + ((abs` y)^2)) + (2 x. (Re` (x x. (*` y))))) + ((((abs` x)^2) + ((abs` y)^2)) - (2 x. (Re` (x x. (*` y)))))) = ((((abs` x)^2) + ((abs` y)^2)) + (((abs` x)^2) + ((abs` y)^2))))
48	26, 47	eqtrd 1504	. . . . 5 |- ((x e. CC /\ y e. CC) -> (((abs` (x + y))^2) + ((abs` (x - y))^2)) = ((((abs` x)^2) + ((abs` y)^2)) + (((abs` x)^2) + ((abs` y)^2))))
49		2timest 5959	. . . . . . 7 |- ((((abs` x)^2) + ((abs` y)^2)) e. CC -> (2 x. (((abs` x)^2) + ((abs` y)^2))) = ((((abs` x)^2) + ((abs` y)^2)) + (((abs` x)^2) + ((abs` y)^2))))
50	49	eqcomd 1477	. . . . . 6 |- ((((abs` x)^2) + ((abs` y)^2)) e. CC -> ((((abs` x)^2) + ((abs` y)^2)) + (((abs` x)^2) + ((abs` y)^2))) = (2 x. (((abs` x)^2) + ((abs` y)^2))))
51	37, 50	syl 10	. . . . 5 |- ((x e. CC /\ y e. CC) -> ((((abs` x)^2) + ((abs` y)^2)) + (((abs` x)^2) + ((abs` y)^2))) = (2 x. (((abs` x)^2) +