HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem ipcj 8301
Description: The complex conjugate of an inner product reverses its arguments. Equation I1 of [Ponnusamy] p. 362.
Hypotheses
Ref Expression
ipcl.1 |- X = (Base` U)
ipcl.7 |- P = (.i` U)
Assertion
Ref Expression
ipcj |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (*` (APB)) = (BPA))
Proof of Theorem ipcj
StepHypRef Expression
1 axaddcl 5243 . . . . 5 |- ((((((norm` U)` (A(+v` U)B))^2) - (((norm` U)` (A(+v` U)(-u1(.s` U)B)))^2)) e. CC /\ (i x. ((((norm` U)` (A(+v` U)(i(.s` U)B)))^2) - (((norm` U)` (A(+v` U)(-ui(.s` U)B)))^2))) e. CC) -> (((((norm` U)` (A(+v` U)B))^2) - (((norm` U)` (A(+v` U)(-u1(.s` U)B)))^2)) + (i x. ((((norm` U)` (A(+v` U)(i(.s` U)B)))^2) - (((norm` U)` (A(+v` U)(-ui(.s` U)B)))^2)))) e. CC)
2 subclt 5339 . . . . . 6 |- (((((norm` U)` (A(+v` U)B))^2) e. CC /\ (((norm` U)` (A(+v` U)(-u1(.s` U)B)))^2) e. CC) -> ((((norm` U)` (A(+v` U)B))^2) - (((norm` U)` (A(+v` U)(-u1(.s` U)B)))^2)) e. CC)
3 ipcl.1 . . . . . . . 8 |- X = (Base` U)
4 eqid 1468 . . . . . . . 8 |- (+v` U) = (+v` U)
5 eqid 1468 . . . . . . . 8 |- (.s` U) = (.s` U)
6 eqid 1468 . . . . . . . 8 |- (norm` U) = (norm` U)
7 ipcl.7 . . . . . . . 8 |- P = (.i` U)
83, 4, 5, 6, 7ipval2lem3 8289 . . . . . . 7 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (((norm` U)` (A(+v` U)B))^2) e. RR)
98recnd 5287 . . . . . 6 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (((norm` U)` (A(+v` U)B))^2) e. CC)
10 ax1cn 5241 . . . . . . . 8 |- 1 e. CC
1110negcl 5341 . . . . . . 7 |- -u1 e. CC
123, 4, 5, 6, 7ipval2lem4 8290 . . . . . . 7 |- (((U e. NrmCVec /\ A e. X /\ B e. X) /\ -u1 e. CC) -> (((norm` U)` (A(+v` U)(-u1(.s` U)B)))^2) e. CC)
1311, 12mpan2 694 . . . . . 6 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (((norm` U)` (A(+v` U)(-u1(.s` U)B)))^2) e. CC)
142, 9, 13sylanc 471 . . . . 5 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> ((((norm` U)` (A(+v` U)B))^2) - (((norm` U)` (A(+v` U)(-u1(.s` U)B)))^2)) e. CC)
15 subclt 5339 . . . . . . 7 |- (((((norm` U)` (A(+v` U)(i(.s` U)B)))^2) e. CC /\ (((norm` U)` (A(+v` U)(-ui(.s` U)B)))^2) e. CC) -> ((((norm` U)` (A(+v` U)(i(.s` U)B)))^2) - (((norm` U)` (A(+v` U)(-ui(.s` U)B)))^2)) e. CC)
16 axicn 5242 . . . . . . . 8 |- i e. CC
173, 4, 5, 6, 7ipval2lem4 8290 . . . . . . . 8 |- (((U e. NrmCVec /\ A e. X /\ B e. X) /\ i e. CC) -> (((norm` U)` (A(+v` U)(i(.s` U)B)))^2) e. CC)
1816, 17mpan2 694 . . . . . . 7 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (((norm` U)` (A(+v` U)(i(.s` U)B)))^2) e. CC)
1916negcl 5341 . . . . . . . 8 |- -ui e. CC
203, 4, 5, 6, 7ipval2lem4 8290 . . . . . . . 8 |- (((U e. NrmCVec /\ A e. X /\ B e. X) /\ -ui e. CC) -> (((norm` U)` (A(+v` U)(-ui(.s` U)B)))^2) e. CC)
2119, 20mpan2 694 . . . . . . 7 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (((norm` U)` (A(+v` U)(-ui(.s` U)B)))^2) e. CC)
2215, 18, 21sylanc 471 . . . . . 6 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> ((((norm` U)` (A(+v` U)(i(.s` U)B)))^2) - (((norm` U)` (A(+v` U)(-ui(.s` U)B)))^2)) e. CC)
23 axmulcl 5245 . . . . . . 7 |- ((i e. CC /\ ((((norm` U)` (A(+v` U)(i(.s` U)B)))^2) - (((norm` U)` (A(+v` U)(-ui(.s` U)B)))^2)) e. CC) -> (i x. ((((norm` U)` (A(+v` U)(i(.s` U)B)))^2) - (((norm` U)` (A(+v` U)(-ui(.s` U)B)))^2))) e. CC)
2416, 23mpan 693 . . . . . 6 |- (((((norm` U)` (A(+v` U)(i(.s` U)B)))^2) - (((norm` U)` (A(+v` U)(-ui(.s` U)B)))^2)) e. CC -> (i x. ((((norm` U)` (A(+v` U)(i(.s` U)B)))^2) - (((norm` U)` (A(+v` U)(-ui(.s` U)B)))^2))) e. CC)
2522, 24syl 10 . . . . 5 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (i x. ((((norm` U)` (A(+v` U)(i(.s` U)B)))^2) - (((norm` U)` (A(+v` U)(-ui(.s` U)B)))^2))) e. CC)
261, 14, 25sylanc 471 . . . 4 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (((((norm` U)` (A(+v` U)B))^2) - (((norm` U)` (A(+v` U)(-u1(.s` U)B)))^2)) + (i x. ((((norm` U)` (A(+v` U)(i(.s` U)B)))^2) - (((norm` U)` (A(+v` U)(-ui(.s` U)B)))^2)))) e. CC)
27 4re 5929 . . . . . 6 |- 4 e. RR
2827recn 5286 . . . . 5 |- 4 e. CC
29 4pos 5939 . . . . . 6 |- 0 < 4
3027, 29gt0ne0i 5591 . . . . 5 |- 4 =/= 0
31 cjdivt 6827 . . . . 5 |- (((((((norm` U)` (A(+v` U)B))^2) - (((norm` U)` (A(+v` U)(-u1(.s` U)B)))^2)) + (i x. ((((norm` U)` (A(+v` U)(i(.s` U)B)))^2) - (((norm` U)` (A(+v` U)(-ui(.s` U)B)))^2)))) e. CC /\ 4 e. CC /\ 4 =/= 0) -> (*` ((((((norm` U)` (A(+v` U)B))^2) - (((norm` U)` (A(+v` U)(-u1(.s` U)B)))^2)) + (i x. ((((norm` U)` (A(+v` U)(i(.s` U)B)))^2) - (((norm` U)` (A(+v` U)(-ui(.s` U)B)))^2)))) / 4)) = ((*` (((((norm` U)` (A(+v` U)B))^2) - (((norm` U)` (A(+v` U)(-u1(.s` U)B)))^2)) + (i x. ((((norm` U)` (A(+v` U)(i(.s` U)B)))^2) - (((norm` U)` (A(+v` U)(-ui(.s` U)B)))^2))))) / (*` 4)))
3228, 30, 31mp3an23 905 . . . 4 |- ((((((norm` U)` (A(+v` U)B))^2) - (((norm` U)` (A(+v` U)(-u1(.s` U)B)))^2)) + (i x. ((((norm