Theorem tcphbas

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

	Ref	Expression
Hypotheses	tcphval.n	|- G = ( toCPreHil ` W )
	tcphbas.v	|- V = ( Base ` W )
Assertion	tcphbas	|- V = ( Base ` G )

Proof

Step	Hyp	Ref	Expression
1		tcphval.n	|- G = ( toCPreHil ` W )
2		tcphbas.v	|- V = ( Base ` W )
3	2	tcphex	|- ( x e. V |-> ( sqrt ` ( x ( .i ` W ) x ) ) ) e. _V
4		eqid	|- ( .i ` W ) = ( .i ` W )
5	1 2 4	tcphval	|- G = ( W toNrmGrp ( x e. V |-> ( sqrt ` ( x ( .i ` W ) x ) ) ) )
6	5 2	tngbas	|- ( ( x e. V |-> ( sqrt ` ( x ( .i ` W ) x ) ) ) e. _V -> V = ( Base ` G ) )
7	3 6	ax-mp	|- V = ( Base ` G )