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	|- .x. = ( .r ` W )
Assertion	tcphmulr	|- .x. = ( .r ` G )

Proof

Step	Hyp	Ref	Expression
1		tcphval.n	|- G = ( toCPreHil ` W )
2		tcphmulr.t	|- .x. = ( .r ` W )
3		eqid	|- ( Base ` W ) = ( Base ` W )
4	3	tcphex	|- ( x e. ( Base ` W ) |-> ( sqrt ` ( x ( .i ` W ) x ) ) ) e. _V
5		eqid	|- ( .i ` W ) = ( .i ` W )
6	1 3 5	tcphval	|- G = ( W toNrmGrp ( x e. ( Base ` W ) |-> ( sqrt ` ( x ( .i ` W ) x ) ) ) )
7	6 2	tngmulr	|- ( ( x e. ( Base ` W ) |-> ( sqrt ` ( x ( .i ` W ) x ) ) ) e. _V -> .x. = ( .r ` G ) )
8	4 7	ax-mp	|- .x. = ( .r ` G )