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=\mathrm{toCPreHil}\left(W\right)$$
	tcphmulr.t	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
Assertion	tcphmulr	$$⊢\underset{\dot{}}{·}={\cdot }_G$$

Proof

Step	Hyp	Ref	Expression
1		tcphval.n	$$⊢G=\mathrm{toCPreHil}\left(W\right)$$
2		tcphmulr.t	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
3		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
4	3	tcphex	$$⊢\left(x\in {\mathrm{Base}}_W⟼\sqrt{x{\cdot }_{𝑖}\left(W\right)x}\right)\in \mathrm{V}$$
5		eqid	$$⊢{\cdot }_{𝑖}\left(W\right)={\cdot }_{𝑖}\left(W\right)$$
6	1 3 5	tcphval	$$⊢G=W\mathrm{toNrmGrp}\left(x\in {\mathrm{Base}}_W⟼\sqrt{x{\cdot }_{𝑖}\left(W\right)x}\right)$$
7	6 2	tngmulr	$$⊢\left(x\in {\mathrm{Base}}_W⟼\sqrt{x{\cdot }_{𝑖}\left(W\right)x}\right)\in \mathrm{V}\to \underset{\dot{}}{·}={\cdot }_G$$
8	4 7	ax-mp	$$⊢\underset{\dot{}}{·}={\cdot }_G$$