Metamath Proof Explorer


Theorem tcphmulr

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 G = toCPreHil W
tcphmulr.t · ˙ = W
Assertion tcphmulr · ˙ = G

Proof

Step Hyp Ref Expression
1 tcphval.n G = toCPreHil W
2 tcphmulr.t · ˙ = W
3 eqid Base W = Base W
4 3 tcphex x Base W x 𝑖 W x V
5 eqid 𝑖 W = 𝑖 W
6 1 3 5 tcphval G = W toNrmGrp x Base W x 𝑖 W x
7 6 2 tngmulr x Base W x 𝑖 W x V · ˙ = G
8 4 7 ax-mp · ˙ = G