Description: The ring operation of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | tcphval.n | ||
tcphmulr.t | |||
Assertion | tcphmulr |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tcphval.n | ||
2 | tcphmulr.t | ||
3 | eqid | ||
4 | 3 | tcphex | |
5 | eqid | ||
6 | 1 3 5 | tcphval | |
7 | 6 2 | tngmulr | |
8 | 4 7 | ax-mp |