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 𝐺 = ( toℂPreHil ‘ 𝑊 )
tcphmulr.t · = ( .r𝑊 )
Assertion tcphmulr · = ( .r𝐺 )

Proof

Step Hyp Ref Expression
1 tcphval.n 𝐺 = ( toℂPreHil ‘ 𝑊 )
2 tcphmulr.t · = ( .r𝑊 )
3 eqid ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
4 3 tcphex ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ ( √ ‘ ( 𝑥 ( ·𝑖𝑊 ) 𝑥 ) ) ) ∈ V
5 eqid ( ·𝑖𝑊 ) = ( ·𝑖𝑊 )
6 1 3 5 tcphval 𝐺 = ( 𝑊 toNrmGrp ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ ( √ ‘ ( 𝑥 ( ·𝑖𝑊 ) 𝑥 ) ) ) )
7 6 2 tngmulr ( ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ ( √ ‘ ( 𝑥 ( ·𝑖𝑊 ) 𝑥 ) ) ) ∈ V → · = ( .r𝐺 ) )
8 4 7 ax-mp · = ( .r𝐺 )