Description: Conjugate of an inner product in a pre-Hilbert space. Equation I1 of Ponnusamy p. 362. (Contributed by NM, 1-Feb-2007) (Revised by Mario Carneiro, 7-Oct-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | phlsrng.f | |
|
phllmhm.h | |
||
phllmhm.v | |
||
ipcj.i | |
||
Assertion | ipcj | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | phlsrng.f | |
|
2 | phllmhm.h | |
|
3 | phllmhm.v | |
|
4 | ipcj.i | |
|
5 | eqid | |
|
6 | eqid | |
|
7 | 3 1 2 5 4 6 | isphl | |
8 | 7 | simp3bi | |
9 | simp3 | |
|
10 | 9 | ralimi | |
11 | 8 10 | syl | |
12 | fvoveq1 | |
|
13 | oveq2 | |
|
14 | 12 13 | eqeq12d | |
15 | oveq2 | |
|
16 | 15 | fveq2d | |
17 | oveq1 | |
|
18 | 16 17 | eqeq12d | |
19 | 14 18 | rspc2v | |
20 | 11 19 | syl5com | |
21 | 20 | 3impib | |