Theorem cnph 8478

Description: The set of complex numbers is an inner product (pre-Hilbert) space. (Contributed by Steve Rodriguez, 28-Apr-2007; revised by nm 24-Jul-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 5317	. . . 4 |- + e. V
3		mulex 5318	. . . 4 |- x. e. V
4		axcnex 5267	. . . . 5 |- CC e. V
5		df-abs 6754	. . . . 5 |- abs = {<.x, y>. | (x e. CC /\ y = (sqr` (x x. (*` x))))}
6	4, 5	fopabex2 3612	. . . 4 |- abs e. V
7		cnaddabl 8126	. . . . . . 7 |- + e. Abel
8		ablgrp 8102	. . . . . . 7 |- ( + e. Abel -> + e. Grp)
9	7, 8	ax-mp 7	. . . . . 6 |- + e. Grp
10		axaddopr 5265	. . . . . . 7 |- + :(CC X. CC)-->CC
11	10	fdmi 3632	. . . . . 6 |- dom + = (CC X. CC)
12	9, 11	grprn 8056	. . . . 5 |- CC = ran +
13	12	isphg 8476	. . . 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))))))
14	2, 3, 6, 13	mp3an 916	. . 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)))))
15		eqid 1475	. . . 4 |- <.<. + , x. >., abs>. = <.<. + , x. >., abs>.
16	15	cnnv 8307	. . 3 |- <.<. + , x. >., abs>. e. NrmCVec
17		mulm1t 5471	. . . . . . . . . . 11 |- (y e. CC -> (-u1 x. y) = -uy)
18	17	adantl 388	. . . . . . . . . 10 |- ((x e. CC /\ y e. CC) -> (-u1 x. y) = -uy)
19	18	opreq2d 3976	. . . . . . . . 9 |- ((x e. CC /\ y e. CC) -> (x + (-u1 x. y)) = (x + -uy))
20		negsubt 5382	. . . . . . . . 9 |- ((x e. CC /\ y e. CC) -> (x + -uy) = (x - y))
21	19, 20	eqtrd 1507	. . . . . . . 8 |- ((x e. CC /\ y e. CC) -> (x + (-u1 x. y)) = (x - y))
22	21	fveq2d 3728	. . . . . . 7 |- ((x e. CC /\ y e. CC) -> (abs` (x + (-u1 x. y))) = (abs` (x - y)))
23	22	opreq1d 3975	. . . . . 6 |- ((x e. CC /\ y e. CC) -> ((abs` (x + (-u1 x. y)))^2) = ((abs` (x - y))^2))
24	23	opreq2d 3976	. . . . 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)))
25		sqabsaddt 6848	. . . . . . 7 |- ((x e. CC /\ y e. CC) -> ((abs` (x + y))^2) = ((((abs` x)^2) + ((abs` y)^2)) + (2 x. (Re` (x x. (*` y))))))
26		sqabssubt 6849	. . . . . . 7 |- ((x e. CC /\ y e. CC) -> ((abs` (x - y))^2) = ((((abs` x)^2) + ((abs` y)^2)) - (2 x. (Re` (x x. (*` y))))))
27	25, 26	opreq12d 3978	. . . . . 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)))))))
28		ppncant 5481	. . . . . . 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))))
29		axaddcl 5271	. . . . . . . 8 |- ((((abs` x)^2) e. CC /\ ((abs` y)^2) e. CC) -> (((abs` x)^2) + ((abs` y)^2)) e. CC)
30		absclt 6833	. . . . . . . . . 10 |- (x e. CC -> (abs` x) e. RR)
31	30	recnd 5315	. . . . . . . . 9 |- (x e. CC -> (abs` x) e. CC)
32		sqclt 6611	. . . . . . . . 9 |- ((abs` x) e. CC -> ((abs` x)^2) e. CC)
33	31, 32	syl 10	. . . . . . . 8 |- (x e. CC -> ((abs` x)^2) e. CC)
34		absclt 6833	. . . . . . . . . 10 |- (y e. CC -> (abs` y) e. RR)
35	34	recnd 5315	. . . . . . . . 9 |- (y e. CC -> (abs` y) e. CC)
36		sqclt 6611	. . . . . . . . 9 |- ((abs` y) e. CC -> ((abs` y)^2) e. CC)
37	35, 36	syl 10	. . . . . . . 8 |- (y e. CC -> ((abs` y)^2) e. CC)
38	29, 33, 37	syl2an 454	. . . . . . 7 |- ((x e. CC /\ y e. CC) -> (((abs` x)^2) + ((abs` y)^2)) e. CC)
39		axmulcl 5273	. . . . . . . . 9 |- ((x e. CC /\ (*` y) e. CC) -> (x x. (*` y)) e. CC)
40		cjclt 6764	. . . . . . . . 9 |- (y e. CC -> (*` y) e. CC)
41	39, 40	sylan2 451	. . . . . . . 8 |- ((x e. CC /\ y e. CC) -> (x x. (*` y)) e. CC)
42		reclt 6757	. . . . . . . . 9 |- ((x x. (*` y)) e. CC -> (Re` (x x. (*` y))) e. RR)
43	42	recnd 5315	. . . . . . . 8 |- ((x x. (*` y)) e. CC -> (Re` (x x. (*` y))) e. CC)
44		2cn 5980	. . . . . . . . 9 |- 2 e. CC
45		axmulcl 5273	. . . . . . . . 9 |- ((2 e. CC /\ (Re` (x x. (*` y))) e. CC) -> (2 x. (Re` (x x. (*` y)))) e. CC)
46	44, 45	mpan 695	. . . . . . . 8 |- ((Re` (x x. (*` y))) e. CC -> (2 x. (Re` (x x. (*` y)))) e. CC)
47	41, 43, 46	3syl 20	. . . . . . 7 |- ((x e. CC /\ y e. CC) -> (2 x. (Re` (x x. (*` y)))) e. CC)
48	28, 38, 47, 38	syl3anc 858	. . . . . 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))))
49	27, 48	eqtrd 1507	. . . . 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))))
50		2timest 6004	. . . . . . 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))))
51	50	eqcomd 1480	. . . . . 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))))
52	38, 51	syl 10	. . . . 5 |- ((x e. CC /\ y e. CC) -> ((((abs` x)^2) + ((abs` y)^2)) + (((abs` x)^2) + ((abs` y)^2))) =