HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem cnph 8409
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
StepHypRef Expression
1 cnph.6 . 2 |- U = <.<. + , x. >., abs>.
2 addex 5289 . . . 4 |- + e. V
3 mulex 5290 . . . 4 |- x. e. V
4 axcnex 5239 . . . . 5 |- CC e. V
5 df-abs 6685 . . . . 5 |- abs = {<.x, y>. | (x e. CC /\ y = (sqr` (x x. (*` x))))}
64, 5fopabex2 3598 . . . 4 |- abs e. V
7 cnaddabl 8063 . . . . . . 7 |- + e. Abel
8 ablgrp 8038 . . . . . . 7 |- ( + e. Abel -> + e. Grp)
97, 8ax-mp 7 . . . . . 6 |- + e. Grp
10 axaddopr 5237 . . . . . 6 |- + :(CC X. CC)-->CC
119, 10grprnOLD 7991 . . . . 5 |- CC = ran +
1211isphg 8407 . . . 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))))))
132, 3, 6, 12mp3an 913 . . 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 1468 . . . 4 |- <.<. + , x. >., abs>. = <.<. + , x. >., abs>.
1514cnnv 8245 . . 3 |- <.<. + , x. >., abs>. e. NrmCVec
16 mulm1t 5443 . . . . . . . . . . 11 |- (y e. CC -> (-u1 x. y) = -uy)
1716adantl 388 . . . . . . . . . 10 |- ((x e. CC /\ y e. CC) -> (-u1 x. y) = -uy)
1817opreq2d 3961 . . . . . . . . 9 |- ((x e. CC /\ y e. CC) -> (x + (-u1 x. y)) = (x + -uy))
19 negsubt 5354 . . . . . . . . 9 |- ((x e. CC /\ y e. CC) -> (x + -uy) = (x - y))
2018, 19eqtrd 1499 . . . . . . . 8 |- ((x e. CC /\ y e. CC) -> (x + (-u1 x. y)) = (x - y))
2120fveq2d 3713 . . . . . . 7 |- ((x e. CC /\ y e. CC) -> (abs` (x + (-u1 x. y))) = (abs` (x - y)))
2221opreq1d 3960 . . . . . 6 |- ((x e. CC /\ y e. CC) -> ((abs` (x + (-u1 x. y)))^2) = ((abs` (x - y))^2))
2322opreq2d 3961 . . . . 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 6783 . . . . . . 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 6784 . . . . . . 7 |- ((x e. CC /\ y e. CC) -> ((abs` (x - y))^2) = ((((abs` x)^2) + ((abs` y)^2)) - (2 x. (Re` (x x. (*` y))))))
2624, 25opreq12d 3963 . . . . . 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 5453 . . . . . . 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 5243 . . . . . . . 8 |- ((((abs` x)^2) e. CC /\ ((abs` y)^2) e. CC) -> (((abs` x)^2) + ((abs` y)^2)) e. CC)
29 absclt 6768 . . . . . . . . . 10 |- (x e. CC -> (abs` x) e. RR)
3029recnd 5287 . . . . . . . . 9 |- (x e. CC -> (abs` x) e. CC)
31 sqclt 6542 . . . . . . . . 9 |- ((abs` x) e. CC -> ((abs` x)^2) e. CC)
3230, 31syl 10 . . . . . . . 8 |- (x e. CC -> ((abs` x)^2) e. CC)
33 absclt 6768 . . . . . . . . . 10 |- (y e. CC -> (abs` y) e. RR)
3433recnd 5287 . . . . . . . . 9 |- (y e. CC -> (abs` y) e. CC)
35 sqclt 6542 . . . . . . . . 9 |- ((abs` y) e. CC -> ((abs` y)^2) e. CC)
3634, 35syl 10 . . . . . . . 8 |- (y e. CC -> ((abs` y)^2) e. CC)
3728, 32, 36syl2an 454 . . . . . . 7 |- ((x e. CC /\ y e. CC) -> (((abs` x)^2) + ((abs` y)^2)) e. CC)
38 axmulcl 5245 . . . . . . . . 9 |- ((x e. CC /\ (*` y) e. CC) -> (x x. (*` y)) e. CC)
39 cjclt 6696 . . . . . . . . 9 |- (y e. CC -> (*` y) e. CC)
4038, 39sylan2 451 . . . . . . . 8 |- ((x e. CC /\ y e. CC) -> (x x. (*` y)) e. CC)
41 reclt 6688 . . . . . . . . 9 |- ((x x. (*` y)) e. CC -> (Re` (x x. (*` y))) e. RR)
4241recnd 5287 . . . . . . . 8 |- ((x x. (*` y)) e. CC -> (Re` (x x. (*` y))) e. CC)
43 2cn 5927 . . . . . . . . 9 |- 2 e. CC
44 axmulcl 5245 . . . . . . . . 9 |- ((2 e. CC /\ (Re` (x x. (*` y))) e. CC) -> (2 x. (Re` (x x. (*` y)))) e. CC)
4543, 44mpan 693 . . . . . . . 8 |- ((Re` (x x. (*` y))) e. CC -> (2 x. (Re` (x x. (*` y)))) e. CC)
4640, 42, 453syl 20 . . . . . . 7 |- ((x e. CC /\ y e. CC) -> (2 x. (Re` (x x. (*` y)))) e. CC)
4727, 37, 46, 37syl3anc 856 . . . . . 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))))
4826, 47eqtrd 1499 . . . . 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 5951 . . . . . . 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))))
5049eqcomd 1472 . . . . . 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))))
5137, 50syl 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) +