Description: A complex inner product space in terms of ordered pair components. (Contributed by NM, 11-Sep-2007) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | nvop.2 | |
|
nvop.4 | |
||
nvop.6 | |
||
Assertion | nvop | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nvop.2 | |
|
2 | nvop.4 | |
|
3 | nvop.6 | |
|
4 | nvrel | |
|
5 | 1st2nd | |
|
6 | 4 5 | mpan | |
7 | 3 | nmcvfval | |
8 | 7 | opeq2i | |
9 | eqid | |
|
10 | 9 1 2 | nvvop | |
11 | 10 | opeq1d | |
12 | 8 11 | eqtr3id | |
13 | 6 12 | eqtrd | |