Metamath Proof Explorer

Theorem tcphip

Description: The inner product of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015)

Ref Expression
Hypotheses tcphval.n ⊒ 𝐺 = ( toβ„‚PreHil β€˜ π‘Š )
tcphip.s ⊒ Β· = ( ·𝑖 β€˜ π‘Š )
Assertion tcphip Β· = ( ·𝑖 β€˜ 𝐺 )

Proof

Step Hyp Ref Expression
1 tcphval.n ⊒ 𝐺 = ( toβ„‚PreHil β€˜ π‘Š )
2 tcphip.s ⊒ Β· = ( ·𝑖 β€˜ π‘Š )
3 eqid ⊒ ( Base β€˜ π‘Š ) = ( Base β€˜ π‘Š )
4 3 tcphex ⊒ ( π‘₯ ∈ ( Base β€˜ π‘Š ) ↦ ( √ β€˜ ( π‘₯ Β· π‘₯ ) ) ) ∈ V
5 1 3 2 tcphval ⊒ 𝐺 = ( π‘Š toNrmGrp ( π‘₯ ∈ ( Base β€˜ π‘Š ) ↦ ( √ β€˜ ( π‘₯ Β· π‘₯ ) ) ) )
6 5 2 tngip ⊒ ( ( π‘₯ ∈ ( Base β€˜ π‘Š ) ↦ ( √ β€˜ ( π‘₯ Β· π‘₯ ) ) ) ∈ V β†’ Β· = ( ·𝑖 β€˜ 𝐺 ) )
7 4 6 ax-mp ⊒ Β· = ( ·𝑖 β€˜ 𝐺 )